Computer Science – Software Engineering
Scientific paper
2008-07-08
Computer Science
Software Engineering
Scientific paper
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 {\it 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 non-probabilistic systems automatically, CEGAR has not been applied 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 paper, we address these issues, and present a CEGAR framework for Markov Decision Processes.
Chadha Rohit
Viswanthan Mahesh
No associations
LandOfFree
A Counterexample Guided Abstraction-Refinement Framework for Markov Decision Processes does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with A Counterexample Guided Abstraction-Refinement Framework for Markov Decision Processes, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and A Counterexample Guided Abstraction-Refinement Framework for Markov Decision Processes will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-268303