Counterexample Generation for Discrete-TimeMarkov Chains Using Bounded Model Checking

摘要

Since its introduction in 1999, bounded model checking hasgained industrial relevance for detecting errors in digital and hybridsystems. One of the main reasons for this is that it always providesa counterexample when an erroneous execution trace is found. Such acounterexample can guide the designer while debugging the system. In this paper we are investigating how bounded model checking canbe applied to generate counterexamples for a different kind of model—namely discrete-time Markov chains. Since in this case counterexamplesin general do not consist of a single path to a safety-critical state, but ofa potentially large set of paths, novel optimization techniques like loop-detection are applied not only to speed-up the counterexample compu-tation, but also to reduce the size of the counterexamples significantly.We report on some experiments which demonstrate the practical appli-cability of our method.