High-level Counterexamples for Probabilistic Automata

TL;DR

This paper introduces a method to generate minimal and understandable counterexamples for probabilistic automata by identifying the smallest command subset causing errors, aiding manual debugging.

Contribution

It presents a novel approach to produce compact counterexamples by selecting minimal command subsets in probabilistic systems, improving interpretability over existing methods.

Findings

Identifies smallest command subsets causing errors

Simplifies counterexamples for better understandability

Enhances manual debugging of probabilistic models

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.