(S)SBMC

| Beteiligte Mitarbeiter | Beschreibung | Benchmarks | Publikationen |

(S)SBMC berechnet Gegenbeispiele für probabilistische Systeme in Form von Markov-Ketten mit diskreter Zeit (DTMCs) oder Markov Reward-Modellen (MRMs) mit diskreter Zeit. Es wird eine Menge von Pfaden berechnet, die eine bestimmte Eigenschaft erfüllen. Die Gesamt-Wahrscheinlichkeit dieser Menge liegt über einer gegebenen Wahrscheinlichkeitsschranke. Die Berechnung basiert auf Bounded Model Checking, wobei entweder der SAT-Solver MiniSat (bei SBMC) oder der SMT-Solver Yices (bei SSBMC) verwendet wird. Es gibt einige zusätzliche Funktionen:
- Schleifenerkennung beschleunigt die Berechnung
- Bisimulationsminimierung verkleinert das System
- Pfadkonvertierung wandelt minimierte Pfade um in Original-Pfade.
Die SMT-basierte Variante SSBMC ermöglicht es, Pfade mit höherer Wahrscheinlichkeit zuerst zu finden, wodurch ein kleineres Gegenbeispiel berechnet werden kann als mit SAT. SSBMC ist außerdem in der Lage, Gegenbeispiele für MRMs zu berechnen. In diesem Fall kann der Suchraum auf ein gegebenes Reward-Intervall beschränkt werden, so dass nur noch Pfade mit einem Reward innerhalb dieses Intervalls betrachtet werden.

- 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/