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

DOI10.1145/1838552.1838553MaRDI QIDQ2946618zbMATH OpenOpenAlexWikidataFDO

Authors Rohit Chadha, Mahesh Viswanathan

Publication date 17 September 2015

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/0807.1173

zbMATH Keywords

abstractionCounterexamplesMarkov decision processesmodel checkingrefinement

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Markov and semi-Markov decision processes (90C40)

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 {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.

Recommendations

• Probabilistic CEGAR
• A game-based abstraction-refinement framework for Markov decision processes
• scientific article; zbMATH DE number 1670775
• Abstract Counterexamples for Non-disjunctive Abstractions
• scientific article; zbMATH DE number 2038762

Cited in

(16)

• Counterexample explanation by learning small strategies in Markov decision processes
• Abstract model repair for probabilistic systems
• Bayesian statistical model checking with application to Stateflow/Simulink verification
• On Abstraction of Probabilistic Systems
• Probabilistic CEGAR
• A Probabilistic Learning Approach for Counterexample Guided Abstraction Refinement
• Abstract Counterexamples for Non-disjunctive Abstractions
• Minimal counterexamples for linear-time probabilistic verification
• scientific article; zbMATH DE number 2038762 (Why is no real title available?)
• Counterexample-guided Cartesian abstraction refinement for classical planning
• Farkas certificates and minimal witnesses for probabilistic reachability constraints
• Counterexample generation for discrete-time Markov models: an introductory survey
• A game-based abstraction-refinement framework for Markov decision processes
• Counterexample-driven synthesis for probabilistic program sketches
• CEGAR for compositional analysis of qualitative properties in Markov decision processes
• Latticed \(k\)-induction with an application to probabilistic programs

This page was built for publication: A counterexample-guided abstraction-refinement framework for Markov decision processes

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2946618)