Computing Conditional Probabilities: Implementation and Evaluation
Research output: Contribution to book/Conference proceedings/Anthology/Report › Conference contribution › Contributed › peer-review
Contributors
Abstract
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.
Details
Original language | English |
---|---|
Title of host publication | Software Engineering and Formal Methods |
Editors | Alessandro Cimatti, Marjan Sirjani |
Publisher | Springer, Berlin [u. a.] |
Pages | 349-366 |
Number of pages | 18 |
ISBN (print) | 978-3-319-66196-4 |
Publication status | Published - 2017 |
Peer-reviewed | Yes |
Publication series
Series | Lecture Notes in Computer Science, Volume 10469 |
---|---|
ISSN | 0302-9743 |
Conference
Title | 15th International Conference on Software Engineering and Formal Methods |
---|---|
Abbreviated title | SEFM 2017 |
Conference number | |
Duration | 4 - 8 September 2017 |
Degree of recognition | International event |
Location | |
City | Trento |
Country | Italy |
External IDs
Scopus | 85029005035 |
---|---|
ORCID | /0000-0002-5321-9343/work/142236720 |
Keywords
Keywords
- Conditional Probabilities, Implementation, Evaluation