A Counterexample-Guided Abstraction-Refinement Framework for Markov Decision Processes

作者：Chadha Rohit^*; Viswanathan Mahesh

来源：ACM Transactions on Computational Logic, 2010, 12(1): 1.

DOI：10.1145/1838552.1838553

• Verification
• Counterexamples
• abstraction
• refinement
• model checking
• Markov decision processes

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.

• 出版日期2010-10
• 单位INRIA