Rohit Chadha
Abstract
The main challenge in using abstractions effectively is to construct a suitable abstraction for the system being verified. One approach that tries to address this problem is that of counterexample guided abstraction refinement (CEGAR), wherein one starts with a coarse abstraction of the system, and progressively refines it, based on invalid counterexamples seen in prior model checking runs, until either an abstraction proves the correctness of the system or a valid counterexample is generated. While CEGAR has been successfully used in verifying nonprobabilistic systems automatically, CEGAR has only recently been investigated in the context of probabilistic systems. The main issues that need to be tackled in order to extend the approach to probabilistic systems is a suitable notion of “counterexample”, algorithms to generate counterexamples, check their validity, and then automatically refine an abstraction based on an invalid counterexample. In this article, we address these issues, and present a CEGAR framework for Markov decision processes.
Supplemental Material
Available for Download
Online appendix to a counterexample-guided abstraction-refinement framework for markov decision processes on article 1.
- Aljazzar, H., Hermanns, H., and Leue, S. 2005. Counterexamples for timed probabilistic reachability. In Proceedings of the International Conference on Formal Modelling and Analysis of Timed Systems. 177--195. Google Scholar
Digital Library
- Aljazzar, H. and Leue, S. 2007. Counterexamples for model checking of Markov decision processes. Tech. rep. soft-08-01. University of Konstanz, Konstanz, Germany.Google Scholar
- Baier, C., Engelen, B., and Majster-Cederbaum, M. E. 2000. Deciding bisimilarity and similarity for probabilistic processes. J. Comput. Syst. Sci. 60, 1, 187--231. Google ScholarDigital Library
- Baier, C., Katoen, J.-P., Hermanns, H., and Wolf, V. 2005. Comparative branching-time semantics for Markov chains. Inform. Computat. 200, 149--214. Google ScholarDigital Library
- Ball, T. and Rajamani, S. 2002. Generating abstract explanations of spurious counterexamples in C programs. Tech. rep. 2002-09. Microsoft Research, Redmand, WA.Google Scholar
- Bianco, A. and de Alfaro, L. 1995. Model checking of probabilistic and nondeterministic systems. In Proceedings of the International Conference on the Foundations of Software Technology and Theoretical Computer Science. 499--513. Google ScholarDigital Library
- Bjesse, P. and Kukula, J. 2004. Using counter example guided abstraction refinement to find complex bugs. In Proceedings of Design, Automation, and Test in Europe Conference and Exposition. 156--161. Google ScholarDigital Library
- Bouajjani, A., Habermehl, P., and Vojnar, T. 2004. Abstract regular model checking. In Proceedings of the International Conference on Computer Aided Verification. 372--286.Google Scholar
- Chatterjee, K., Henzinger, T., Jhala, R., and Majumdar, R. 2005. Counter-example guided planning. In Proceedings of the Conference on Uncertainty in Artificial Intelligence. 104--111.Google Scholar
- Clarke, E., Grumberg, O., Jha, S., Lu, Y., and Veith, H. 2000. Counterexample-guided abstraction refinement. In Proceedings of the International Conference on Computer Aided Verification. 154--169. Google ScholarDigital Library
- Clarke, E., Gupta, A., Kukula, J., and Strichman, O. 2002a. SAT based abstraction-refinement using ILP and machine learning techniques. In Proceedings of the International Conference on Computer Aided Verification. 265--279. Google ScholarDigital Library
- Clarke, E., Jha, S., Lu, Y., and Veith, H. 2002b. Tree-like counterexamples in model checking. In Proceedings of the IEEE Symposium on Logic in Computer Science. 19--29. Google ScholarDigital Library
- Cook, B., Podelski, A., and Rybalchenko, A. 2005. Abstraction refinement for termination. In Proceedings of the International Static Analysis Symposium. 87--101. Google ScholarDigital Library
- D'Argenio, P. R., Jeannet, B., Jensen, H. E., and Larsen, K. G. 2001. Reachability analysis of probabilistic systems by successive refinements. In Proceedings of the International Workshop on Performance Modeling and Verification. 39--56. Google ScholarDigital Library
- D'Argenio, P. R., Jeannet, B., Jensen, H. E., and Larsen, K. G. 2002. Reduction and refinement strategies for probabilistic analysis. In Proceedings of the International Workshop on Performance Modeling and Verification. 57--76. Google ScholarDigital Library
- Das, S. 2003. Predicate abstraction. Ph.D. dissertation. Stanford University, Stanford, CA.Google Scholar
- de Alfaro, L. and Roy, P. 2007. Magnifying-lens abstraction for markov decision processes. In Proceedings of the International Conference on Computer Aided Verification. 325--338. Google ScholarDigital Library
- Desharnais, J. 1999a. Labelled Markov processes. Ph.D. dissertation. McGill University, Montreal, P.Q., Canada.Google Scholar
- Desharnais, J. 1999b. Logical characterization of simulation for Markov chains. In Proceedings of the International Workshop on Performance Modeling and Verification.Google Scholar
- Desharnais, J., Gupta, V., Jagadeesan, R., and Panangaden, P. 2000. Approximating labeled Markov processes. In Proceedings of the IEEE Symposium on Logic in Computer Science. 95--106. Google ScholarDigital Library
- Dodis, Y. and Khanna, S. 1999. Designing networks with bounded pairwise distance. In Proceedings of the ACM Symposium on the Theory of Computing. 750--759. Google ScholarDigital Library
- Fecher, H., Leucker, M., and Wolf, V. 2006. Don't know in probabilistic systems. In Proceedings of the International SPIN Workshop on Model Checking Software. 71--88. Google ScholarDigital Library
- Garey, M. and Johnson, D. 1979. Computers and Intractability: A Guide to the Theory of NP-Completeness. Freeman, New York, NY. Google ScholarDigital Library
- Glussman, M., Kamhi, G., Mador-Haim, S., Fraer, R., and Vardi, M. 2003. Multiple-counterexample guided iterative abstraction refinement: an industrial evaluation. In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 176--191. Google ScholarDigital Library
- Gurfinkel, A. and Chechik, M. 2006. Why waste a perfectly good abstraction? In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 212--226. Google ScholarDigital Library
- Han, T. and Katoen, J.-P. 2007a. Counterexamples in probabilistic model checking. In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 72--86. Google ScholarDigital Library
- Han, T. and Katoen, J.-P. 2007b. Providing evidence of likely being on time—counterexample generation for CTMC. In Proceedings of the International Symposium on Automated Technology for Verification and Analysis. Google ScholarDigital Library
- Hermanns, H., Wachter, B., and Zhang, L. 2008. Probabilistic CEGAR. In Proceedings of the International Conference on Computer Aided Verification. Google ScholarDigital Library
- Huth, M. 2004. An abstraction framework for mixed non-deterministic and probabilistic systems. In Validation of Stochastic Systems: A Guide to Current Research. Lecture Notes in Computer Science, vol. 2925. Springer, Berlin, Germany, 419--444.Google Scholar
- Huth, M. 2005. On finite-state approximants for probabilistic computation tree logic. Theoret. Comp. Sci. 346, 113--134. Google ScholarDigital Library
- Jonsson, B. and Larsen, K. G. 1991. Specification and refinement of probabilistic processes. In Proceedings of the IEEE Symposium on Logic in Computer Science. 266--277.Google Scholar
- Katoen, J.-P., Klink, D., Leucker, M., and Wolf, V. 2007. Three-valued abstraction for continuous-time Markov chains. In Proceedings of the International Conference on Computer Aided Verification. 311--324. Google ScholarDigital Library
- Kattenbelt, M., Kwiatkowska, M., Norman, G., and Parker, D. 2009. Abstraction refinement for probabilistic software. In Proceedings of the 10th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), N. Jones and M. Muller-Olm, Eds. Lecture Notes in Computer Science, vol. 5403. Springer, Berlin, Germany, 182--197. Google ScholarDigital Library
- Kemeny, J. and Snell, J. 1976. Denumerable Markov Chains. Springer-Verlag, Berlin, Germany.Google Scholar
- Kroening, D., Groce, A., and Clarke, E. 2004. Counterexample guided abstraction refinement via program execution. In Proceedings of the International Conference on Formal Engineering Methods. 224--238.Google Scholar
- Kwiatkowska, M., Norman, G., and Parker, D. 2006. Game-based abstraction for Markov decision processes. In Proceedings of the International Conference on Quantitative Evaluation of Systems. 157--166. Google ScholarDigital Library
- Lakhnech, Y., Bensalem, S., Berezin, S., and Owre, S. 2001. Incremental verification by abstraction. In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 98--112. Google ScholarDigital Library
- Majumdar, R., Henzinger, T., Jhala, R., and Sutre, G. 2002. Lazy abstraction. In Proceedings of the ACM Symposium on Principles of Programming Languages. 58--70. Google ScholarDigital Library
- McIver, A. and Morgan, C. 2004. Abstraction, Refinement and Proof for Probabilistic Systems. Springer, Berlin, Germany. Google ScholarDigital Library
- Monniaux, D. 2005. Abstract interpretation of programs as Markov decision processes. Sci. Comput. Program. 58, 179--205. Google ScholarDigital Library
- Norman, G. 2004. Analyzing randomized distributed algorithms. In Validation of Stochastic Systems: A Guide to Current Research. Lecture Notes in Computer Science, vol. 2925. Springer, Berlin, Germany, 384--418.Google Scholar
- Papoulis, A. and Pillai, S. U. 2002. Probability, Random Variables and Stochastic Processes. McGraw Hill, New York, NY.Google Scholar
- Rutten, J. M., Kwiatkowska, M., Norman, G., and Parker, D. 2004. Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems. AMS, Providence, RI.Google Scholar
- Segala, R. 2006. Probability and nondeterminism in operational models of concurrency. In Proceedings of the International Conference on Concurrency Theory. 64--78. Google ScholarDigital Library
- Segala, R. and Lynch, N. A. 1994. Probabilistic simulations for probabilistic processes. In Proceedings of the International Conference on Concurrency Theory. 481--496. Google ScholarDigital Library
- Segala, R. and Lynch, N. A. 1995. Probabilistic simulations for probabilistic processes. Nord. J. Comput. 2, 2, 250--273. Google ScholarDigital Library
- Shoham, S. and Grumberg, O. 2007. A game-based framework for CTL counterexamples and 3-valued abstraction-refinement. ACM Trans. Computat. Log. 9, 1. Google ScholarDigital Library
- Wachter, B., Zhang, L., and Hermanns, H. 2007. Probabilistic model checking modulo theories. In Proceedings of the International Conference on Quantitative Evaluation of Systems. Google ScholarDigital Library
- Zhang, L., Hermanns, H., Eisenbrand, F., and Jansen, D. N. 2007. Flow faster: efficient decision algorithms for probabilistic simulation. In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 155--170. Google ScholarDigital Library
Index Terms
- A counterexample-guided abstraction-refinement framework for markov decision processes
Recommendations
Counterexample-guided abstraction refinement for symbolic model checking
The state explosion problem remains a major hurdle in applying symbolic model checking to large hardware designs. State space abstraction, having been essential for verifying designs of industrial complexity, is typically a manual process, requiring ...
SAT-based counterexample-guided abstraction refinement
We describe new techniques for model checking in the counterexample-guided abstraction-refinement framework. The abstraction phase "hides" the logic of various variables, hence considering them as inputs. This type of abstraction may lead to "spurious" ...
A game-based abstraction-refinement framework for Markov decision processes
In the field of model checking, abstraction refinement has proved to be an extremely successful methodology for combating the state-space explosion problem. However, little practical progress has been made in the setting of probabilistic verification. ...
Reviews
Andre Platzer
In this paper, Chadha and Viswanathan study notions of counterexamples for finite-state Markov decision processes (MDPs). An appropriate definition of counterexamples is the most important ingredient for generalizing counterexample-guided abstraction refinement (CEGAR) from discrete systems to probabilistic systems. CEGAR is a technique introduced by Clarke et al. [1] that has been very successful in fighting the state explosion problem for model checking in discrete systems. This technique has become quite instrumental in software model checking. In discrete systems, a single execution trace violating the property of interest is all it takes to define a counterexample. This approach does not work in the probabilistic setting, however, because the probability of a single execution may be very small, and the corresponding probability mass not enough to constitute a counterexample to the probabilistic property. For probabilistic systems, earlier researchers had proposed sets of traces, tree-like counterexamples (with cycles), and discrete-time Markov chains as counterexamples. Chadha and Viswanathan show that some MDPs need more general counterexamples for complex properties (for example, nested probabilistic computational tree logic (PCTL) formulas and PCTL formulas with strict inequalities as probability bounds). Trace sets are inadequate as counterexamples for properties that are arbitrarily close to being true, but still false. Tree-like counterexamples cannot capture systems where the counterexample depends on multiple intertwined cycles, because those cannot be unraveled into a tree of cycles. The fact that discrete-time Markov chains are sufficient as counterexamples for single probability operators does not extend to nested probability operators. The authors propose MDPs as counterexamples to overcome these issues and show that MDPs are indeed always available as counterexamples. With a suitable definition of a counterexample in place, the paper goes on to lift basic CEGAR algorithms to the probabilistic case in a straightforward way, and proves their correctness. The paper generally assumes that the reader is familiar with PCTL and has an intuition for MDPs, but it otherwise introduces all required notions very carefully, and emphasizes proving the correctness of the presented approach. In the future, it would be interesting to see in more detail how MDPs and stochastic games compare in abstraction-refinement approaches for probabilistic systems. An implementation of the approach would very likely also shed more light on the steps in the probabilistic CEGAR loop that need practical advances to scale well. With a long cascade of improvements in CEGAR for discrete systems, the last word about efficient algorithms for CEGAR in the probabilistic case has most likely not been spoken yet. However, the authors develop the basics for successful probabilistic CEGAR, which can hardly work without having the right notion of counterexamples in place. Online Computing Reviews Service
Access critical reviews of Computing literature here
Become a reviewer for Computing Reviews.
Comments