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.