Reachability Analysis of Probabilistic Systems by Successive Refinements

  • Pedro R. D’Argenio
  • Bertrand Jeannet
  • Henrik E. Jensen
  • Kim G. Larsen
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2165)


We report on a novel development to model check quantitative reachability properties on Markov decision processes together with its prototype implementation. The innovation of the technique is that the analysis is performed on an abstraction of the model under analysis. Such an abstraction is significantly smaller than the original model and may safely refute or accept the required property. Otherwise, the abstraction is refined and the process repeated. As the numerical analysis necessary to determine the validity of the property is more costly than the refinement process, the technique profits from applying such numerical analysis on smaller state spaces.


Model Check Markov Decision Process Simple Path Reachable State Reachability Analysis 
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, N. Halbwachs, D. Dill, and H. Wong-Toi. Minimization of timed transition systems. In R. Cleaveland, ed., Procs. of CONCUR 92, Stony Brook, NY, LNCS 630, pp. 340–354. Springer, 1992.Google Scholar
  2. 2.
    A. Aziz, V. Singhal, F. Balarin, R.K. Bryton, and A.L. Sangiovanni-Vincentelli. It usually works:the temporal logics of stochastic systems. In P. Wolper, ed., Procs. of the 7th CAV, Liège, LNCS 939, pp. 155–165. Springer, 1995.Google Scholar
  3. 3.
    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
  4. 4.
    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., Procs. of CONCUR 99, Eindhoven, LNCS 1664, pp. 146–161. Springer, 1999.Google Scholar
  5. 5.
    A. Bianco and L. de Alfaro. Model checking of probabilistic and non-deterministic systems. In Procs. 15 th FSTTCS, Pune, LNCS 1026, pp. 499–513. Springer, 1995.Google Scholar
  6. 6.
    A. Bouajjani, J. C. Fernandez, N. Halbwachs, P. Raymond, and C. Ratel. Minimal state graph generation. Science of Computer Programming, 18:247–269, 1992.zbMATHCrossRefMathSciNetGoogle Scholar
  7. 7.
    P.R. D’Argenio, J.-P. Katoen, T.C. Ruys, and J. Tretmans. The bounded retransmission protocol must be on time! In E. Brinksma, ed., Procs. of the 3rd TACAS, Enschede, LNCS 1217, pp. 416–431. Springer, 1997.Google Scholar
  8. 8.
    P.R. D’Argenio, B. Jeannet, H.E. Jensen, and K.G. Larsen. Reachability Analysis of Probabilistic Systems by Successive Refinements. CTIT Technical Report, 2001. To appear.Google Scholar
  9. 9.
    L. de Alfaro, M. Kwiatkowska, G. Norman, D. Parker, and R. Segala. Symbolic model checking of concurrent probabilistic processes using MTBDDs and the Kronecker representation. In Graf and Schwartzbach [11].Google Scholar
  10. 10.
    M. Fujita, P.C. McGeer, and J.C.-Y. Yang. Multi-terminal binary decision diagrams: An efficient data structure for matrix representation. Formal Methods in System Design, 10(2/3):149–169, April 1997.CrossRefGoogle Scholar
  11. 11.
    S. Graf and M. Schwartzbach, eds. Procs. of the 6th Workshop TACAS, Berlin, LNCS 1785. Springer, 2000.zbMATHGoogle Scholar
  12. 12.
    J.F. Groote and J. van de Pol. A bounded retransmission protocol for large data packets — A case study in computer checked algebraic verification. In M. Wirsing and M. Nivat, eds., Procs. of the 5 th AMAST Conference, Munich, LNCS 1101. Springer, 1996.Google Scholar
  13. 13.
    H.A. Hansson and B. Jonsson. A logic for reasoning about time and reliability. Formal Aspects of Computing, 6:512–535, 1994.zbMATHCrossRefGoogle Scholar
  14. 14.
    V. Hartonas-Garmhausen and S. Campos. ProbVerus: Probabilistic symbolic model mhecking. In In Katoen [24], pp. 96–110.Google Scholar
  15. 15.
    L. Helmink, M.P.A. Sellink, and F.W. Vaandrager. Proof-checking a data link protocol. In H. Barendregt and T. Nipkow, eds., Procs. International Workshop TYPES’93, Nijmegen, LNCS 806, pp. 127–165. Springer, 1994.Google Scholar
  16. 16.
    H. Hermanns. Personal communication, 2001.Google Scholar
  17. 17.
    H. Hermanns, J.-P. Katoen, J. Meyer-Kayser, and M. Siegle. A Markov chain model checker. In Graf and Schwartzbach [11], p. 347–362.Google Scholar
  18. 18.
    H. Hermanns, J. Meyer-Kayser, and M. Siegle. Multi terminal binary decision diagrams to represent and analyse continuous time Markov chains. In B. Plateau, W.J. Stewart, and M. Silva, eds., 3rd Int. Workshop on the Numerical Solution of Markov Chains, pp. 188–207. Prensas Universitarias de Zaragoza, 1999.Google Scholar
  19. 19.
    C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall International, Englewood Cliffs, 1985.zbMATHGoogle Scholar
  20. 20.
    M. Huth and M. Kwiatkowska. Quantitative analysis and model checking. In Procs. 12 th Annual Symposium on Logic in Computer Science, Warsaw. IEEE Press, 1997.Google Scholar
  21. 21.
    B. Jeannet. Dynamic partitioning in linear relation analysis. Application to the verification of reactive systems. Formal Methods in System Design, 2001. To appear.Google Scholar
  22. 22.
    B. Jonsson and K.G. Larsen. Specification and refinement of probailistic processes. In Procs. 6 th Annual Symposium on Logic in Computer Science, Amsterdam, pp. 266–277. IEEE Press, 1991.Google Scholar
  23. 23.
    B. Jonsson, K.G. Larsen, and W. Yi. Probabilistic extensions in process algebras. In J.A. Bergstra, A. Ponse, and S. Smolka, eds., Handbook of Process Algebras, pp. 685–710. Elsevier, 2001.Google Scholar
  24. 24.
    J.-P. Katoen, ed. Procs of the 5th ARTS, Bamberg, LNCS 1601. Springer, 1999.Google Scholar
  25. 25.
    M. Kwiatkowska, G. Norman, R. Segala, and J. Sproston. Automatic verification of real-time systems with probability distributions. In Katoen [24], pp. 75–95.Google Scholar
  26. 26.
    K.G. Larsen and A. Skou. Bisimulation through probabilistic testing. Information and Computation, 94:1–28, 1991.zbMATHCrossRefMathSciNetGoogle Scholar
  27. 27.
    M.L. Puterman. Markov Decision Processes: Discrete Stochastic Dynamic Programming. John Wiley & Sons, 1994.Google Scholar
  28. 28.
    R. Segala. Modeling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, Massachusetts Institute of Technology, 1995.Google Scholar
  29. 29.
    H. Sipma, T.E. Uribe, and Z. Manna. Deductive model checking. In R. Alur and T.A. Henzinger, eds. Procs. of the 8th CAV, New Brunswick, New Jersey, LNCS 1102. Springer, 1996.Google Scholar
  30. 30.
    F. Somenzi. Cudd: Colorado University Decision Diagram Package.
  31. 31.
    R. F. Lutje Spelberg, W. J. Toetenel, and M. Ammerlaan. Partition refinement in real-time model checking. In A.P. Ravn and H. Rischel, eds., Procs. of the 5th FTRTFT, Lyngby, LNCS 1486, pp. 143–157. Springer, 1998.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Pedro R. D’Argenio
    • 1
  • Bertrand Jeannet
    • 2
  • Henrik E. Jensen
    • 2
  • Kim G. Larsen
    • 1
    • 2
  1. 1.Faculty of InformaticsUniversity of TwenteAE - EnschedeThe Netherlands
  2. 2.BRICS -Aalb org UniversityAalborgDenmark

Personalised recommendations