Sciweavers

CORR
2008
Springer

A Counterexample Guided Abstraction-Refinement Framework for Markov Decision Processes

13 years 11 months ago
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...
Rohit Chadha, Mahesh Viswanathan
Added 09 Dec 2010
Updated 09 Dec 2010
Type Journal
Year 2008
Where CORR
Authors Rohit Chadha, Mahesh Viswanathan
Comments (0)