Skip to main content
SpringerLink
Log in

Model Checking Markov Chains Using Krylov Subspace Methods: An Experience Report

  • Conference paper
Computer Performance Engineering (EPEW 2010)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 6342))

Included in the following conference series:

Abstract

The predominant technique for computing the transient distribution of a Continuous Time Markov Chain (CTMC) exploits uniformization, which is known to be stable and efficient for non-stiff to mildly-stiff CTMCs. On stiff CTMCs however, uniformization suffers from severe performance degradation. In this paper, we report on our observations and analysis of an alternative technique using Krylov subspaces. We implemented a Krylov-based extension to MRMC (Markov Reward Model Checker) and conducted extensive experiments on five case studies from different application domains. The results reveal that the Krylov-based technique is an order of magnitude faster on stiff CTMCs.

Funded by ESA/ESTEC under Contract No. 21171/07/NL/JD.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abdallah, H., Marie, R.: The uniformized power method for transient solutions of Markov processes. Computers & Operations Research 20(5), 515–526 (1993)

    Article  MATH  Google Scholar 

  2. Baier, C., Haverkort, B., Hermanns, H., Katoen, J.-P.: Model-checking algorithms for continuous-time Markov chains. IEEE Trans. on Softw. Eng. 29(6), 524–541 (2003)

    Article  MATH  Google Scholar 

  3. Bosnacki, D., Edelkamp, S., Sulewski, D.: Efficient probabilistic model checking on general purpose graphics processors. In: Păsăreanu, C.S. (ed.) SPIN Workshop. LNCS, vol. 5578, pp. 32–49. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  4. Busch, H., Sandmann, W., Wolf, V.: A numerical aggregation algorithm for the enzyme-catalyzed substrate conversion. In: Priami, C. (ed.) CMSB 2006. LNCS (LNBI), vol. 4210, pp. 298–311. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  5. Carrasco, J.A.: Transient analysis of rewarded continuous time Markov models by regenerative randomization with laplace transform inversion. The Conputer Journal 46(1), 84–99 (2003)

    MathSciNet  MATH  Google Scholar 

  6. Chen, T., Han, T., Katoen, J.-P., Mereacre, A.: Quantitative model checking of continuous-time Markov chains against timed automata specification. In: LICS, pp. 309–318 (2009)

    Google Scholar 

  7. de Souza e Silva, E., Gail, H.R.: Transient solutions for Markov chains. In: Grassmann, W. (ed.) Computational Probability, pp. 43–81. Kluwer Academic Publishers, Dordrecht (2000)

    Chapter  Google Scholar 

  8. Duff, I., Grimes, R., Lewis, J.: User’s guide for the Harwell-Boeing sparse matrix collection. Technical Report TR/PA/92/86, CERFACS (1992)

    Google Scholar 

  9. Fox, B.L., Glynn, P.W.: Computing Poisson probabilities. Commun. ACM 31(4), 440–445 (1988)

    Article  MathSciNet  Google Scholar 

  10. Garren, S.T., Smith, R.L.: Estimating the second largest eigenvalue of a Markov transition matrix. Bernoulli 6(2), 215–242 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  11. Henzinger, T.A., Mateescu, M., Wolf, V.: Sliding window abstraction for infinite Markov chains. In: Bouajjani, A., Maler, O. (eds.) Computer Aided Verification. LNCS, vol. 5643, pp. 337–352. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  12. Hermanns, H., Meyer-Kayser, J., Siegle, M.: Multi terminal binary decision diagrams to represent and analyse continuous time Markov chains. In: Plateau, B., Stewart, W., Silva, M. (eds.) Proc. 3rd International Workshop on Numerical Solution of Markov Chains (NSMC 1999), pp. 188–207. Prensas Universitarias de Zaragoza (1999)

    Google Scholar 

  13. Hochbruck, M., Lubich, C.: On Krylov subspace approximations to the matrix exponential operator. SIAM on Numerical Analysis 34(5), 1911–1925 (1997)

    Article  MathSciNet  MATH  Google Scholar 

  14. Horn, R.A., Johnson, C.R.: Topics in Matrix Analysis. Cambridge University Press, Cambridge (1986)

    MATH  Google Scholar 

  15. Ibe, O., Trivedi, K.: Stochastic Petri net models of polling systems. IEEE Journal on Selected Areas in Communications 8(9), 1649–1657 (1990)

    Article  Google Scholar 

  16. Jensen, A.: Markoff chains as an aid in the study of markoff processes. In: Skand. Aktuarietidskrift, vol. 36, pp. 87–91 (1953)

    Google Scholar 

  17. Katoen, J.-P., Zapreev, I.S.: Safe on-the-fly steady-state detection for time-bounded reachability. In: QEST, pp. 301–310. IEEE CS, Los Alamitos (2006)

    Google Scholar 

  18. Katoen, J.-P., Zapreev, I.S., Hahn, E.M., Hermanns, H., Jansen, D.N.: The ins and outs of the probabilistic model checker MRMC. In: Quantitative Evaluation of Systems, pp. 167–176. IEEE CS Press, Los Alamitos (2009)

    Google Scholar 

  19. Kwiatkowska, M., Norman, G., Parker, D.: Symmetry reduction for probabilistic model checking. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 234–248. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  20. Massink, M., Katoen, J.-P., Latella, D.: Model checking dependability attributes of wireless group communication. In: Dependable Systems and Networks (DSN), pp. 711–720. IEEE CS Press, Los Alamitos (2004)

    Google Scholar 

  21. Moler, C., Van Loan, C.: Nineteen dubious ways to compute the exponential of a matrix, twenty-five years later. SIAM Review 45(1), 3–49 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  22. Rinehart, R.F.: The equivalence of definitions of a matrix function. The American Mathematical Monthly 62(6), 395–414 (1955)

    Article  MathSciNet  MATH  Google Scholar 

  23. Saad, Y.: Analysis of some Krylov subspace approximations to the matrix exponential operator. SIAM Journal on Numerical Analysis 29(1), 209–228 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  24. Sidje, R.: Expokit: a software package for computing matrix exponentials. ACM Trans. Math. Softw. 24(1), 130–156 (1998)

    Article  MATH  Google Scholar 

  25. Sidje, R., Stewart, W.J.: A survey of methods for computing large sparse matrix exponentials arising in Markov chains. Markov Chains, Computational Statistics and Data Analysis 29, 345–368 (1996)

    Article  MATH  Google Scholar 

  26. Trefethen, L.N., Bau III, D.: Numerical Linear Algebra. Society for Industrial and Applied Mathematics, Philadelphia (1997)

    Book  MATH  Google Scholar 

  27. van Moorsel, A., Sanders, W.: Adaptive uniformization. Communications in Statistics - Stochastic Models 10(3), 619–648 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  28. Ward, R.C.: Numerical computation of the matrix exponential with accuracy estimate. SIAM Journal on Numerical Analysis 14(4), 600–610 (1977)

    Article  MathSciNet  MATH  Google Scholar 

  29. Weiss, R.: Error-minimizing Krylov subspace methods. SIAM Journal on Scientific Computing 15(3), 511–527 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  30. Zapreev, I.S.: Model Checking Markov Chains: Techniques and Tools. PhD thesis, Univ. of Twente (2008)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Software Modeling and Verification Group, RWTH Aachen University, Germany

    Falko Dulat, Joost-Pieter Katoen & Viet Yen Nguyen

Authors
  1. Falko Dulat
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Joost-Pieter Katoen
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Viet Yen Nguyen
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Dipartimento di Matematica, Fisica e Chimica, Università di Urbino “Carlo Bo”, Piazza della Repubblica 13, 61029, Urbino, Italy

    Alessandro Aldini  & Marco Bernardo  & 

  2. Dipartimento di Scienze dell’Informazione, Universit di Bologna, Mura Anteo Zamboni 7, 40126, Bologna, Italy

    Luciano Bononi

  3. Dipartimento di Informatica, Universit dell’Aquila, Via Vetoio, Coppito, 67100, L’Aquila, Italy

    Vittorio Cortellessa

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Dulat, F., Katoen, JP., Nguyen, V.Y. (2010). Model Checking Markov Chains Using Krylov Subspace Methods: An Experience Report. In: Aldini, A., Bernardo, M., Bononi, L., Cortellessa, V. (eds) Computer Performance Engineering. EPEW 2010. Lecture Notes in Computer Science, vol 6342. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15784-4_8

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-15784-4_8

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-15783-7

  • Online ISBN: 978-3-642-15784-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation