Computing Conditional Probabilities: Implementation and Evaluation

Research output: Contribution to book/conference proceedings/anthology/reportConference contributionContributedpeer-review

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 languageEnglish
Title of host publicationSoftware Engineering and Formal Methods
EditorsAlessandro Cimatti, Marjan Sirjani
PublisherSpringer, Berlin [u. a.]
Pages349-366
Number of pages18
ISBN (print)978-3-319-66196-4
Publication statusPublished - 2017
Peer-reviewedYes

Publication series

SeriesLecture Notes in Computer Science, Volume 10469
ISSN0302-9743

Conference

Title15th International Conference on Software Engineering and Formal Methods
Abbreviated titleSEFM 2017
Conference number
Duration4 - 8 September 2017
Degree of recognitionInternational event
Location
CityTrento
CountryItaly

External IDs

Scopus 85029005035
ORCID /0000-0002-5321-9343/work/142236720

Keywords

Keywords

  • Conditional Probabilities, Implementation, Evaluation

Library keywords