- Titel
- Advances in probabilistic model checking with PRISM
- Untertitel
- Variable reordering, quantiles and weak deterministic Büchi automata
- Zitierfähige Url:
- https://nbn-resolving.org/urn:nbn:de:bsz:14-qucosa2-742658
- Quellenangabe
- International Journal on Software Tools for Technology Transfer
Erscheinungsjahr: 2018
Jahrgang: 20
Heft: 2
Seiten: 179-194
E-ISSN: 1433-2787 - Erstveröffentlichung
- 2018
- Abstract (EN)
- The popular model checker PRISM has been successfully used for the modeling and analysis of complex probabilistic systems. As one way to tackle the challenging state explosion problem, PRISM supports symbolic storage and manipulation using multi-terminal binary decision diagrams for representing the models and in the computations. However, it lacks automated heuristics for variable reordering, even though it is well known that the order of BDD variables plays a crucial role for compact representations and efficient computations. In this article, we present a collection of extensions to PRISM. First, we provide support for automatic variable reordering within the symbolic engines of PRISM and allow users to manually control the variable ordering at a fine-grained level. Second, we provide extensions in the realm of reward-bounded properties, namely symbolic computations of quantiles in Markov decision processes and, for both the explicit and symbolic engines, the approximative computation of quantiles for continuous-time Markov chains as well as support for multi-reward-bounded properties. Finally, we provide an implementation for obtaining minimal weak deterministic Büchi automata for the obligation fragment of linear temporal logic (LTL), with applications for expected accumulated reward computations with a finite horizon given by a co-safe LTL formula.
- Andere Ausgabe
- Zuerst erschienen in 'International Journal on Software Tools for Technology Transfer' bei Springer Link.
DOI: 10.1007/s10009-017-0456-3 - Freie Schlagwörter (DE)
- Formale Methoden, Modellprüfung
- Freie Schlagwörter (EN)
- formal methods, model checking
- Klassifikation (DDC)
- 004
- Verlag
- Springer, Berlin
- Version / Begutachtungsstatus
- angenommene Version / Postprint / Autorenversion
- URN Qucosa
- urn:nbn:de:bsz:14-qucosa2-742658
- Veröffentlichungsdatum Qucosa
- 30.03.2021
- Dokumenttyp
- Artikel
- Sprache des Dokumentes
- Englisch
- Lizenz / Rechtehinweis
