Computing Conditional Probabilities: Implementation and Evaluation

Aus International Center for Computational Logic
Wechseln zu:Navigation, Suche

Toggle side column

Computing Conditional Probabilities: Implementation and Evaluation

Steffen MärckerSteffen Märcker,  Christel BaierChristel Baier,  Joachim KleinJoachim Klein,  Sascha KlüppelholzSascha Klüppelholz
Steffen Märcker, Christel Baier, Joachim Klein, Sascha Klüppelholz
Computing Conditional Probabilities: Implementation and Evaluation
Proc. of the 15th International Conference on Software Engineering and Formal Methods (SEFM), volume 10469 of Lecture Notes in Computer Science, 349--366, 2017. Springer
  • KurzfassungAbstract
    Conditional probabilities and expectations are an important concept in the quantitative analysis of stochastic systems, e.g., to analyze the impact and cost of error handling mechanisms in rare failure scenarios or for a utility-analysis assuming an exceptional shortage of resources. This paper reports on the main features of an implementation of computation schemes for conditional probabilities in discrete-time Markov chains and Markov decision processes within the probabilistic model checker Prism and a comparative experimental evaluation. Our implementation has full support for computing conditional probabilities where both the objective and condition are given as linear temporal logic formulas, as well as specialized algorithms for reachability and other simple types of path properties. In the case of Markov chains we provide implementations for three alternative methods (quotient, scale and reset). We support Prism’s explicit and (semi-)symbolic engines. Besides comparative studies exploring the three dimensions (methods, engines, general vs. special handling), we compare the performance of our implementation and the probabilistic model checker Storm that provides facilities for conditional probabilities of reachability properties.
  • 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-319-66197-1_22.
@inproceedings{MBKK2017,
  author    = {Steffen M{\"{a}}rcker and Christel Baier and Joachim Klein and
               Sascha Kl{\"{u}}ppelholz},
  title     = {Computing Conditional Probabilities: Implementation and
               Evaluation},
  booktitle = {Proc. of the 15th International Conference on Software
               Engineering and Formal Methods (SEFM)},
  series    = {Lecture Notes in Computer Science},
  volume    = {10469},
  publisher = {Springer},
  year      = {2017},
  pages     = {349--366},
  doi       = {10.1007/978-3-319-66197-1_22}
}