This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Model-Checking Algorithms for Continuous-Time Markov Chains
June 2003 (vol. 29 no. 6)
pp. 524-541

Abstract—Continuous-time Markov chains (CTMCs) have been widely used to determine system performance and dependability characteristics. Their analysis most often concerns the computation of steady-state and transient-state probabilities. This paper introduces a branching temporal logic for expressing real-time probabilistic properties on CTMCs and presents approximate model checking algorithms for this logic. The logic, an extension of the continuous stochastic logic CSL of Aziz et al., contains a time-bounded until operator to express probabilistic timing properties over paths as well as an operator to express steady-state probabilities. We show that the model checking problem for this logic reduces to a system of linear equations (for unbounded until and the steady-state operator) and a Volterra integral equation system (for time-bounded until). We then show that the problem of model-checking time-bounded until properties can be reduced to the problem of computing transient state probabilities for CTMCs. This allows the verification of probabilistic timing properties by efficient techniques for transient analysis for CTMCs such as uniformization. Finally, we show that a variant of lumping equivalence (bisimulation), a well-known notion for aggregating CTMCs, preserves the validity of all formulas in the logic.

[1] A.V. Aho, J.E. Hopcroft, and J.D. Ullmann, The Design and Analysis of Computer Algorithms. Addison-Wesley, 1974.
[2] M. Ajmone Marsan, G. Balbo, G. Conte, S. Donatelli, and G. Franceschinis, Modeling with Generalized Stochastic Petri Nets. John Wiley&Sons, 1995.
[3] L. de Alfaro, Formal Verification of Probabilistic Systems PhD dissertation, Stanford Univ., 1997.
[4] L. de Alfaro, Temporal Logics for the Specification of Performance and Reliability Proc. Fourth Ann. Symp. Theoretical Aspects of Computer Science, 1997.
[5] L. de Alfaro, How to Specify and Verify the Long-Run Average Behavior of Probabilistic Systems Proc. IEEE 13th Symp. Logic in Computer Science, pp. 174-183, 1998.
[6] R. Alur and D. Dill, A Theory of Timed Automata Theoretical Computer Science, vol. 126, pp. 183-235, 1994.
[7] R. Alur, C. Courcoubetis, and D. Dill, Model-Checking for Probabilistic Real-Time Systems Automata, Languages, and Programming, 1991.
[8] A. Aziz, V. Singhal, F. Balarin, R. Brayton, and A. Sangiovanni-Vincentelli, It Usually Works: The Temporal Logic of Stochastic Systems Computer-Aided Verification, 1995.
[9] A. Aziz, K. Sanwal, V. Singhal, and R. Brayton, Model Checking Continuous Time Markov Chains ACM Trans. Computational Logic, vol. 1, no. 1, pp. 162-170, 2000.
[10] C. Baier, On Algorithmic Verification Methods for Probabilistic Systems habilitation thesis, Univ. of Mannheim, Germany, 1999, avaliable atweb.informatik.uni-bonn.de/I/papershaupt.ps .
[11] C. Baier, J.-P. Katoen, and H. Hermanns, Approximate Symbolic Model Checking of Continuous-Time Markov Chains Concurrency Theory, 1999.
[12] C. Baier, B.R. Haverkort, and H. Hermanns, J.-P. Katoen, Model Checking Continuous-Time Markov Chains by Transient Analysis Computer Aided Verification, 2000.
[13] C. Baier, B.R. Haverkort, H. Hermanns, and J.-P. Katoen, On the Logical Characterisation of Performability Properties Automata, Languages, and Programming, 2000.
[14] C. Baier and M. Kwiatkowska, On the Verification of Qualitative Properties of Probabilistic Processes Under Fairness Constraints Information Processing Letters, vol. 66, no. 2, pp. 71-79, 1998.
[15] C. Baier and M.Z. Kwiatkowska, Model Checking for a Probabilistic Branching Time Logic with Fairness Distributed Computing, vol. 11, pp. 125-155, 1998.
[16] A. Bianco and L. de Alfaro, Model Checking of Probabilistic and Nondeterministic Systems Foundations of Software Technology and Theoretical Computer Science, 1995.
[17] M. Brown, E. Clarke, and O. Grumberg, Characterizing Finite Kripke Structures in Propositional Temporal Logic Theoretical Computer Science, vol. 59, pp. 115-131, 1988.
[18] P. Buchholz, Exact and Ordinary Lumpability in Finite Markov Chains J. Applied Probability, vol. 31, pp. 59-75, 1994.
[19] P. Buchholz, Markovian Process Algebra Technical Report 500, Fachbereich Informatik, Univ. of Dortmund, 1994.
[20] P. Buchholz, J.-P. Katoen, P. Kemper, and C. Tepper, Model-Checking Large Structured Markov Chains J. Logic and Algebraic Programming, to appear.
[21] G. Ciardo, J. Muppala, and K. Trivedi, SPNP: Stochastic Petri Net Package Proc. Third Int'l Workshop Petri Nets and Performance Models, pp. 142-151, 1989.
[22] A. Cimatti, E. Clarke, F. Giunchiglia, and M. Roveri, NuSMV: A New Symbolic Model Checker J. Software Tools for Technology Transfer, vol. 2, pp. 410-425, 2000.
[23] E. Clarke, E. Emerson, and A. Sistla, Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications ACM Trans. Programming Languages and Systems, vol. 8, pp. 244-263, 1986.
[24] E. Clarke, M. Fujita, P.C. McGeer, and J.C-Y. Yang, Multi-Terminal Binary Decision Diagrams: An Efficient Data Structure for Matrix Representation Formal Methods in System Design, vol. 10, nos. 2/3, pp. 149-169, 1997.
[25] E. Clarke, O. Grumberg, and D. Peled, Model Checking. MIT Press, 1999.
[26] A.E. Conway and N.D. Georganas, Queueing Networks: Exact Computational Algorithms. MIT Press, 1989.
[27] C. Courcoubetis and M. Yannakakis, Verifying Temporal Properties of Finite-State Probabilistic Programs Proc. Ann. Symp. Foundations of Computer Science, pp. 338-345, 1988.
[28] C. Courcoubetis and M. Yannakakis, The Complexity of Probabilistic Verification J. ACM, vol. 42, no. 4, pp. 857-907, 1995.
[29] S. Derisavi, H. Hermanns, and W.H. Sanders, Optimal State-Space Lumping in Markov Chains Information Processing Letters, to appear.
[30] J. Desharnais and P. Panangaden, Continuous Stochastic Logic Characterizes Bisimulation of Continuous-Time Markov Processes J. Logic and Algebraic Programming, to appear.
[31] D.L. Dill, The Murphi Verification System Computer-Aided Verification, 1996.
[32] E.A. Emerson and E.M. Clarke, Using Branching Time Temporal Logic to Synthesize Synchronization Skeletons Science of Computer Programming, vol. 2, pp. 241-266, 1982.
[33] E.A. Emerson and C.-L. Lei, Modalities for Model Checking: Branching Time Logic Strikes Back Science of Computer Programming, vol. 8, no. 3, pp. 275-306, 1987.
[34] W. Feller, An Introduction to Probability Theory and Its Applications. John Wiley&Sons, 1968.
[35] B.L. Fox and P.W. Glynn, Computing Poisson Probabilities Comm. ACM, vol. 31, no. 4, pp. 440-445, 1988.
[36] W.K. Grassmann, Finding Transient Solutions in Markovian Event Systems through Randomization Numerical Solution of Markov Chains, pp. 357-371, 1991.
[37] D. Gross and D.R. Miller, The Randomization Technique as a Modeling Tool and Solution Procedure for Transient Markov Chains Operations Research, vol. 32, no. 2, pp. 343-361, 1984.
[38] H. Hansson and B. Jonsson, A Logic for Reasoning about Time and Reliability Formal Aspects of Computing, vol. 6, pp. 512-535, 1994.
[39] B.R. Haverkort, Performance of Computer Communication Systems: A Model-Based Approach. John Wiley&Sons, 1998.
[40] B. Haverkort and H. Hermanns, J.-P. Katoen, On the Use of Model Checking Techniques for Quantitative Dependability Evaluation Proc. IEEE Symp. Reliable Distributed Systems, pp. 228-238, 2000.
[41] H. Hermanns, U. Herzog, and J.-P. Katoen, Process Algebra for Performance Evaluation Theoretical Computer Science, vol. 274, nos. 1-2, pp. 43-87, 2002.
[42] H. Hermanns, U. Herzog, U. Klehmet, V. Mertsiotakis, and M. Siegle, Compositional Performance Modeling with the TIPPtool Performance Evaluation, vol. 39, nos. 1-4, pp. 5-35, 2000.
[43] H. Hermanns, J.-P. Katoen, J. Meyer-Kayser, and M. Siegle, A Markov Chain Model Checker J. Software Tools and Technology Transfer, vol. 4, no. 2, pp. 153-172, 2003.
[44] J. Hillston, A Compositional Approach to Performance Modeling. Cambridge Univ. Press, 1996.
[45] G.J. Holzmann, “The Model Checker SPIN,” IEEE Trans. Software Eng., vol. 23, May 1997.
[46] R.A. Howard, Dynamic Probabilistic Systems: Markov Models, vol. 1. John Wiley&Sons, 1971.
[47] A. Jensen, Markov Chains as an Aid in the Study of Markov Processes Skand. Aktuarietidskrift, vol. 3, pp. 87-91, 1953.
[48] J.-P. Katoen, M.Z. Kwiatkowska, G. Norman, and D. Parker, Faster and Symbolic CTMC Model Checking Process Algebra and Probabilistic Methods, 2001.
[49] J.G. Kemeny and J.L. Snell, Finite Markov Chains. Van Nostrand, 1960.
[50] A.N. Kolmogorov, Über die analytische Methoden in der Wahrscheinlichkeitsrechnung Mathematische Annalen, vol. 104, pp. 415-458, 1931.
[51] A.N. Kolmogorov, Anfangsgründe der Theorie der Markoffschen Ketten mit unendlichen vielen möglichen Zuständen Matematicheskii Sbornik N. S., pp. 607-610, 1936.
[52] U. Krieger, B. Müller-Clostermann, and M. Sczittnick, Modeling and Analysis of Communication Systems Based on Computational Methods for Markov Chains IEEE Trans. Selected Areas in Comm., vol. 8, no. 9, pp. 1630-1648, 1990.
[53] V.G. Kulkarni, Modeling and Analysis of Stochastic Systems. Chapman Hall, 1995.
[54] M.Z. Kwiatkowska, G. Norman, R. Segala, and J. Sproston, Automatic Verification of Real-Time Systems with Discrete Probability Distributions Theoretical Computer Science, vol. 282, no. 1, pp. 101-150, 2002.
[55] K.G. Larsen and A. Skou, Bisimulation through Probabilistic Testing Information and Computation, vol. 94, no. 1, pp. 1-28, 1992.
[56] A.A. Markov, Investigations of an Important Case of Dependent Trials Izvestia Acad., Nauk VI, Series I, vol. 61 (in Russian), 1907.
[57] J.F. Meyer, A. Movaghar, and W.H. Sanders, Stochastic Activity Networks: Structure, Behavior, and Application Proc. Int'l Workshop Timed Petri Nets, pp. 106-115, 1985.
[58] C. Moler and C.F. vanLoan, Nineteen Dubious Ways to Compute the Exponential of a Matrix SIAM Rev., vol. 20, no. 4, pp. 801-835, 1978.
[59] J.K. Muppala and K.S. Trivedi, Numerical Transient Solution of Finite Markovian Queueing Systems Queueing and Related Models, 1992.
[60] W.D. Obal II and W.H. Sanders, State-Space Support for Path-Based Reward Variables Performance Evaluation, vol. 35, pp. 233-251, 1999.
[61] B. Plateau and K. Atif, Stochastic Automata Network for Modeling Parallel Systems IEEE Trans. Software Eng., vol. 17, no. 10, pp. 1093-1108, Oct. 1991.
[62] A. Pnueli and L. Zuck, Probabilistic Verification Information and Computation, vol. 103, pp. 1-29, 1993.
[63] W. Press, B. Flannery, S. Teukolsky, and W. Vetterling, Numerical Recipes in C: The Art of Scientific Computing. Cambridge Univ. Press, 1989.
[64] M.L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming. John Wiley&Sons, 1994.
[65] J.-P. Quielle and J. Sifakis, Specification and Verification of Concurrent Systems in CESAR Proc. Int'l Symp. Programming, 1982.
[66] A.L. Reibman, R. Smith, and K.S. Trivedi, Markov and Markov Reward Models Transient Analysis: An Overview of Numerical Approaches European J. Operational Research, vol. 4, pp. 257-267, 1989.
[67] A.L. Reibman and K.S. Trivedi, Numerical Transient Analysis of Markov Models Computers and Operations Research, vol. 15, no. 1, pp. 19-36, 1988.
[68] W.H. Sanders, W.D. Obal II, M.A. Qureshi, and F.K. Widnajarko, The UltraSAN Modeling Environment Performance Evaluation, vol. 24, pp. 89-115, 1995.
[69] W.J. Stewart, Introduction to the Numerical Solution of Markov Chains. Princeton Univ. Press, 1994.
[70] R.E. Tarjan, Depth-First Search and Linear Graph Algorithms SIAM J. Compting, vol. 1, pp. 146-160, 1972.
[71] M.Y. Vardi, Automatic Verification of Probabilistic Concurrent Finite State Programs Proc. Ann. Symp. Foundations of Computer Science, pp. 327-338, 1985.
[72] H. Younes and R. Simmons, Probabilistic Verification of Discrete Event Systems Using Acceptance Sampling Computer-Aided Verification, 2002.

Index Terms:
Continuous-time Markov chain, lumping, model checking, temporal logic, steady-state analysis, transient analysis, uniformization.
Citation:
Christel Baier, Boudewijn Haverkort, Holger Hermanns, Joost-Pieter Katoen, "Model-Checking Algorithms for Continuous-Time Markov Chains," IEEE Transactions on Software Engineering, vol. 29, no. 6, pp. 524-541, June 2003, doi:10.1109/TSE.2003.1205180
Usage of this product signifies your acceptance of the Terms of Use.