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 language | English |
---|---|
Title of host publication | Tools and Algorithms for the Construction and Analysis of Systems |
Subtitle of host publication | 29th 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 |
Editors | Sriram Sankaranarayanan, Natasha Sharygina |
Publisher | Springer Nature |
Pages | 469-488 |
Number of pages | 20 |
ISBN (Electronic) | 978-3-031-30823-9 |
ISBN (Print) | 978-3-031-30822-2 |
DOIs | |
Publication status | Published - 22 Apr 2023 |
Event | 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2023 - Paris, France Duration: 22 Apr 2023 → 27 Apr 2023 Conference number: 29 |
Publication series
Name | Lecture Notes in Computer Science |
---|---|
Publisher | Springer |
Volume | 13993 |
Conference
Conference | 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2023 |
---|---|
Abbreviated title | TACAS 2023 |
Country/Territory | France |
City | Paris |
Period | 22/04/23 → 27/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.