Beyond Memoryless Distributions: Model Checking Semi-Markov Chains

  • Gabriel G. Infante López
  • Holger Hermanns
  • Joost-Pieter Katoen
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2165)


Recent investigations have shown that the automated verification of continuous-time Markov chains (CTMCs) against CSL (Continuous Stochastic Logic) can be performed in a rather efficient manner. The state holding time distributions in CTMCs are restricted to negative exponential distributions. This paper investigates model checking of semi-Markov chains (SMCs), a model in which state holding times are governed by general distributions. We report on the semantical issues of adopting CSL for specifying properties of SMCs and present model checking algorithms for this logic.


Model Check General Distribution Model Check Algorithm Negative Exponential Distribution Duration Calculus 
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, C. Courcoubetis and D. Dill. Model-checking in dense real-time. Inf. and Comp., 104: 2–34, 1993.zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    S. Asmussen, O. Nermand and M. Olsson. Fitting phase-type distributions via the EM algorithm. Scand. J. Statist., 23: 420–441, 1996.Google Scholar
  3. 3.
    A. Aziz, K. Sanwal, V. Singhal and R. Brayton. Verifying continuous time Markov chains. In R. Alur and T.A. Henzinger (eds), Computer-Aided Verification, LNCS 1102, pp. 269–276, Springer, 1996.Google Scholar
  4. 4.
    A. Aziz, K. Sanwal, V. Singhal and R. Brayton. Model checking continuous time Markov chains. ACM Trans. on Computational Logic, 1(1): 162–170, 2000.CrossRefMathSciNetGoogle Scholar
  5. 5.
    C. Baier, J.-P. Katoen and H. Hermanns. Approximate symbolic model checking of continuous-time Markov chains. In J.C.M. Baeten and S. Mauw (eds), Concurrency Theory, LNCS 1664, pp. 146–162, Springer, 1999.CrossRefGoogle Scholar
  6. 6.
    C. Baier, B. R. Haverkort, H. Hermanns and J.-P. Katoen. Model checking continuous-time Markov chains by transient analysis. In E.A Emerson and A.P. Sistla (eds), Computer Aided Verification, LNCS 1855, pp. 358–372, Springer, 2000.CrossRefGoogle Scholar
  7. 7.
    H. Brunner and P. van der Houwen, The Numerical Solution of Volterra Equations. North Holland, 1986.Google Scholar
  8. 8.
    E. Cinlar. Introduction to Stochastic Processes. Prentice-Hall Inc., 1975.Google Scholar
  9. 9.
    E. Clarke, E. Emerson and A. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8: 244–263, 1986.zbMATHCrossRefGoogle Scholar
  10. 10.
    M.E. Crovella. Performance evaluation with heavy tailed distributions (extended abstract). In B. Haverkort, H. Bohnenkamp and C. Smith (eds), Computer Performance Evaluation, LNCS 1786, pp. 1–9, Springer, 2000.Google Scholar
  11. 11.
    P.R. D’Argenio, J.-P. Katoen and E. Brinksma. An algebraic approach to the specification of stochastic systems (extended abstract). In D. Gries and W.-P. de Roever (eds), Programming Concepts and Methods. Chapman & Hall, pp. 126–147, 1998.Google Scholar
  12. 12.
    L. de Alfaro. Formal Verification of Probabilistic Systems. PhD thesis, Stanford University, 1997.Google Scholar
  13. 13.
    A. Feyzi Ates, M. Bilgic, S. Saito, and B. Sarikaya. Using timed CSP for specification, verification and simulation of multimedia synchronization. IEEE J. on Sel. Areas in Comm., 14:126–137, 1996.CrossRefGoogle Scholar
  14. 14.
    R. German Performance Analysis of Communication Systems: Modeling with Non-Markovian Stochastic Petri Nets. John Wiley & Sons, 2000.Google Scholar
  15. 15.
    R. German, D. Logothe, and K.S. Trivedi. Transient analysis of Markov regenerative stochastic Petri nets: A comparison of approaches. Proc. 6th Int. Workshop on Petri Nets and Performance Models, pages 103–112, IEEE CS Press, 1995.Google Scholar
  16. 16.
    H. Hansson and B. Jonsson. A logic for reasoning about time and reliability. Formal Aspects of Computing 6: 512–535, 1994.zbMATHCrossRefGoogle Scholar
  17. 17.
    D. Van Hung and Z. Chaochen. Probabilistic duration calculus for continuous time. Formal Aspects of Computing, 11: 21–44, 1999.zbMATHCrossRefGoogle Scholar
  18. 18.
    V. Kulkarni. Modeling and Analysis of Stochastic Systems. Chapman & Hall, 1995.Google Scholar
  19. 19.
    M.Z. Kwiatkowska, G. Norman, R. Segala, and J. Sproston. Verifying quantitative properties of continuous probabilistic timed automata. In C. Palamadessi (ed), Concurrency Theory, LNCS 1877, pp. 123–137, Springer, 2000.Google Scholar
  20. 20.
    W. Nelson. Weibull analysis of reliability data with few or no failures. Journal of Quality Technology 17(3), 140–146, 1985.Google Scholar
  21. 21.
    A.D. Swain and H.E. Guttmann. Handbook of human reliability analysis with emphasis on nuclear power plant applications-final report. Technical Report NRC FIN A 1188 NUREG/CR-1278 SAND80-0200, US Nuclear Regulatory Commission, 1983.Google Scholar
  22. 22.
    R.E. Tarjan. Depth-first search and linear graph algorithms. SIAM Journal of Computing, 1: 146–160, 1972.zbMATHCrossRefMathSciNetGoogle Scholar
  23. 23.
    H. Taylor and S. Karlin. An Introduction To Stochastic Modeling. Academic Press, 1998.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Gabriel G. Infante López
    • 1
  • Holger Hermanns
    • 1
  • Joost-Pieter Katoen
    • 1
  1. 1.Formal Methods and Tools Group, Faculty of Computer ScienceUniversity of TwenteAE EnschedeThe Netherlands

Personalised recommendations