Previous research on the analysis of probabilistic systems concentrated on the computation of the probability with which runs of a stochastic system satisfy a given property. If this probability does not lie within the admissible bounds, the available model checking algorithms provide the probability value, but no counterexample. First steps towards counterexample generation for probabilistic systems consider discrete-time Markov chains, a relatively simple class of  stochastic systems.
The goal of this project is, on the one hand, to improve the available technologies for counterexample generation and, on the other hand, to develop and implement algorithms for more expressive properties and for richer modeling languagessystems. We are going to demonstrate the practical applicability of our algorithms on a set of benchmarks.