Abstract
Hermanns has introduced interactive Markov chains (IMCs) which arise as an orthogonal extension of labelled transition systems and continuous-time Markov chains (CTMCs). IMCs enjoy nice compositional aggregation properties which help to minimize the state space incrementally. However, the model checking problem for IMCs remains unsolved apart from those instances, where the IMC can be converted into a CTMC. This paper tackles this problem: We interpret the continuous stochastic logic (CSL) over IMCs and define the semantics of probabilistic CSL formulas with respect to the class of fully time and history dependent schedulers. Our main contribution is an efficient model checking algorithm for verifying CSL formulas on IMCs. Moreover, we show the applicability of our approach and provide some experimental results.
Supported by the NWO projects QUPES (612.000.420), by the EU grant FP7-ICT-2007-1 (QUASIMODO) and the DFG as part of SFB/TR 14 AVACS.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Ash, R., Doléans-Dade, C.: Probability & Measure Theory, 2nd edn. Academic Press, London (2000)
Aziz, A., Sanwal, K., Singhal, V., Brayton, R.K.: Verifying continuous time Markov chains. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 269–276. Springer, Heidelberg (1996)
Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P.: Model-checking algorithms for continuous-time Markov chains. IEEE TSE 29, 524–541 (2003)
Baier, C., Hermanns, H., Katoen, J.-P., Haverkort, B.R.: Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes. Theor. Comp. Sci. 345, 2–26 (2005)
Bertsekas, D.: Dynamic Programming and Optimal Control, vol. II. Athena Scientific, Belmont (1995)
Bianco, A., de Alfaro, L.: Model checking of probabilistic and nondeterministic systems. In: Thiagarajan, P.S. (ed.) FSTTCS 1995. LNCS, vol. 1026, pp. 499–513. Springer, Heidelberg (1995)
Böde, E., Herbstritt, M., Hermanns, H., Johr, S., Peikenkamp, T., Pulungan, R., Rakow, J., Wimmer, R., Becker, B.: Compositional dependability evaluation for STATEMATE. IEEE Trans. Software Eng. 35, 274–292 (2009)
Boudali, H., Crouzen, P., Haverkort, B.R., Kuntz, M., Stoelinga, M.: Architectural dependability evaluation with Arcade. In: DSN, pp. 512–521. IEEE, Los Alamitos (2008)
Bouyer, P., Forejt, V.: Reachability in stochastic timed games. In: Albers, S., Marchetti-Spaccamela, A., Matias, Y., Nikoletseas, S., Thomas, W. (eds.) ICALP 2009. LNCS, vol. 5556, pp. 103–114. Springer, Heidelberg (2009)
Bravetti, M., Hermanns, H., Katoen, J.-P.: YMCA: Why Markov chain algebra? In: Essays on Algebraic Process Calculi. Electronic Notes in Theoretical Computer Science, vol. 162, pp. 107–112. Elsevier, Amsterdam (2006)
Brazdil, T., Forejt, V., Krcal, J., Kretinsky, J., Kucera, A.: Continuous-time stochastic games with time-bounded reachability. In: FSTTCS. LIPIcs (2009) (to appear)
Cerotti, D., Donatelli, S., Horváth, A., Sproston, J.: CSL model checking for generalized stochastic Petri nets. In: QEST, pp. 199–210. IEEE, Los Alamitos (2006)
Coppersmith, D., Winograd, S.: Matrix multiplication via arithmetic progressions. In: ACM Symposium on Theory of Computing. ACM, New York (1987)
Coste, N., Garavel, H., Hermanns, H., Hersemeule, R., Thonnart, Y., Zidouni, M.: Quantitative evaluation in embedded system design: Validation of multiprocessor multithreaded architectures. In: DATE, pp. 88–89. IEEE, Los Alamitos (2008)
Coste, N., Hermanns, H., Lantreibecq, E., Serwe, W.: Towards performance prediction of compositional models in industrial GALS designs. In: Bouajjani, A., Maler, O. (eds.) Computer Aided Verification. LNCS, vol. 5643, pp. 204–218. Springer, Heidelberg (2009)
Haverkort, B.R., Hermanns, H., Katoen, J.-P.: On the use of model checking techniques for dependability evaluation. In: Reliable Distributed Systems, pp. 228–239. IEEE, Los Alamitos (2000)
Hermanns, H. (ed.): Interactive Markov Chains: The Quest for Quantified Quality. LNCS, vol. 2428. Springer, Heidelberg (2002)
Hermanns, H., Herzog, U., Katoen, J.-P.: Process algebra for performance evaluation. Theor. Comp. Sci. 274, 43–87 (2002)
Hermanns, H., Katoen, J.-P.: Automated compositional Markov chain generation for a plain-old telephone system. Sci. Comput. Program. 36, 97–127 (2000)
Hillston, J.: A Compositional Approach to Performance Modelling. Cambridge University Press, Cambridge (1996)
Johr, S.: Model Checking Compositional Markov Systems. PhD thesis, Saarland University, Saarbrücken, Germany (2007)
Maciá, H., Valero, V., Cuartero, F., Ruiz, M.C.: sPBC: A Markovian extension of Petri box calculus with immediate multiactions. Fundamenta Informaticae 87, 367–406 (2008)
Neuhäußer, M.R.: Model Checking Nondeterministic and Randomly Timed Systems. PhD thesis, RWTH Aachen University, Aachen, Germany (2010)
Neuhäußer, M.R., Stoelinga, M., Katoen, J.-P.: Delayed nondeterminism in continuous-time Markov decision processes. In: de Alfaro, L. (ed.) FOSSACS 2009. LNCS, vol. 5504, pp. 364–379. Springer, Heidelberg (2009)
Neuhäußer, M.R., Zhang, L.: Time-bounded reachability in continuous-time Markov decision processes. Technical report, RWTH Aachen University (2009)
Pulungan, R.: Reduction of Acyclic Phase-Type Representations. PhD thesis, Universität des Saarlandes, Saarbrücken, Germany (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Zhang, L., Neuhäußer, M.R. (2010). Model Checking Interactive Markov Chains. In: Esparza, J., Majumdar, R. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2010. Lecture Notes in Computer Science, vol 6015. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-12002-2_5
Download citation
DOI: https://doi.org/10.1007/978-3-642-12002-2_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-12001-5
Online ISBN: 978-3-642-12002-2
eBook Packages: Computer ScienceComputer Science (R0)