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

Rohit Chadha, Mahesh Viswanathan

Research output: Contribution to journalArticlepeer-review


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
Issue number1
StatePublished - Oct 2010


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

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science
  • Logic
  • Computational Mathematics


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

Cite this