# High-level Counterexamples for Probabilistic Automata

arXiv: https://arxiv.org/abs/1305.5055 · HTML: https://mlsanity.com/paper/1305.5055/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 22 May 2013.

## Built on by (most cited first, 2 of 2)

- [Inductive Synthesis for Probabilistic Programs Reaches New Horizons](https://mlsanity.com/paper/2101.12683/) (2021)
- [Probabilistic Counterexample Guidance for Safer Reinforcement Learning (Extended Version)](https://mlsanity.com/paper/2307.04927/) (2023)

## Abstract (arXiv)

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.