@inProceedings{ braitling-et-al-mbmv-2011,
author = "Bettina Braitling and Ralf Wimmer and Bernd Becker
and Nils Jansen and Erika {\'A}brah{\'a}m",
title = "{SMT}-based Counterexample Generation for {Markov} Chains",
year = "2011",
month = mar,
pages = "19--28",
isbn = "978-3-00-033820-5",
publisher = "Offis Oldenburg",
editor = "Frank Oppenheimer",
booktitle = "Proceedings of the 14\textsuperscript{th} Workshop ``Methoden und
Beschreibungssprachen zur Modellierung und
Verifikation von Schaltungen und Systemen'' (MBMV)",
address = "Oldenburg, Germany",
abstract = "Counterexamples are a highly important feature of the
model checking process. In contrast to, e.\,g., digital circuits where
counterexamples typically consist of a single path leading to a
critical state of the system, in the probabilistic setting,
counterexamples may consist of a large number of paths. In order to
be able to handle large systems and to use the capabilities of modern
SAT-solvers, bounded model checking (BMC) for discrete-time Markov
chains was established.\par
In this paper we introduce the usage of SMT-solving over the reals
for the BMC procedure. SMT-solving, extending SAT with theories, leads
in this context on the one hand to a convenient way to express
conditions on the probability of certain paths and on the other hand
to handle Markov Reward models. The former can be used to find paths with
high probability first. This leads to more compact counterexamples.
We report on some experiments, which show promising results.",
}