Probabilistic CEGAR. (English) Zbl 1155.68438
Gupta, Aarti (ed.) et al., Computer aided verification. 20th international conference, CAV 2008, Princeton, NJ, USA, July 7–14, 2008. Proceedings. Berlin: Springer (ISBN 978-3-540-70543-7/pbk). Lecture Notes in Computer Science 5123, 162-175 (2008).
Summary: Counterexample-guided abstraction refinement (CEGAR) has been en vogue for the automatic verification of very large systems in the past years. When trying to apply CEGAR to the verification of probabilistic systems, various foundational questions arise. This paper explores them in the context of predicate abstraction.
For the entire collection see [Zbl 1139.68005].
For the entire collection see [Zbl 1139.68005].
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
Software:
CEGARReferences:
| [1] | Hansson, H.; Jonsson, B., A Logic for Reasoning about Time and Reliability, Formal Asp. Comput., 6, 512-535 (1994) · Zbl 0820.68113 · doi:10.1007/BF01211866 |
| [2] | Bianco, A.; de Alfaro, L.; Thiagarajan, P. S., Model checking of probabilistic and nondeterministic systems, Foundations of Software Technology and Theoretical Computer Science, 499-513 (1995), Heidelberg: Springer, Heidelberg · Zbl 1354.68167 |
| [3] | Hinton, A.; Kwiatkowska, M. Z.; Norman, G.; Parker, D.; Hermanns, H.; Palsberg, J., PRISM: A Tool for Automatic Verification of Probabilistic Systems, Tools and Algorithms for the Construction and Analysis of Systems, 441-444 (2006), Heidelberg: Springer, Heidelberg · doi:10.1007/11691372_29 |
| [4] | Katoen, J.P., Khattri, M., Zapreev, I.S.: A Markov reward model checker. In: QEST, pp. 243-244 (2005) |
| [5] | Graf, S.; Saídi, H.; Grumberg, O., Construction of Abstract State Graphs with PVS, Computer Aided Verification, 72-83 (1997), Heidelberg: Springer, Heidelberg |
| [6] | Ball, T., Rajamani, S.K.: The SLAM project: debugging system software via static analysis. In: POPL, pp. 1-3 (2002) |
| [7] | Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL, pp. 58-70 (2002) · Zbl 1323.68374 |
| [8] | Clarke, E. M.; Grumberg, O.; Jha, S.; Lu, Y.; Veith, H.; Emerson, E. A.; Sistla, A. P., Counterexample-Guided Abstraction Refinement, Computer Aided Verification, 154-169 (2000), Heidelberg: Springer, Heidelberg · Zbl 0974.68517 · doi:10.1007/10722167_15 |
| [9] | Wachter, B., Zhang, L., Hermanns, H.: Probabilistic Model Checking Modulo Theories. In: QEST, pp. 129-138 (2007) |
| [10] | Segala, R.; Lynch, N. A., Probabilistic simulations for probabilistic processes, Nord. J. Comput., 2, 250-273 (1995) · Zbl 0839.68067 |
| [11] | Chatterjee, K., Henzinger, T.A., Majumdar, R.: Counterexample-Guided Planning. In: UAI (2005) |
| [12] | Han, T.; Katoen, J. P.; Grumberg, O.; Huth, M., Counterexamples in probabilistic model checking, Tools and Algorithms for the Construction and Analysis of Systems, 72-86 (2007), Heidelberg: Springer, Heidelberg · Zbl 1186.68293 · doi:10.1007/978-3-540-71209-1_8 |
| [13] | Papadimitriou, C. H.; Yannakakis, M., Optimization, approximation, and complexity classes, J. Comput. Syst. Sci., 43, 425-440 (1991) · Zbl 0765.68036 · doi:10.1016/0022-0000(91)90023-X |
| [14] | McMillan, K. L.; Ball, T.; Jones, R. B., Lazy abstraction with interpolants, Computer Aided Verification, 123-136 (2006), Heidelberg: Springer, Heidelberg · Zbl 1188.68196 · doi:10.1007/11817963_14 |
| [15] | Aljazzar, H.; Hermanns, H.; Leue, S.; Pettersson, P.; Yi, W., Counterexamples for timed probabilistic reachability, Formal Modeling and Analysis of Timed Systems, 177-195 (2005), Heidelberg: Springer, Heidelberg · Zbl 1175.68239 · doi:10.1007/11603009_15 |
| [16] | D’Argenio, P. R.; Jeannet, B.; Jensen, H. E.; Larsen, K. G.; Hermanns, H.; Segala, R., Reduction and Refinement Strategies for Probabilistic Analysis, Process Algebra and Probabilistic Methods. Performance Modeling and Verification, 57-76 (2002), Heidelberg: Springer, Heidelberg · Zbl 1065.68582 · doi:10.1007/3-540-45605-8_5 |
| [17] | de Alfaro, L.; Roy, P.; Damm, W.; Hermanns, H., Magnifying-lens abstraction for markov decision processes, Computer Aided Verification, 325-338 (2007), Heidelberg: Springer, Heidelberg · Zbl 1135.68486 · doi:10.1007/978-3-540-73368-3_38 |
| [18] | Kwiatkowska, M., Norman, G., Parker, D.: Game-based Abstraction for Markov Decision Processes. In: QEST, pp. 157-166 (2006) |
| [19] | Fecher, H.; Leucker, M.; Wolf, V.; Valmari, A., Don’t Know, Model Checking Software, 71-88 (2006), Heidelberg: Springer, Heidelberg · Zbl 1178.68341 · doi:10.1007/11691617_5 |
| [20] | Puterman, M. L., Markov Decision Processes: Discrete Stochastic Dynamic Programming (1994), Chichester: John Wiley & Sons, Chichester · Zbl 0829.90134 |
| [21] | Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: POPL, pp. 232-244 (2004) · Zbl 1325.68147 |
| [22] | Dechter, R.; Pearl, J., Generalized best-first search strategies and the optimality af A*, J. ACM, 32, 505-536 (1985) · Zbl 0631.68075 · doi:10.1145/3828.3830 |
| [23] | Dutertre, B.; de Moura, L. M.; Ball, T.; Jones, R. B., A Fast Linear-Arithmetic Solver for DPLL(T), Computer Aided Verification, 81-94 (2006), Heidelberg: Springer, Heidelberg · doi:10.1007/11817963_11 |
| [24] | McMillan, K. L., An interpolating theorem prover, Theor. Comput. Sci., 345, 101-121 (2005) · Zbl 1079.68092 · doi:10.1016/j.tcs.2005.07.003 |
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.
