2011-11: Hierarchical Counterexamples for Discrete-Time Markov Chains
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.
participants (1)
-
Carsten Fuhs