Skip to main content
SpringerLink
Log in

Probabilistic Model Checking: Formalisms and Algorithms for Discrete and Real-time Systems

  • Chapter
Book cover Verification of Digital and Hybrid Systems

Part of the book series: NATO ASI Series ((NATO ASI F,volume 170))

Abstract

This paper considers the problem of verification of probabilistic Systems, for both the discrete- and real-time cases. Probabilistic Systems are modeled as Markov chains, concurrent Markov chains (i.e. MCs with non-determinism) or, in the real-time case, generalized semi-Markov processes (Markovian processes with time delays on events). Discrete-time specifications are described in the logics PTL (propositional temporal logic), ETL (extended temporal logic) or PCTL* (probabilistic full computation tree logic), or as Bèchi automata. Real-time specifications are described either in TCTL (timed computation tree logic) or as deterministic timed Muller automata. The problems considered are either the probabilistic satisfaction of a specification by a system (i.e., satisfaction with probability one) or the computation of the satisfaction probability. We give complexity results for the above problems and present some of the corresponding algorithms. Finally, we illustrate the approach with some examples.

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 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.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. C. Courcoubetis and M. Yannakakis. Verifying temporal properties of finite-state probabilistic programs. In Proc. of 29th FOCS, Berkeley, October 1988.

    Google Scholar 

  2. C. Courcoubetis and M. Yannakakis. The complexity of probabilistic verification. Journal of the ACM, 42(4):857–907, July 1995.

    Article  MathSciNet  MATH  Google Scholar 

  3. R. Alur, C. Courcoubetis, and D. Dill. Model-checking for probabilistic real-time systems. In Proceedings of the 18th IC ALP, pages 115–126, Madrid, July 1991.

    Google Scholar 

  4. R. Alur, C. Courcoubetis, and D. Dill. Verifying automata specifications of probabilistic real-time systems. In Proceedings of the REX Workshop “Real-Time: Theory in Practice”, LNCS, volume 600, Berlin, June 1991. Springer-Verlag.

    Google Scholar 

  5. A. Pnueli. The temporal logic of concurrent programs. Theoretical Computer Science, 13:45–60, 1981.

    MathSciNet  MATH  Google Scholar 

  6. R. Buchi. On a decision method in restricted second order arithmetic. In Proc. Int. Congr. Logic, Method and Philos. Sciences. Stanford U. Press, 1962.

    Google Scholar 

  7. P. Wolper. Temporal logic can be more expressive. Information and Control, pages 72–99, 1983.

    Google Scholar 

  8. H. Hansson and B. Jonsson. A framework for reasoning about time and reliability. In Proc. of the 10th IEEE Real-Time Systems Symposium, 1989.

    Google Scholar 

  9. A. Aziz, V . Singhar, F. Balarin, R.K. Brayton, and A.L. Sangiovanni-Vincetelli. It usually works: the temporal logic of stochastic Systems. In Computer-Aided Verification. LNCS 939, 1995.

    Google Scholar 

  10. G.S. Shedler. Regeneration and Networks of Queues. Spinger-Verlag, 1987.

    Book  MATH  Google Scholar 

  11. W. Whitt. Continuity of generalized semi-Markov processes. Math. Oper. Res.,5, 1980.

    Google Scholar 

  12. R. Alur, C. Courcoubetis, and D.L. Dill. Model checking in dense real time.Information and Computation, 104(1):2–34, 1993.

    Article  MathSciNet  MATH  Google Scholar 

  13. D. Lehman and S. Shelah. Reasoning with time and chance. Information and Control, 53(3):165–198

    Article  MathSciNet  Google Scholar 

  14. A. Pnueli. On the extremely fair treatment of probabilistic algorithms. In Proc. 15th Symp. Theory of Computation, 1983.

    Google Scholar 

  15. S. Hart and M. Sharir. Probabilistic temporal logic for finite and bounded models. In Proc. 16th Symp. Theory of Computation, 1984.

    Google Scholar 

  16. M. Vardi. Automatic verification of probabilistic concurrent finite-state programs. In Proc. 26th IEEE Symp. on Foundations of Computer Science, pages 327–338, Portland, October 1985.

    Google Scholar 

  17. A. Pnueli and L. Zuck. Probabilistic verification by tableaux. In Proc. 1st Symp. on Logic in Computer Science, pages 322–331, Cambridge, June 1986.

    Google Scholar 

  18. H. Hansson and B. Jonsson. A logic for reasoning about time and reliability. Formal Aspects of Computing, 6(5):512–535, 1994.

    Article  MATH  Google Scholar 

  19. C. Courcoubetis and M. Yannakakis. Markov decision processes and regular events. In Proc. llth Int. Coli, on Automata Languages and Programming, volume 443, Coventry, July 1990. Lecture Notes in Computer Science, Springer-Verlag.

    Google Scholar 

  20. A. Bianco and L. de Alfaro. Model checking of probabilistic and nondeterministic systems. In Found. of Software Tech, and Theor. Comp. Sei. LNCS 1026, 1995.

    Google Scholar 

  21. L. de Alfaro. Formal verification of Performance and reliability of real-time Systems. Technical Report STAN-CS-TR-96-1571, Stanford University, 1996.

    Google Scholar 

  22. R. Segala. Modeling and verification of randomized distributed real-time Systems. PhD thesis, MIT, 1995.

    Google Scholar 

  23. R. Segala and N. Lynch. Probabilistic simulations for probabilistic processes. In CONCUR ’94, 1994.

    Google Scholar 

  24. S. Gilmore and J. Hillston. The PEPA workbench: a tool to support a process-algebra based approach to Performance modeling. In Conf. on modeling techniques and tools for Computer Performance evaluation, 1994.

    Google Scholar 

  25. H. Hermanns, V. Mertsiotakis, and M. Rettelbach. A construction and analysis tool based on the stochastic process-algebra TIPP. In TACAS ’96, 1996.

    Google Scholar 

  26. M. Bernardo, L. Donatiello, and R. Gorrieri. A tutorial on EMPA: a theory of concurrent processes with nondeterminism, priorities, probabilities and time. Theor. Comp. Sei., 1997. To appear.

    Google Scholar 

  27. L. Breiman. Probability. Addison-Wesley, 1968.

    MATH  Google Scholar 

  28. J.G. Kemeny, J.L. Snell, and A.W. Knapp. Denumerable Markov Chains. Spinger-Verlag, 1976.

    MATH  Google Scholar 

  29. W.J. Stewart. Numerical Solution of Markov Chains. Princeton University Press, 1994.

    MATH  Google Scholar 

  30. M. Rabin. On the advantage of free choice: A symmetric and fully distributed Solution to the dining philosophers problem. In Proc. of the 8th ACM Symposium on Principles of Programming Languages, 1981.

    Google Scholar 

  31. R. Tarjan. Depth first search and linear graph algorithms. SIAM Journal on Computing, 1(2):146–170, 1972.

    Article  MathSciNet  MATH  Google Scholar 

  32. A. Aho, J. Hopcroft, and J. Ullman. The Design and Analysis of Computer Algorithms. Addison Wesley, 1974.

    MATH  Google Scholar 

  33. A.K. Chandra, D.C. Kozen, and L.J. Stockmeyer. Alternation. Journal of the ACM, 28(1):114–133, January 1981.

    Article  MathSciNet  MATH  Google Scholar 

  34. M.Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proc. Symp. on Logic in Computer Science, pages 322–331, Cambridge, june 1986.

    Google Scholar 

  35. A.P. Sistla, M.Y. Vardi, and P. Wolper. The complementation problem for Büchi automata with applications to temporal logic. Theoretical Computer Science, 49:217–237, 1987.

    Article  MathSciNet  MATH  Google Scholar 

  36. E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite-state concurrent Systems using temporal logic specifications. ACM TOPLAS, 8(2), 1986.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Université de Joseph Fourier And VERIMAG Centre Equation 2, Rue Vignate, 38610, Gières, France

    Costas Courcoubetis

  2. Computer Science Department, University of Crete and Institute of Computer Science Foundation Research and Technology, 1385, 71110, Heraklion, Greece

    Stavros Tripakis

Authors
  1. Costas Courcoubetis
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Stavros Tripakis
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Faculty of Engineering and Natural Sciences , Sabanci University, Orhanli, 81474, Tuzla-Istanbul, Turkey

    M. Kemal Inan

  2. Bell Laboratories, 600 Mountain Avenue, 2A-410 Murray Hill, 07974, NJ, USA

    Robert P. Kurshan

Rights and permissions

Reprints and permissions

Copyright information

© 2000 Springer-Verlag Berlin Heidelberg New York

About this chapter

Cite this chapter

Courcoubetis, C., Tripakis, S. (2000). Probabilistic Model Checking: Formalisms and Algorithms for Discrete and Real-time Systems. In: Inan, M.K., Kurshan, R.P. (eds) Verification of Digital and Hybrid Systems. NATO ASI Series, vol 170. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-59615-5_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-59615-5_10

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-64052-0

  • Online ISBN: 978-3-642-59615-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation