March 27 – 30 , 2011, Event 11132

Counterexamples for Stochastic Systems


Erika Abraham (RWTH Aachen, DE)
Bernd Becker (Universität Freiburg, DE)
Nils Jansen (RWTH Aachen, DE)
Ralf Wimmer (Universität Freiburg, DE)

For support, please contact

Heike Clemens


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.

Online Publications

We offer several possibilities to publish the results of your event. Please contact publishing(at) if you are interested.

Dagstuhl's Impact

Please inform us when a publication was published as a result from your seminar. These publications are listed in the category Dagstuhl's Impact and are presented on a special shelf in the library.