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

DOI Link

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

Details
Bibtex

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