(S)SBMC

| project staff | description | benchmarks | publications |

(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.

- Contract Signing Protocol (*)(**)
- Crowds Protocol (*)(**)
- Synchronous Leader Election Protocol (*)(**)
- Self-stabilizing Minimal Spanning-Tree (**)

(*) http://www.prismmodelchecker.org/casestudies/index.php
(**) http://www.avacs.org/benchmarks/