Advances in Symbolic Probabilistic Model Checking with PRISM

Joachim KleinJoachim Klein, Christel BaierChristel Baier, Philipp ChrszonPhilipp Chrszon, Marcus DaumMarcus Daum, Clemens DubslaffClemens Dubslaff, Sascha KlüppelholzSascha Klüppelholz, Steffen MärckerSteffen Märcker, David MüllerDavid Müller

DOI Link

Joachim Klein, Christel Baier, Philipp Chrszon, Marcus Daum, Clemens Dubslaff, Sascha Klüppelholz, Steffen Märcker, David Müller
Advances in Symbolic Probabilistic Model Checking with PRISM
Proc. of the 22th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 9636 of Lecture Notes in Computer Science, 349--366, 2016. Springer

Details
Bibtex

KurzfassungAbstract
For modeling and reasoning about complex systems, symbolic methods provide a prominent way to tackle the state explosion problem. It is well known that for symbolic approaches based on binary decision diagrams (BDD), the ordering of BDD variables plays a crucial role for compact representations and efficient computations. We have extended the popular probabilistic model checker PRISM with support for automatic variable reordering in its multi-terminal-BDD-based engines and report on benchmark results. Our extensions additionally allow the user to manually control the variable ordering at a finer-grained level. Furthermore, we present our implementation of the symbolic computation of quantiles and support for multi-reward-bounded properties, automata specifications and accepting end component computations for Streett conditions.
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-662-49674-9_20.

@inproceedings{KBCDDKMM2016,
  author    = {Joachim Klein and Christel Baier and Philipp Chrszon and Marcus
               Daum and Clemens Dubslaff and Sascha Kl{\"{u}}ppelholz and
               Steffen M{\"{a}}rcker and David M{\"{u}}ller},
  title     = {Advances in Symbolic Probabilistic Model Checking with {PRISM}},
  booktitle = {Proc. of the 22th International Conference on Tools and
               Algorithms for the Construction and Analysis of Systems (TACAS)},
  series    = {Lecture Notes in Computer Science},
  volume    = {9636},
  publisher = {Springer},
  year      = {2016},
  pages     = {349--366},
  doi       = {10.1007/978-3-662-49674-9_20}
}