Ensuring the Reliability of Your Model Checker: Interval Iteration for Markov Decision Processes

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

Abstract

Probabilistic model checking provides formal guarantees on quantitative properties such as reliability, performance or risk, so the accuracy of the numerical results that it returns is critical. However, recent results have shown that implementations of value iteration, a widely used iterative numerical method for computing reachability probabilities, can return results that are incorrect by several orders of magnitude. To remedy this, interval iteration, which instead converges simultaneously from both above and below, has been proposed. In this paper, we present interval iteration techniques for computing expected accumulated weights (or costs), a considerably broader class of properties. This relies on an efficient, mainly graph-based method to determine lower and upper bounds for extremal expected accumulated weights. To offset the additional effort of dual convergence, we also propose topological interval iteration, which increases efficiency using a model decomposition into strongly connected components. Finally, we present a detailed experimental evaluation, which highlights inaccuracies in standard benchmarks, rather than just artificial examples, and illustrates the feasibility of our techniques.

Details

OriginalspracheEnglisch
TitelComputer Aided Verification
Redakteure/-innenRupak Majumdar, Viktor Kunčak
Herausgeber (Verlag)Springer, Berlin [u. a.]
Seiten160-180
Seitenumfang21
ISBN (Print)978-3-319-63386-2
PublikationsstatusVeröffentlicht - 2017
Peer-Review-StatusJa

Publikationsreihe

ReiheLecture Notes in Computer Science, Volume 10426
ISSN0302-9743

Konferenz

Titel29th International Conference of Computer Aided Verification
KurztitelCAV 2017
Veranstaltungsnummer
Dauer24 - 29 Juli 2017
BekanntheitsgradInternationale Veranstaltung
Ort
StadtHeidelberg
LandDeutschland

Externe IDs

Scopus 85026738318
ORCID /0000-0002-5321-9343/work/142236721

Schlagworte

Schlagwörter

  • Reliability, Model Checking, Interval Iteration, Markov Decision Processes

Bibliotheksschlagworte