The revised practitioner’s guide to MDP model checking algorithms Hartmanns, Arnd Junges, Sebastian Quatmann, Tim Weininger, Maximilian ; https://orcid.org/0000-0002-0163-2152 Quantitative model checking Markov decision process Linear programming Value iteration Policy iteration ddc:000 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. Springer Nature 2026 info:eu-repo/semantics/article doc-type:article text http://purl.org/coar/resource_type/c_2df8fbb1 https://research-explorer.ista.ac.at/record/21661 Hartmanns A, Junges S, Quatmann T, Weininger M. The revised practitioner’s guide to MDP model checking algorithms. <i>International Journal on Software Tools for Technology Transfer</i>. 2026. doi:<a href="https://doi.org/10.1007/s10009-026-00848-y">10.1007/s10009-026-00848-y</a> eng info:eu-repo/semantics/altIdentifier/doi/10.1007/s10009-026-00848-y info:eu-repo/semantics/altIdentifier/issn/1433-2779 info:eu-repo/semantics/altIdentifier/e-issn/1433-2787 info:eu-repo/semantics/openAccess