Counterexample Generation for Discrete-Time Markov Chains using Bounded Model Checking

Ralf Wimmer (Universität Freiburg)

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.

In this talk I will show 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.