Model Checking Infinite-State Markov Chains

  • Anne Remke
  • Boudewijn R. Haverkort
  • Lucia Cloth
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3440)


In this paper algorithms for model checking CSL (continuous stochastic logic) against infinite-state continuous-time Markov chains of so-called quasi birth-death type are developed. In doing so we extend the applicability of CSL model checking beyond the recently proposed case for finite-state continuous-time Markov chains, to an important class of infinite-state Markov chains. We present syntax and semantics for CSL and develop efficient model checking algorithms for the steady-state operator and the time-bounded next and until operator. For the former, we rely on the so-called matrix-geometric solution of the steady-state probabilities of the infinite-state Markov chain. For the time-bounded until operator we develop a new algorithm for the transient analysis of infinite-state Markov chains, thereby exploiting the quasi birth-death structure. A case study shows the feasibility of our approach.


  1. 1.
    Abdulla, P., Jonsson, B., Nilsson, M., Saksena, M.: A survey of regular model checking. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 35–48. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  2. 2.
    Aziz, A., Sanwal, K., Brayton, R.: Model checking continuous-time Markov chains. ACM Transactions on Computational Logic 1(1), 162–170 (2000)CrossRefMathSciNetGoogle Scholar
  3. 3.
    Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P.: On the logical characterisation of performability properties. In: Welzl, E., Montanari, U., Rolim, J.D.P. (eds.) ICALP 2000. LNCS, vol. 1853, pp. 780–792. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  4. 4.
    Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P.: Model-checking algorithms for continuous-time Markov chains. IEEE Transactions on Software Engineering 29(7), 524–541 (2003)CrossRefGoogle Scholar
  5. 5.
    Bell, A.: Distributed evaluation of stochasic Petri nets. PhD thesis, Dept. of Computer Science, RWTH Aachen (2004)Google Scholar
  6. 6.
    Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specification for finite-state verification. In: Proc. 21st Int. Conf. on Software Engineering, pp. 411–420. IEEE CS Press, Los Alamitos (1999)CrossRefGoogle Scholar
  7. 7.
    El-Rayes, A., Kwiatkowska, M., Norman, G.: Solving infinite stochastic process algebra models through matrix-geometric methods. In: Proc. 7th Process Algebras and Performance Modelling Workshop (PAPM 1999), pp. 41–62. University of Zaragoza (1999)Google Scholar
  8. 8.
    Gross, D., Miller, D.R.: The randomization technique as a modeling tool and solution procedure for transient Markov processes. Operations Research 32(2), 343–361 (1984)zbMATHCrossRefMathSciNetGoogle Scholar
  9. 9.
    Haverkort, B.R.: Performance of Computer Communication Systems. John Wiley & Sons, Chichester (1998)CrossRefGoogle Scholar
  10. 10.
    Haverkort, B.R., Hermanns, H., Katoen, J.-P.: On the use of model checking techniques for dependability evaluation. In: Proc. 19th IEEE Symposium on Reliable Distributed Systems (SRDS 2000), pp. 228–237. IEEE CS Press, Los Alamitos (2000)CrossRefGoogle Scholar
  11. 11.
    Hermanns, H., Katoen, J.-P., Meyer-Kayser, J., Siegle, M.: A tool for model-checking Markov chains. International Journal on Software Tools for Technology Transfer 4(2), 153–172 (2003)CrossRefGoogle Scholar
  12. 12.
    Katoen, J.-P.: Concepts, Algorithms, and Tools for Model Checking. In: Arbeitsberichte des IMMD, vol. 32(1), Friedrich-Alexander Universität Erlangen Nürnberg (June 1999)Google Scholar
  13. 13.
    Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic symbolic model checking with PRISM: a hybrid approach. International Journal on Software Tools for Technology Transfer 6(2), 128–142 (2004)CrossRefGoogle Scholar
  14. 14.
    Latouche, G., Ramaswami, V.: A logarithmic reduction algorithm for quasi birth and death processes. Journal of Applied Probability 30, 650–674 (1993)zbMATHCrossRefMathSciNetGoogle Scholar
  15. 15.
    Mitrani, I., Ost, A., Rettelbach, M.: TIPP and the spectral expansion method. In: Baccelli, F., Jean-Marie, A., Mitrani, I. (eds.) Quantitative Models in Parallel Systems, pp. 99–113. Springer, Heidelberg (1995)Google Scholar
  16. 16.
    Neuts, M.F.: Matrix Geometric Solutions in Stochastic Models: An Algorithmic Approach. Johns Hopkins University Press, Baltimore (1981)zbMATHGoogle Scholar
  17. 17.
    Ost, A.: Performance of Communication Systems. A Model-Based Approach with Matrix-Geometric Methods. PhD thesis, Dept. of Computer Science, RWTH Aachen (2001)Google Scholar
  18. 18.
    Remke, A.: Model Checking Quasi Birth Death Processes. Master’s thesis, Dept. of Computer Science, RWTH Aachen (2004),
  19. 19.
    Schnoebelen, P.: The verification of probabilistic lossy channel systems. In: Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P., Siegle, M. (eds.) Validation of Stochastic Systems. LNCS, vol. 2925, pp. 445–465. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  20. 20.
    Zhang, J., Coyle, E.J.: Transient analysis of quasi-birth-death processes. Stochastic Models 5(3), 459–496 (1989)zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Anne Remke
    • 1
  • Boudewijn R. Haverkort
    • 1
  • Lucia Cloth
    • 1
  1. 1.Faculty for Electrical Engineering, Mathematics and Computer ScienceUniversity of Twente 

Personalised recommendations