CEBug: Counter Example Generation for Stochastic Systems using Bounded Model Checking

CEBug

Project 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 languages. We are going to demonstrate the practical applicability of our algorithms on a set of benchmarks.

Funding

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

Team

RWTH Aachen University, Germany

University of Freiburg, Germany

Student assistants