Reduction and Refinement Strategies for Probabilistic Analysis
- 296 Downloads
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.
KeywordsLinear Programming Problem Essential State Simple Path Reachable State Initial Partition
Unable to display preview. Download preview PDF.
- 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.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.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.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.Christel Baier. On Algorithmic Verification Methods for Probabilistic Systems. Habilitation thesis, Faculty for Mathematics and Informatics, University of Mannheim, 1998.Google Scholar
- 6.M. Berkelaar. LP_Solve: Mixed integer linear program solver, ftp://ftp.ics.ele.tue.nl/pub/lp_solve.
- 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
- 10.Luca de Alfaro. Formal Verification of Probabilistic Systems. PhD thesis, Stanford University, 1997.Google Scholar
- 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.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.K. Fukuda. Cddlib. ftp://ftp.ifor.math.ethz.ch/pub/fukuda/cdd.
- 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
- 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.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.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.M. Kwiatkowska, G. Norman, and D. Parker. PRISM: Probabilistic symbolic model checker. In TOOLS’2002, volume 2324 of LNCS, April 2002.Google Scholar
- 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.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.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.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.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.PRISM Web Page, http://www.cs.bham.ac.uk/~dxp/prism/.
- 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.R. Segala. Modeling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, Department of Mathematics, Massachusetts Institute of Technology, 1995.Google Scholar
- 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.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