@InProceedings{wimmer-et-al-vmcai-2009,
author = "Ralf Wimmer and Bettina Braitling and Bernd Becker",
title = "Counterexample Generation for Discrete-time
{Markov} Chains using Bounded Model Checking",
booktitle = "Proceedings of the 10\textsuperscript{th} International
Conference on Verification, Model Checking, and
Abstract Interpretation (VMCAI)",
address = "Savannah, GA, USA",
month = jan,
year = "2009",
editor = "Neil D. Jones and Markus M{\"u}ller-Olm",
series = "Lecture Notes in Computer Science",
number = "5403",
pages = "366--380",
isbn-13 = "978-3-540-93899-6",
isbn-10 = "3-540-93899-0",
publisher = "Springer-Verlag",
abstract = "Since its introduction in 1999, bounded model checking
has gained industrial relevance for detecting errors
in digital and hybrid systems. One of the main reasons
for this is that it always provides a counterexample
when an erroneous execution trace is found. Such a
counterexample can guide the designer while debugging
the system.\par
In this paper we are investigating how bounded model
checking can be applied to generate counterexamples
for a different kind of model---namely discrete-time
Markov chains. Since in this case counterexamples in general
do not consist of a single path to a safety-critical
state, but of a potentially large set of paths,
novel optimization techniques like loop-detection
are applied not only to speed-up the counterexample
computation, but also to reduce the size of the
counterexamples significantly. We report on some
experiments which demonstrate the practical applicability
of our method.",
citedby = "Alj09,FHPW09,Han09,SVV09",
}