Significant Diagnostic Counterexamples in Probabilistic Model Checking

 

Miguel Andres (Radboud University Nijmegen, NL)

 

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
similarly outside strongly connected components.

Then, we show 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.