The revised practitioner’s guide to MDP model checking algorithms

article The revised practitioner’s guide to MDP model checking algorithms epub_ahead yes Arnd Hartmanns author Sebastian Junges author Tim Quatmann author Maximilian Weininger author 02ab0197-cc70-11ed-ab61-918e71f568810000-0002-0163-2152 KrCh department IST-BRIDGE: International postdoctoral program project Model checking undiscounted reachability and expected-reward properties on Markov decision processes (MDPs) are 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 programme, 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. https://creativecommons.org/licenses/by/4.0/ Springer Nature2026 eng Quantitative model checkingMarkov decision processLinear programmingValue iterationPolicy iteration International Journal on Software Tools for Technology Transfer 1433-2779 1433-278710.1007/s10009-026-00848-y https://research-explorer.ista.ac.at/record/21668 Hartmanns A, Junges S, Quatmann T, Weininger M. The revised practitioner’s guide to MDP model checking algorithms. International Journal on Software Tools for Technology Transfer. 2026. doi:<a href="https://doi.org/10.1007/s10009-026-00848-y">10.1007/s10009-026-00848-y</a> A. Hartmanns, S. Junges, T. Quatmann, M. Weininger, International Journal on Software Tools for Technology Transfer (2026). Hartmanns, Arnd, et al. “The Revised Practitioner’s Guide to MDP Model Checking Algorithms.” International Journal on Software Tools for Technology Transfer, Springer Nature, 2026, doi:<a href="https://doi.org/10.1007/s10009-026-00848-y">10.1007/s10009-026-00848-y</a>. Hartmanns A, Junges S, Quatmann T, Weininger M. 2026. The revised practitioner’s guide to MDP model checking algorithms. International Journal on Software Tools for Technology Transfer. A. Hartmanns, S. Junges, T. Quatmann, and M. Weininger, “The revised practitioner’s guide to MDP model checking algorithms,” International Journal on Software Tools for Technology Transfer. Springer Nature, 2026. Hartmanns, Arnd, Sebastian Junges, Tim Quatmann, and Maximilian Weininger. “The Revised Practitioner’s Guide to MDP Model Checking Algorithms.” International Journal on Software Tools for Technology Transfer. Springer Nature, 2026. <a href="https://doi.org/10.1007/s10009-026-00848-y">https://doi.org/10.1007/s10009-026-00848-y</a>. Hartmanns, A., Junges, S., Quatmann, T., & Weininger, M. (2026). The revised practitioner’s guide to MDP model checking algorithms. International Journal on Software Tools for Technology Transfer. Springer Nature. <a href="https://doi.org/10.1007/s10009-026-00848-y">https://doi.org/10.1007/s10009-026-00848-y</a> 216612026-04-05T22:01:32Z2026-04-07T09:52:54Z