Counter Example Generation for Stochastic Systems using Bounded Model Checking (CEBug)

CEBugProject description

For the correction of erroneous systems it is crucial to have counterexamples at hand, i.e., system runs which lead to erroneous behavior.

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.


This project was funded 2010-2013 by the German Research Foundation (DFG) under the project number AB 461/1-1.



Erika Ábrahám
Joost-Pieter Katoen
Nils Jansen


Bernd Becker
Ralf Wimmer

Student assistants

Maik Scheffler
Matthias Volk
Andreas Vorpahl
Barna Zajzon