High-level counterexamples for probabilistic automata
From MaRDI portal
Abstract: Providing compact and understandable counterexamples for violated system properties is an essential task in model checking. Existing works on counterexamples for probabilistic systems so far computed either a large set of system runs or a subset of the system's states, both of which are of limited use in manual debugging. Many probabilistic systems are described in a guarded command language like the one used by the popular model checker PRISM. In this paper we describe how a smallest possible subset of the commands can be identified which together make the system erroneous. We additionally show how the selected commands can be further simplified to obtain a well-understandable counterexample.
Recommendations
Cited in
(10)- Fast debugging of PRISM models
- Counterexample-guided inductive synthesis for probabilistic systems
- A Debugging Game for Probabilistic Models
- Minimal counterexamples for linear-time probabilistic verification
- scientific article; zbMATH DE number 7204940 (Why is no real title available?)
- An oracle-guided approach to constrained policy synthesis under uncertainty
- Inductive synthesis for probabilistic programs reaches new horizons
- Counterexamples in Probabilistic LTL Model Checking for Markov Chains
- Generating counterexamples for quantitative safety specifications in probabilistic B
- A practitioner's guide to MDP model checking algorithms
This page was built for publication: High-level counterexamples for probabilistic automata
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5246720)
