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

Christel Baier, Joachim Klein, Linda Leuschner, David Parker

Research output: Chapter in Book/Report/Conference proceedingConference contribution

21 Citations (Scopus)
260 Downloads (Pure)


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.
Original languageEnglish
Title of host publicationComputer Aided Verification
Subtitle of host publication29th International Conference, CAV 2017, Heidelberg, Germany, July 22-28, Proceedings
EditorsRupak Majumdar, Viktor Kunčak
Number of pages21
Publication statusPublished - Jul 2017
EventComputer Aided Verification, 29th International Conference - Heidelberg, Germany
Duration: 22 Jul 201728 Jul 2017

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


ConferenceComputer Aided Verification, 29th International Conference
Abbreviated titleCAV 2017


Dive into the research topics of 'Ensuring the Reliability of Your Model Checker: Interval Iteration for Markov Decision Processes'. Together they form a unique fingerprint.

Cite this