Exact quantitative probabilistic model checking through rational search. (English) Zbl 1506.68057
Summary: Model checking systems formalized using probabilistic models such as discrete time Markov chains (DTMCs) and Markov decision processes (MDPs) can be reduced to computing constrained reachability properties. Linear programming methods to compute reachability probabilities for DTMCs and MDPs do not scale to large models. Thus, model checking tools often employ iterative methods to approximate reachability probabilities. These approximations can be far from the actual probabilities, leading to inaccurate model checking results. On the other hand, specialized techniques employed in existing state-of-the-art exact quantitative model checkers, don’t scale as well as their iterative counterparts. In this work, we present a new model checking algorithm that improves the approximate results obtained by scalable iterative techniques to compute exact reachability probabilities. Our techniques are implemented as an extension of the PRISM model checker and are evaluated against other exact quantitative model checking engines.
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 60J20 | Applications of Markov chains and discrete-time Markov processes on general state spaces (social mobility, learning theory, industrial processes, etc.) |
| 68Q87 | Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) |
| 90C40 | Markov and semi-Markov decision processes |
Keywords:
exact quantitative model checking; Markov decision processes; Markov chains; probabilistic systemsReferences:
| [1] | (2017) Ensuring the reliability of your model checker: interval iteration for Markov decision processes. https://wwwtcs.inf.tu-dresden.de/ALGI/PUB/CAV17/ |
| [2] | (2017) PRISM benchmark suite,http://www.prismmodelchecker.org/benchmarks/. Accessed 5 May 2020 |
| [3] | (2017) PRISM case studies, http://www.prismmodelchecker.org/casestudies/. Accessed 5 May 2020 |
| [4] | (2019) Apfloat. http://www.apfloat.org/ |
| [5] | (2019) CUDD. http://vlsi.colorado.edu/ fabio/CUDD/html/ |
| [6] | (2019) GNU multiple precision arithmetic library. https://gmplib.org/ |
| [7] | (2019) JScience. http://jscience.org/ |
| [8] | (2019) RationalSearch. https://publish.illinois.edu/rationalmodelchecker/ |
| [9] | de Alfaro L (1997) Formal verification of probabilistic systems. Ph.D. thesis, Stanford University |
| [10] | Baier, C.; Katoen, JP, Principles of model checking (representation and mind series) (2008), Cambridge: The MIT Press, Cambridge · Zbl 1179.68076 |
| [11] | Baier C, Klein J, Leuschner L, Parker D, Wunderlich S (2017) Ensuring the reliability of your model checker: interval iteration for Markov decision processes. In: Computer aided verification |
| [12] | Banach, S., Sur les opérations dans les ensembles abstraits et leur application aux équations intégrales, Fundamenta Mathematicae, 3, 1, 133-181 (1922) · JFM 48.0201.01 · doi:10.4064/fm-3-1-133-181 |
| [13] | Bauer MS, Mathur U, Chadha R, Sistla AP, Viswanathan M (2017) Exact quantitative probabilistic model checking through rational search. In: Proceedings of the 17th conference on formal methods in computer-aided design, FMCAD Inc, Austin, TX, FMCAD ’17, pp 92-99. doi:10.23919/FMCAD.2017.8102246. http://dl.acm.org/citation.cfm?id=3168451.3168475 |
| [14] | Benini, L.; Bogliolo, A.; Paleologo, GA; De Micheli, G., Policy optimization for dynamic power management, IEEE Trans Comput-Aided Des Integr Circuits Syst, 13, 813-833 (1999) · doi:10.1109/43.766730 |
| [15] | Bhaduri, D.; Shukla, SK; Graham, PS; Gokhale, MB, Reliability analysis of large circuits using scalable techniques and tools, IEEE Trans Circuits Syst I: Regul Pap, 54, 2447-2460 (2007) · Zbl 1374.94961 · doi:10.1109/TCSI.2007.907863 |
| [16] | Bianco A, de Alfaro L (1995) Model checking of probabilistic and nondeterministic systems. In: 15th Conference foundations of software technology and theoretical computer science, lecture notes in computer science. Springer, Berlin, vol 1026, pp 499-513 · Zbl 1354.68167 |
| [17] | Brázdil T, Chatterjee K, Chmelík M, Forejt V, Křetínský J, Kwiatkowska M, Parker D, Ujma M (2014) Verification of markov decision processes using learning algorithms. In: Automated technology for verification and analysis. Springer, Cham, pp 98-114 · Zbl 1448.68290 |
| [18] | Bryant, RE, Graph-based algorithms for boolean function manipulation, EEE Trans Comput, 100, 8, 677-691 (1986) · Zbl 0593.94022 · doi:10.1109/TC.1986.1676819 |
| [19] | Chatterjee, K.; Henzinger, TA, Value iteration, 107-138 (2008), Berlin: Springer, Berlin · Zbl 1143.68042 · doi:10.1007/978-3-540-69850-0_7 |
| [20] | Chaum, D., The dining cryptographers problem: Unconditional sender and recipient untraceability, J Cryptol, 1, 1, 65-75 (1988) · Zbl 0654.94012 · doi:10.1007/BF00206326 |
| [21] | Daws C (2004) Symbolic and parametric model checking of discrete-time Markov chains. In: International Colloquium on theoretical aspects of computing. Springer, Berlin, pp 280-294 · Zbl 1108.68497 |
| [22] | Dehnert C, Junges S, Katoen JP, Volk M (2017) A storm is coming: A modern probabilistic model checker. In: 29th international conference computer aided verification CAV 2017 |
| [23] | Dehnert C, Junges S, Jansen N, Corzilius F, Volk M, Bruintjes H, Katoen JP, Abraham E (2015) Prophesy: a probabilistic parameter synthesis tool. In: International conference on computer aided verification, CAV |
| [24] | van Dijk T, van de Pol J (2015) Sylvan: Multi-core decision diagrams. In: International conference on tools and algorithms for the construction and analysis of systems. Springer, Berlin, pp 677-691 |
| [25] | Dijkstra EW (1982) Self-stabilization in spite of distributed control. In: Selected writings on computing: a personal perspective. Springer, Berlin · Zbl 0497.68001 |
| [26] | Duflot, M.; Kwiatkowska, M.; Norman, G.; Parker, D., A formal analysis of bluetooth device discovery, Int J Softw Tools Technol Transf (STTT), 8, 6, 621-632 (2006) · doi:10.1007/s10009-006-0014-x |
| [27] | Forejt V, Kwiatkowska M, Norman G, Parker D (2011a) Automated verification techniques for probabilistic systems. In: International school on formal methods for the design of computer, communication and software systems. Springer, Berlin, pp 53-113 · Zbl 1315.68177 |
| [28] | Forejt V, Kwiatkowska MZ, Norman G, Parker D (2011b) Automated verification techniques for probabilistic systems. In: Formal methods for eternal networked software systems—11th international school on formal methods for the design of computer, communication and software systems, SFM, pp 53-113 · Zbl 1315.68177 |
| [29] | Fujita, M.; McGeer, PC; Yang, JY, Multi-terminal binary decision diagrams: an efficient data structure for matrix representation, Formal Methods Syst Des, 10, 2-3, 149-169 (1997) · doi:10.1023/A:1008647823331 |
| [30] | Giro S (2012) Efficient computation of exact solutions for quantitative model checking. In: Proceedings of 10th workshop on quantitative aspects of programming languages (QAPL’12) |
| [31] | Haddad S, Monmege B (2014) Reachability in MDPS: refining convergence of value iteration. In: International workshop on reachability problems. Springer, Berlin, pp 125-137 · Zbl 1393.68102 |
| [32] | Hahn EM, Hermanns H, Wachter B, Zhang L (2010) PARAM: a model checker for parametric Markov models. In: International conference on computer aided verification (CAV’10) |
| [33] | Hahn EM, Han T, Zhang L (2011a) Synthesis for PCTL in parametric Markov decision processes. In: NASA formal methods symposium. Springer, Berlin, pp 146-161 |
| [34] | Hahn, EM; Hermanns, H.; Zhang, L., Probabilistic reachability for parametric Markov models, Int J Softw Tools Technol Transf, 13, 1, 3-19 (2011) · doi:10.1007/s10009-010-0146-x |
| [35] | Han, J.; Chen, H.; Boykin, E.; Fortes, J., Reliability evaluation of logic circuits using probabilistic gate models, Microelectron Reliab, 51, 468-476 (2011) · doi:10.1016/j.microrel.2010.07.154 |
| [36] | Hoey J, St-Aubin R, Hu A, Boutilier C (1999) Spudd: Stochastic planning using decision diagrams. In: Proceedings of the fifteenth conference on uncertainty in artificial intelligence |
| [37] | Hopcroft, JE, Introduction to automata theory, languages, and computation (2008), Delhi: Pearson Education India, Delhi |
| [38] | Jeannet B, D’Argenio P, Larsen K (2002) Rapture: a tool for verifying Markov decision processes. In: Proceeding of tools day, affiliated to 13th international conference concurrency theory (CONCUR’02) |
| [39] | Katoen JP, Khattri M, Zapreevt I (2005) A Markov reward model checker. In: Second international conference on the quantitative evaluation of systems (QEST’05), IEEE |
| [40] | Kwek, S.; Mehlhorn, K., Optimal search for rationals, Inf Process Lett, 86, 1, 23-26 (2003) · Zbl 1173.68826 · doi:10.1016/S0020-0190(02)00455-6 |
| [41] | Kwiatkowska M, Norman G, Sproston J (2002) Probabilistic model checking of the IEEE 802.11 wireless local area network protocol. In: Proceedings of 2nd joint international workshop on process algebra and probabilistic methods, performance modeling and verification (PAPM/PROBMIV’02) · Zbl 1065.68583 |
| [42] | Kwiatkowska, M.; Norman, G.; Sproston, J., Probabilistic model checking of deadline properties in the IEEE 1394 FireWire root contention protocol, Formal Aspects Comput, 14, 3, 295-318 (2003) · Zbl 1029.68017 · doi:10.1007/s001650300007 |
| [43] | Kwiatkowska M, Norman G, Parker D (2004) Controller dependability analysis by probabilistic model checking. In: 11th IFAC symposium on information control problems in manufacturing (INCOM’04) |
| [44] | Kwiatkowska M, Norman G, Parker D (2011) Prism 4.0: verification of probabilistic real-time systems. In: International conference on computer aided verification. Springer, Berlin, pp 585-591 |
| [45] | McMillan, KL, Symbolic model checking (1993), Norwell: Kluwer Academic Publishers, Norwell · Zbl 0784.68004 · doi:10.1007/978-1-4615-3190-6 |
| [46] | Mohyuddin N, Pakbaznia E, Pedram M (2011) Probabilistic error propagation in a logic circuit using the Boolean difference calculus. In: Advanced techniques in logic synthesis, optimizations and applications. Springer, Berlin, pp 359-381 |
| [47] | Norman, G.; Parker, D.; Kwiatkowska, M.; Shukla, S., Evaluating the reliability of NAND multiplexing with PRISM, IEEE Trans Comput-Aided Des Integr Circuits Syst, 24, 1629-1637 (2005) · doi:10.1109/TCAD.2005.852033 |
| [48] | Parker D (2002) Implementation of symbolic model checking for probabilistic systems. Ph.D. thesis, University of Birmingham |
| [49] | Qiu, Q.; Qu, Q.; Pedram, M., Stochastic modeling of a power-managed system-construction and optimization, IEEE Trans Comput-Aided Des Integr Circuits Syst, 20, 1200-1217 (2001) · doi:10.1109/43.952737 |
| [50] | Rabin M (1983) Randomized Byzantine generals. In: Proceedings of symposium on foundations of computer science, pp 403-409 |
| [51] | Rutten, J.; Kwiatkowska, M.; Norman, G.; Parker, D.; Panangaden, P.; van Breugel, F., Mathematical techniques for analyzing concurrent and probabilistic systems, CRM monograph series (2004), Providence: American Mathematical Society, Providence · Zbl 1069.68074 |
| [52] | Rutten, JJ; Kwiatkowska, M.; Norman, G.; Parker, D., Mathematical techniques for analyzing concurrent and probabilistic systems (2004), Providence: American Mathematical Society, Providence · Zbl 1069.68074 · doi:10.1090/crmm/023 |
| [53] | St-Aubin R, Hoey J, Boutilier C (2001) APRICODD: approximate policy construction using decision diagrams. In: Advances in neural information processing systems, pp 1089-1095 |
| [54] | Wimmer R, Kortus A, Herbstritt M, Becker B (2008) Probabilistic model checking and reliability of results. In: 11th IEEE workshop on design and diagnostics of electronic circuits and systems, 2008. DDECS, IEEE, pp 1-6 · Zbl 1156.68480 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
