Computing Conditional Probabilities: Implementation and Evaluation
Aus International Center for Computational Logic
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
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
@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}
}