Significant Diagnostic Counterexamples in Probabilistic Model Checking

TL;DR

This paper introduces a new method for generating meaningful counterexamples in probabilistic model checking, grouping similar paths into witnesses that aid debugging of Markov models.

Contribution

It proposes a novel witness-based approach satisfying five key properties, reducing complex counterexample generation to a simpler reachability problem.

Findings

Witnesses are composed of paths similar outside strongly connected components.

The method effectively groups paths to improve debugging insights.

Counterexample generation is reduced to reachability analysis in acyclic Markov Chains.

Abstract

This paper presents a novel technique for counterexample generation in probabilistic model checking of Markov Chains and Markov Decision Processes. (Finite) paths in counterexamples are grouped together in witnesses that are likely to provide similar debugging information to the user. We list five properties that witnesses should satisfy in order to be useful as debugging aid: similarity, accuracy, originality, significance, and finiteness. Our witnesses contain paths that behave similar outside strongly connected components. This papers shows how to compute these witnesses by reducing the problem of generating counterexamples for general properties over Markov Decision Processes, in several steps, to the easy problem of generating counterexamples for reachability properties over acyclic Markov Chains.