Advances in probabilistic model checking with PRISM: variable reordering, quantiles and weak deterministic Büchi automata
From International Center for Computational Logic
Advances in probabilistic model checking with PRISM: variable reordering, quantiles and weak deterministic Büchi automata
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
Joachim Klein, Christel Baier, Philipp Chrszon, Marcus Daum, Clemens Dubslaff, Sascha Klüppelholz, Steffen Märcker, David Müller
Advances in probabilistic model checking with PRISM: variable reordering, quantiles and weak deterministic Büchi automata
International Journal on Software Tools for Technology Transfer (STTT), 20(2):179--194, 2018
Advances in probabilistic model checking with PRISM: variable reordering, quantiles and weak deterministic Büchi automata
International Journal on Software Tools for Technology Transfer (STTT), 20(2):179--194, 2018
- KurzfassungAbstract
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. - Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science
@article{KBCDDKMM2018,
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 probabilistic model checking with {PRISM:} variable
reordering, quantiles and weak deterministic B{\"{u}}chi automata},
journal = {International Journal on Software Tools for Technology Transfer
(STTT)},
volume = {20},
number = {2},
year = {2018},
pages = {179--194},
doi = {10.1007/s10009-017-0456-3}
}