A counterexample-guided abstraction-refinement framework for markov decision processes

Rohit Chadha, Mahesh Viswanathan

Research output: Contribution to journalArticlepeer-review

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 nonprob- abilistic 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.

Original languageEnglish (US)
Article number1
JournalACM Transactions on Computational Logic
Volume12
Issue number1
DOIs
StatePublished - Oct 2010

Keywords

  • Abstraction
  • Counterexamples
  • Markov decision processes
  • Model checking
  • Refinement

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)
  • Logic
  • Computational Mathematics

Fingerprint Dive into the research topics of 'A counterexample-guided abstraction-refinement framework for markov decision processes'. Together they form a unique fingerprint.

Cite this