Counterexamples are of utmost importance for the correction of erroneous systems. For many important classes of properties, model checking algorithms on digital circuits are able to generate counterexamples without additional effort. For stochastic systems, however, the situation is different: Computing probabilities for model checking is done by solving appropriate equation systems. If a property is violated, the user does not obtain any information about the reasons of violation. Therefore intensive research on probabilistic counterexamples has been initiated during the last few years.

During our Dagstuhl meeting we want to discuss and work on the combination of different approaches for counterexample generation for Markov chains which were developed at the RWTH Aachen University and the University of Freiburg.