Family-Based Modeling and Analysis for Probabilistic Systems - Featuring ProFeat

Philipp ChrszonPhilipp Chrszon, Clemens DubslaffClemens Dubslaff, Sascha KlüppelholzSascha Klüppelholz, Christel BaierChristel Baier

DOI Link

Philipp Chrszon, Clemens Dubslaff, Sascha Klüppelholz, Christel Baier
Family-Based Modeling and Analysis for Probabilistic Systems - Featuring ProFeat
Proc. of the 19th International Conference on Fundamental Approaches to Software Engineering (FASE), volume 9633 of Lecture Notes in Computer Science, 287--304, 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-49665-7_17.

@inproceedings{CDKB2016,
  author    = {Philipp Chrszon and Clemens Dubslaff and Sascha Kl{\"{u}}ppelholz
               and Christel Baier},
  title     = {Family-Based Modeling and Analysis for Probabilistic Systems -
               Featuring {ProFeat}},
  booktitle = {Proc. of the 19th International Conference on Fundamental
               Approaches to Software Engineering (FASE)},
  series    = {Lecture Notes in Computer Science},
  volume    = {9633},
  publisher = {Springer},
  year      = {2016},
  pages     = {287--304},
  doi       = {10.1007/978-3-662-49665-7_17}
}