CEBug

| project staff | cooperation partners | project description |

For the correction of erroneous systems it is crucial to have counterexamples at hand. Counterexamples are system runs which lead to erroneous behavior. Previous research on the analysis of stochastic 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 stochastic 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 systems. We are going to demonstrate the practical applicability of our algorithms on a set of benchmarks.

This project is funded by the German Research Foundation (DFG).