The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Hierarchical Counterexamples for Discrete-Time Markov Chains
Nils Jansen, Erika Ábrahám, Jens Katelaan, Ralf Wimmer,
Joost-Pieter Katoen, Bernd Becker
AIB 2011-11
In this paper we introduce a novel counterexample generation approach
for discrete-time Markov chains (DTMCs) with two main advantages:
(1) We generate *abstract* counterexamples, which
can be refined in a *hierarchical* manner.
(2) We aim at minimizing the number of states involved in the
counterexamples, and compute a *critical subsystem* of the DTMC,
whose paths form a counterexample.
Experiments show that with our approach we can reduce the size of
counterexamples and the number of computation steps by orders of
magnitude.
