A Practitioner's Guide to MDP Model Checking Algorithms

Arnd Hartmanns, Sebastian Junges, Tim Quatmann, Maximilian Weininger*

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

5 Citations (Scopus)
74 Downloads (Pure)

Abstract

Model checking undiscounted reachability and expected-reward properties on Markov decision processes (MDPs) is key for the verification of systems that act under uncertainty. Popular algorithms are policy iteration and variants of value iteration; in tool competitions, most participants rely on the latter. These algorithms generally need worst-case exponential time. However, the problem can equally be formulated as a linear program, solvable in polynomial time. In this paper, we give a detailed overview of today’s state-of-the-art algorithms for MDP model checking with a focus on performance and correctness. We highlight their fundamental differences, and describe various optimizations and implementation variants. We experimentally compare floating-point and exact-arithmetic implementations of all algorithms on three benchmark sets using two probabilistic model checkers. Our results show that (optimistic) value iteration is a sensible default, but other algorithms are preferable in specific settings. This paper thereby provides a guide for MDP verification practitioners—tool builders and users alike.
Original languageEnglish
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems
Subtitle of host publication29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Paris, France, April 22–27, 2023, Proceedings, Part I
EditorsSriram Sankaranarayanan, Natasha Sharygina
PublisherSpringer Nature
Pages469-488
Number of pages20
ISBN (Electronic)978-3-031-30823-9
ISBN (Print)978-3-031-30822-2
DOIs
Publication statusPublished - 22 Apr 2023
Event29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2023 - Paris, France
Duration: 22 Apr 202327 Apr 2023
Conference number: 29

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume13993

Conference

Conference29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2023
Abbreviated titleTACAS 2023
Country/TerritoryFrance
CityParis
Period22/04/2327/04/23

Keywords

  • This work was part of the MISSION (Models in Space Systems: Integration, Operation, and Networking) project, funded by the European Union’s Horizon 2020 research and innovation programme under Marie Skłodowska-Curie Actions grant number 101008233.

Fingerprint

Dive into the research topics of 'A Practitioner's Guide to MDP Model Checking Algorithms'. Together they form a unique fingerprint.

Cite this