Reduction and Refinement Strategies for Probabilistic Analysis

  • 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 2399)


We report on new strategies for model checking quantitative reachability properties of Markov decision processes by successive refinements. In our approach, properties are analyzed on abstractions rather than directly on the given model. Such abstractions are expected to be 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 involved in settling the validity of the property is more costly than the refinement process, the method profits from applying such numerical analysis on smaller state spaces. The method is significantly enhanced by a number of novel strategies: a strategy for reducing the size of the numerical problems to be analyzed by identification of so-called essential states, and heuristic strategies for guiding the refinement process.


Linear Programming Problem Essential State Simple Path Reachable State Initial Partition 
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, D. Dill, N. Halbwachs, and H. Wong-Toi. Minimization of timed transition systems. In Proceedings of the Third Conference on Concurrency Theory CONCUR’ 92, volume 630 of LNCS, pages 340–354. Springer-Verlag, 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 Computer Aided Verification, CAV’95, volume 939 of LNCS, July 1995.Google Scholar
  3. 3.
    R. Bahar, E. Frohm, C. Gaona, G. Hachtel, E. Macii, A. Pardo, and F. Somenzi. Algebraic decision diagrams and their applications. Formal Methods in System Design, 10(2/3):171–206, April 1997.Google Scholar
  4. 4.
    C. Baier, J.-P. Katoen, and H. Hermanns. Approximate symbolic model checking of continuous-time Markov chains. In CONCUR’99, volume 1664 of LNCS, 1999.Google Scholar
  5. 5.
    Christel Baier. On Algorithmic Verification Methods for Probabilistic Systems. Habilitation thesis, Faculty for Mathematics and Informatics, University of Mannheim, 1998.Google Scholar
  6. 6.
    M. Berkelaar. LP_Solve: Mixed integer linear program solver,
  7. 7.
    A. Bianco and L. de Alfaro. Model checking of probabilistic and nondeterministic systems. In Foundations of Software Technology and Theoretical Computer Science, FSTTCS’95, volume 1026 of LNCS, 1995.Google Scholar
  8. 8.
    M. Bozga, C. Daws, O. Maler, A. Olivero, S. Tripakis, and S. Yovine. Kronos: A model-checking tool for real-time systems. In Computer Aided Verification, CAV’98, volume 1427 of LNCS, July 1998.CrossRefGoogle Scholar
  9. 9.
    P.R. D’Argenio, B. Jeannet, H.E. Jensen, and K.G. Larsen. Reachability analysis of probabilistic systems by successive refinements. In Process Algebra and Probabilistic Methods-Performance Modelling and Verification, PAPM-PROBMIV 2001, volume 2165 of LNCS, pages 39–56, 2001.CrossRefGoogle Scholar
  10. 10.
    Luca de Alfaro. Formal Verification of Probabilistic Systems. PhD thesis, Stanford University, 1997.Google Scholar
  11. 11.
    J.-C. Fernandez, H. Garavel, A. Kerbrat, R. Mateescu, L. Mounier, and M. Sighireanu. CADP (Cæsar / Aldébaran Development Package): A protocol validation and verification toolbox. In Computer Aided Verification, GAV’96, volume 1102 of LNCS, July 1996.Google Scholar
  12. 12.
    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.Google Scholar
  13. 13.
  14. 14.
    H.A. Hansson and B. Jonsson. A logic for reasoning about time and reliability. Formal Aspects of Computing, 6:512–535, 1994.zbMATHCrossRefGoogle Scholar
  15. 15.
    V. Hartonas-Garmhausen and S. Campos. ProbVerus: Probabilistic symbolic model checking. In AMAST Workshop on Real-Time and Probabilistic Systems, AMAST’99, volume 1601 of LNCS, 1999.CrossRefGoogle Scholar
  16. 16.
    L. Helmink, M. Sellink, and F. Vaandrager. Proof-checking a data link protocol. In Proc. International Workshop TYPES’93, volume 806 of LNCS, 1994.Google Scholar
  17. 17.
    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, TACAS 2000, volume 1785 of LNCS, 2000.CrossRefGoogle Scholar
  18. 18.
    G. Holzmann. The model cheker spin. IEEE Transactions on Software Engineering, 23(5):279–295, 1997.CrossRefMathSciNetGoogle Scholar
  19. 19.
    M. Huth and M. Kwiatkowska. Quantitative analysis and model checking. In Logic in Computer Science, LICS’97. IEEE Computer Society Press, 1997.Google Scholar
  20. 20.
    B. Jonsson and K.G. Larsen. Specification and refinement of probabilistic processes. In Procs. 6th Annual Symposium on Logic in Computer Science, pages 266–277. IEEE Press, 1991.Google Scholar
  21. 21.
    B. Jonsson, K.G. Larsen, and W. Yi. Probabilistic extensions in process algebras. In J.A. Bergstra, A. Ponse, and S. Smolka, editors, Handbook of Process Algebras. Elsevier, 2001.Google Scholar
  22. 22.
    M. Kwiatkowska, G. Norman, and D. Parker. PRISM: Probabilistic symbolic model checker. In TOOLS’2002, volume 2324 of LNCS, April 2002.Google Scholar
  23. 23.
    M. Kwiatkowska, G. Norman, R. Segala, and J. Sproston. Automatic verification of real-time systems with probability distributions. In J.P. Katoen, editor, Procs. of the 5th ARTS, volume 1601 of LNCS, pages 75–95. Springer, 1999.Google Scholar
  24. 24.
    Kim G. Larsen, Paul Pettersson, and Wang Yi. UPPAAL in a nutshell. Springer International Journal of Software Tools for Technology Transfer, 1(1/2), 1997.Google Scholar
  25. 25.
    D. Lehmann and M. Rabin. On the advantages of free choice: A symmetric fully distributed solution to the dining philosophers problem. In Proc. 8th Symposium on Principles of Programming Languages, 1981.Google Scholar
  26. 26.
    N. Lynch, I. Saias, and R. Segala. Proving time bounds for randomized distributed algorithms. In Proc. 13th ACM Symposium on Principles of Distributed Computing, 1984.Google Scholar
  27. 27.
    K. Mehlhorn and A.K. Tsakalidis:. Data structures. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume A: Algorithms and Complexity, pages 301–342. Elsevier, 1990.Google Scholar
  28. 28.
  29. 29.
    M.L. Puterman. Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley series in probability and mathematical statistics. John Wiley & Sons, 1994.Google Scholar
  30. 30.
    R. Segala. Modeling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, Department of Mathematics, Massachusetts Institute of Technology, 1995.Google Scholar
  31. 31.
    D. Simons, and M. Stoelinga. Mechanical verification of the IEEE1394a root contention protocol using Uppaal2k. To appear in International Journal on Software Tools for Technlogy Transfer, 2001.Google Scholar
  32. 32.
    M. Stoelinga and F. Vaandrager. Root contention in IEEE 1394. In Proc. 5th AMAST Workshop on Real-Time and Probabilistic Systems (ARTS’99), volume 1601 of LNCS, 1999.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Pedro R. D’Argenio
    • 1
  • Bertrand Jeannet
    • 2
  • Henrik E. Jensen
    • 3
  • Kim G. Larsen
    • 3
  1. 1.FaMAFUniversidad Nacional de CórdobaCórdobaArgentina
  2. 2.IRISA - INRIARennes CedexFrance
  3. 3.BRICSAalborg UniversityAalborgDenmark

Personalised recommendations