Abstract
We present a novel abstraction technique which allows the analysis of reachability and safety properties of Markov decision processes with very large state spaces. The technique, called magnifying-lens abstraction, (MLA) copes with the state-explosion problem by partitioning the state-space into regions, and by computing upper and lower bounds for reachability and safety properties on the regions, rather than on the states. To compute these bounds, MLA iterates over the regions, considering the concrete states of each region in turn, as if one were sliding across the abstraction a magnifying lens which allowed viewing the concrete states. The algorithm adaptively refines the regions, using smaller regions where more detail is needed, until the difference between upper and lower bounds is smaller than a specified accuracy. We provide experimental results on three case studies illustrating that MLA can provide accurate answers, with savings in memory requirements.
This research was sponsored in part by the grant NSF-CCR-0132780.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
Bahar, R.I., Frohm, E.A., Gaona, C.M., Hachtel, G.D., Macii, E., Pardo, A., Somenzi, F.: Algebraic decision diagrams and their applications. Journal of Formal Methods in System Design 10(2/3), 171–206 (1997)
Baier, C., Hermanns, H.: Weak bisimulation for fully probabilistic processes. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 119–130. Springer, Heidelberg (1997)
B., J., Berger, J.O.: Adaptive mesh refinement for hyperbolic partial differential equations. Journal of Computational Physics 53, 484–512 (1984)
Bertsekas, D.: Dynamic Programming and Optimal Control. Athena Scientific vol. I, II (1995)
Cheshire, S., Adoba, B., Gutterman, E.: Dynamic configuration of ipv4 link local addresses (internet draft)
Clarke, E., Fujita, M., McGeer, P., Yang, J., Zhao, X.: Multi-terminal binary decision diagrams: An efficient data structure for matrix representation. In: International Workshop for Logic Synthesis (1993)
D’Argenio, P., Jeannet, B., Jensen, H., Larsen, K.: Reachability analysis of probabilistic systems by successive refinements. In: de Luca, L., Gilmore, S.T. (eds.) PROBMIV 2001, PAPM-PROBMIV 2001, and PAPM 2001. LNCS, vol. 2165, pp. 39–56. Springer, Heidelberg (2001)
de Alfaro, L.: Formal Verification of Probabilistic Systems. PhD thesis, Stanford University, Technical Report STAN-CS-TR-98-1601 (1997)
de Alfaro, L.: Computing minimum and maximum reachability times in probabilistic systems. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 66–81. Springer, Heidelberg (1999)
de Alfaro, L., Kwiatkowska, M., Norman, G., Parker, D., Segala, R.: Symbolic model checking of concurrent probabilistic processes using MTBDDs and the Kronecker representation. In: Schwartzbach, M.I., Graf, S. (eds.) ETAPS 2000 and TACAS 2000. LNCS, vol. 1785, pp. 395–410. Springer, Heidelberg (2000)
de Alfaro, L., Majumdar, R.: Quantitative solution of omega-regular games. Journal of Computer and System Sciences 68, 374–397 (2004)
Dean, T., Givan, R.: Model minimization in markov decision processes. In: AAAI/IAAI, pp. 106–111 (1997)
Derman, C.: Finite State Markovian Decision Processes. Academic Press, London (1970)
Fecher, H., Leucker, M., Wolf, V.: Don’t know in probabilistic systems. In: Valmari, A. (ed.) Model Checking Software. LNCS, vol. 3925, Springer, Heidelberg (2006)
Gilboa, I.: Expected utility with purely subjective non-additive probabilities. Journal of Mathematical Economics 16, 65–88 (1987)
Gilboa, I., Schmeidler, D.: Additive representations of non-additive measures and the choquet integral. Discussion Papers 985, Northwestern University, Center for Mathematical Studies in Economics and Management Science (1992), available at http://ideas.repec.org/p/nwu/cmsems/985.html.
Hinton, A., Kwiatkowska, M., Norman, G., Parker, D.: PRISM: A tool for automatic verification of probabilistic systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006 and ETAPS 2006. LNCS, vol. 3920, pp. 441–444. Springer, Heidelberg (2006)
Huth, M.: On finite-state approximations for probabilistic computational-tree logic. Theor. Comp. Sci. 346(1), 113–134 (2005)
Kwiatkowska, M., Norman, G., Parker, D.: Game-based abstraction for markov decision processes. In: Proc. of QEST: Quantitative Evaluation of Systems, pp. 157–166. IEEE Computer Society Press, Los Alamitos (2006)
Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, New York (1991)
McIver, A., Morgan, C.: Abstraction, Refinement, and Proof for Probabilistic Systems. In: Monographs in Computer Science, Springer, Heidelberg (2004)
Monniaux, D.: Abstract interpretation of programs as Markov decision processes. Science of Computer Programming 58(1–2), 179–205 (2005)
Plateau, B.: On the stochastic structure of parallelism and synchronization models for distributed algorithms. In: SIGMETRICS 1985. Proceedings of the 1985 ACM SIGMETRICS conference on Measurement and modeling of computer systems, pp. 147–154. ACM Press, New York, NY, USA (1985)
Plilippou, A., Lee, I., Sokolsky, O.: Weak bisimulation for probabilistic systems. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 334–349. Springer, Heidelberg (2000)
Schmeidler, D.: Integral representation without additivity. Proceedings of the American Mathematical Society 97, 255–261 (1986)
Segala, R.: Modeling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, MIT, Technical Report MIT/LCS/TR-676 (1995)
Segala, R., Lynch, N.A.: Probabilistic simulations for probabilistic processes. In: Jonsson, B., Parrow, J. (eds.) CONCUR 1994. LNCS, vol. 836, pp. 481–496. Springer, Heidelberg (1994)
Vardi, M.Y.: Automatic verification of probabilistic concurrent finite-state systems. In: Proc. 26th IEEE Symp. Found. of Comp. Sci., pp. 327–338. IEEE Computer Society Press, Los Alamitos (1985)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
de Alfaro, L., Roy, P. (2007). Magnifying-Lens Abstraction for Markov Decision Processes. In: Damm, W., Hermanns, H. (eds) Computer Aided Verification. CAV 2007. Lecture Notes in Computer Science, vol 4590. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73368-3_38
Download citation
DOI: https://doi.org/10.1007/978-3-540-73368-3_38
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-73367-6
Online ISBN: 978-3-540-73368-3
eBook Packages: Computer ScienceComputer Science (R0)