A Counterexample Guided Abstraction-Refinement Framework for Markov Decision Processes

rexample Guided Abstraction-Refinement Framework for Markov Decision Processes ROHIT CHADHA and MAHESH VISWANATHAN Dept. of Computer Science, University of Illinois at Urbana-Champaign 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 bstraction-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 til either an abstraction proves the correctness of the system or a valid counterexample is generated. While CEGAR has been successfully used in verifying non-probabilistic 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 g...

• Type: Journal
• Year: 2008
• Where: CORR
• Authors: Rohit Chadha, Mahesh Viswanathan
• Keywords: Abstraction, CORR 2008, Counterexamples, Education, Markov Decision