We propose a way of presenting and computing 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 counterexample presented helps the user identify the underlying error in the system by means of an interactive game with the model checker. © 2009 Springer Berlin Heidelberg.
CITATION STYLE
Schmalz, M., Varacca, D., & Völzer, H. (2009). Counterexamples in probabilistic ltl model checking for markov chains. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5710 LNCS, pp. 587–602). https://doi.org/10.1007/978-3-642-04081-8_39
Mendeley helps you to discover research relevant for your work.