Faster and Symbolic CTMC Model Checking

  • Joost-Pieter Katoen
  • Marta Kwiatkowska
  • Gethin Norman
  • David Parker
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2165)


This paper reports on the implementation and the experiments with symbolic model checking of continuous-time Markov chains using multi-terminal binary decision diagrams (MTBDDs). Properties are expressed in Continuous Stochastic Logic (CSL) [7] which includes the means to express both transient and steady-state performance measures. We show that all CSL operators can be treated using standard operations on MTBDDs, thus allowing a rather straightforward implementation of symbolic CSL model checking on existing MTBDD-based platforms such as the verifier PRISM. The main result of the paper is an improvement of O(N) in the time complexity of checking time-bounded until-formulas, where N is the number of states in the CTMC under consideration. This result yields a drastic speed-up in the verification time of model checking CTMCs, both in the symbolic and non-symbolic case.


Model Check Polling System Transient Analysis Atomic Proposition Terminal Vertex 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    R. Alur and T.A. Henzinger. Reactive modules. In IEEE Symp. on Logic in Computer Science, 207–218, 1996.Google Scholar
  2. 2.
    A. Aziz, K. Sanwal, V. Singhal and R. Brayton. Verifying continuous time Markov chains. In Computer-Aided Verification, LNCS 1102: 269–276, 1996.Google Scholar
  3. 3.
    A. Aziz, K. Sanwal, V. Singhal and R. Brayton. Model checking continuous time Markov chains. ACMT rans. on Computational Logic, 1(1): 162–170, 2000.CrossRefMathSciNetGoogle Scholar
  4. 4.
    R.I. Bahar, E.A. Frohm, C.M. Gaona, G.D. Hachtel, E. Macii, A. Pardo and F. Somenzi. Algebraic decision diagrams and their applications. Formal Methods in System Design, 10(2/3): 171–206, 1997.CrossRefGoogle Scholar
  5. 5.
    C. Baier, E. Clarke, V. Hartonas-Garmhausen, M. Kwiatkowska, and M. Ryan. Symbolic model checking for probabilistic processes. In Automata, Languages and Programming, LNCS 1256: 430–440, 1997.Google Scholar
  6. 6.
    C. Baier, B.R. Haverkort, H. Hermanns and J.-P. Katoen. Model checking continuous-time Markov chains by transient analysis. In Computer Aided Verification, LNCS 1855: 358–372, 2000.CrossRefGoogle Scholar
  7. 7.
    C. Baier, J.-P. Katoen and H. Hermanns. Approximate symbolic model checking of continuous-time Markov chains. In Concurrency Theory, LNCS 1664: 146–162, 1999.CrossRefGoogle Scholar
  8. 8.
    C. Baier and M. Kwiatkowska. Model checking for a probabilistic branching-time logic with fairness. Distr. Comp., 11(3): 125–155, 1998.CrossRefGoogle Scholar
  9. 9.
    A. Bianco and L. de Alfaro. Model checking of probabilistic and nondeterministic systems. In Found. of Softw. Techn. and Th. Comp. Sc., LNCS 1026: 499–513, 1995.Google Scholar
  10. 10.
    K. Brace, R. Rudell and R. Bryant. Efficient implementation of a BDD package. In: 27th ACM/IEEE Design Automation Conference, 1990.Google Scholar
  11. 11.
    E. Clarke, E. Emerson and A. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACMT rans. on Progr. Lang. and Sys., 8: 244–263, 1986.zbMATHCrossRefGoogle Scholar
  12. 12.
    E. Clarke, M. Fujita, P.C. McGeer and J.C-Y. Yang. Multi-terminal binary decision diagrams: an efficient data structure for matrix representation. In Formal Methods in System Design, 10(2/3): 149–169, 1997.CrossRefGoogle Scholar
  13. 13.
    E. Clarke, O. Grumberg and D. Long. Verification tools for finite-state concurrent programs. In A Decade of Concurrency, LNCS 803: 124–175, 1993.Google Scholar
  14. 14.
    L. de Alfaro, M. Kwiatkowska, G. Norman, D. Parker and R. Segala. Symbolic model checking for probabilistic processes using MTBDDs and the Kronecker representation. In Tools and Algorithms for the Analysis and Construction of Systems, LNCS 1785: 395–410, 2000.CrossRefGoogle Scholar
  15. 15.
    B.L. Fox and P.W. Glynn. Computing Poisson probabilities. Comm. of the ACM, 31(4): 440–445, 1988.CrossRefMathSciNetGoogle Scholar
  16. 16.
    D. Gross and D.R. Miller. The randomization technique as a modeling tool and solution procedure for transient Markov chains. Oper. Res. 32(2): 343–361, 1984.zbMATHMathSciNetCrossRefGoogle Scholar
  17. 17.
    H.A. Hansson and B. Jonsson. A logic for reasoning about time and reliability. Form. Asp. of Comp., 6(5): 512–535, 1994.zbMATHCrossRefGoogle Scholar
  18. 18.
    V. Hartonas-Garmhausen, S. Campos and E.M. Clarke. ProbVerus: probabilistic symbolic model checking. In Formal Methods for Real-Time and Prob. Sys., LNCS 1601: 96–111, 1999.CrossRefGoogle Scholar
  19. 19.
    H. Hermanns, J.-P. Katoen, J. Meyer-Kayser and M. Siegle. A Markov chain model checker. In Tools and Algorithms for the Construction and Analysis of Systems, LNCS 1785: 347–362, 2000.CrossRefGoogle Scholar
  20. 20.
    H. Hermanns, J. Meyer-Kayser and M. Siegle. Multi-terminal binary decision diagrams to represent and analyse continuous-time Markov chains. In Proc. 3rd Int. Workshop on the Num. Sol. of Markov Chains, pp. 188–207, 1999.Google Scholar
  21. 21.
    O.C. Ibe and K.S. Trivedi. Stochastic Petri net models of polling systems. IEEE J. on Sel. Areas in Comms., 8(9): 1649–1657, 1990.CrossRefGoogle Scholar
  22. 22.
    J. Kemeny, J. Snell and A. Knapp. Denumerable Markov Chains. Van Nostrand, 1966.Google Scholar
  23. 23.
    A. Jensen. Markov chains as an aid in the study of Markov processes. Skand. Aktuarietidskrift, 3: 87–91, 1953.Google Scholar
  24. 24.
    J.K. Muppala and K.S. Trivedi. Numerical transient solution of finite Markovian queueing systems. In U. Bhat, ed, Queueing and Related Models, Oxford University Press, 1992.Google Scholar
  25. 25.
    W.D. Obal II and W.H. Sanders. State-space support for path-based reward variables. Perf. Ev., 35: 233–251, 1999.zbMATHCrossRefGoogle Scholar
  26. 26.
    D. Parker. Implementation of symbolic model checking for probabilistic systems. Ph.D thesis, School of Computer Science, University of Birmingham, 2001 (to appear).Google Scholar
  27. 27.
    F. Somenzi. CUDD: CU decision diagram package. Public software, Colorado University, Boulder, 1997.Google Scholar
  28. 28.
    W. Stewart. Introduction to the Numerical Solution of Markov Chains. Princeton Univ. Press, 1994.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Joost-Pieter Katoen
    • 1
  • Marta Kwiatkowska
    • 2
  • Gethin Norman
    • 2
  • David Parker
    • 2
  1. 1.Formal Methods and Tools Group, Faculty of Computer ScienceUniversity of TwenteAE EnschedeThe Netherlands
  2. 2.School of Computer ScienceUniversity of BirminghamEdgbaston, BirminghamUK

Personalised recommendations