Sciweavers

Share
CONCUR
2009
Springer

Counterexamples in Probabilistic LTL Model Checking for Markov Chains

10 years 4 months ago
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.
Matthias Schmalz, Daniele Varacca, Hagen Völz
Added 26 May 2010
Updated 26 May 2010
Type Conference
Year 2009
Where CONCUR
Authors Matthias Schmalz, Daniele Varacca, Hagen Völzer
Comments (0)
books