High-level Counterexamples for Probabilistic Automata
This addresses the need for better debugging tools in probabilistic model checking, though it is incremental as it builds on existing command-based descriptions.
The paper tackles the problem of generating compact and understandable counterexamples for probabilistic automata in model checking, resulting in a method that identifies a smallest subset of commands causing errors and simplifies them for clarity.
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.