Subproject

S3

Categories

Model checker / solver for probabilistic systems

Overview

(S)SBMC generates counterexamples for probabilistic systems, namely Discrete-Time Markov Chains (DTMCs) and Markov Reward Models (MRMs) with discrete-time. This is done by computing a set of paths which fulfil a given property. The total probability of this set exceeds a given probability bound. The basic computation is done with Bounded Model Checking using the SAT-solver MiniSat (in case of SBMC) or the SMT-solver Yices (in case of SSBMC). There exist several features:

- Loop Detection speeds up the computation,

- Bisimulation Minimization downsizes the system,

- Path Conversion converts minimized paths back to the original ones.

The SMT-based variant SSBMC is able to find paths with a higher probability first, thus generating smaller counterexamples than with SAT. SSBMC also allows to generate counterexamples for MRMs. In case of the latter, the search space might be restricted to a given reward interval, so that only paths with a reward within the interval are considered.

Publications

B. Braitling, R. Wimmer, B. Becker, N. Jansen, and E. Ábrahám. Counterexample generation for Markov chains using SMT-based bounded model checking. In Roberto Bruni and Jürgen Dingel, editors, Proceedings of the 13th IFIP International Conference on Formal Methods for Open Object-based Distributed Systems (FMOODS) / 31st IFIP International Conference on FORmal TEchniques for Networked and Distributed Systems (FORTE), volume 6722 of Lecture Notes in Computer Science, pages 75-89, 2011.

R. Wimmer, B. Braitling, and B. Becker. Counterexample generation for discrete-time Markov chains using bounded model checking. In Neil D. Jones and Markus Müller-Olm, editors, Proceedings of the 10th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), number 5403 in Lecture Notes in Computer Science (LNCS), pages 366-380, 2009

Benchmarks

Contract Signing Protocol, Crowds Protocol, Synchronous Leader Election Protocol, Self-stabilizing Minimal Spanning-Tree Algorithm

Download

Click here for the binary.

Manual

Just type ./sbmc (respectively ./ssbmc) to see how the tool can be used and to receive information about the available options.

Status

Prototype