Counterexamples in Probabilistic LTL Model Checking for Markov Chains

We propose how to present and compute a counterexample in probabilistic LTL model checking for discrete-time Markov chains. In qualitative probabilistic model checking, we present a counterexample as a pair (α,γ) where α,γ are finite words such that all paths that extend α and have infinitely many occurrences of γ violate the specification. In quantitative probabilistic model checking, we present a counterexample as a pair (W,R) where W is a set of such finite words α and R is a set of such finite words γ. Moreover, we suggest how the presented counterexample helps the user to identify the underlying error in the system through an interactive game with the model checker.

• Type: Conference
• Year: 2009
• Where: CONCUR
• Authors: Matthias Schmalz, Daniele Varacca, Hagen Völzer
• Keywords: CONCUR 2009, Distributed And Parallel Computing, Model Checking, Probabilistic Model, finite Words