Computing Conditional Probabilities: Implementation and Evaluation

Publikation: Beitrag in Buch/Konferenzbericht/Sammelband/GutachtenBeitrag in KonferenzbandBeigetragenBegutachtung

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

OriginalspracheEnglisch
TitelSoftware Engineering and Formal Methods
Redakteure/-innenAlessandro Cimatti, Marjan Sirjani
Herausgeber (Verlag)Springer, Berlin [u. a.]
Seiten349-366
Seitenumfang18
ISBN (Print)978-3-319-66196-4
PublikationsstatusVeröffentlicht - 2017
Peer-Review-StatusJa

Publikationsreihe

ReiheLecture Notes in Computer Science, Volume 10469
ISSN0302-9743

Konferenz

Titel15th International Conference on Software Engineering and Formal Methods
KurztitelSEFM 2017
Veranstaltungsnummer
Dauer4 - 8 September 2017
BekanntheitsgradInternationale Veranstaltung
Ort
StadtTrento
LandItalien

Externe IDs

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

Schlagworte

Schlagwörter

  • Conditional Probabilities, Implementation, Evaluation

Bibliotheksschlagworte