# A Practitioner's Guide to MDP Model Checking Algorithms

arXiv: https://arxiv.org/abs/2301.10197 · HTML: https://mlsanity.com/paper/2301.10197/

## Key facts

- Cited by 10 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 24 Jan 2023.

## Built on by (most cited first, 10 of 10)

- [Robust Markov Decision Processes: A Place Where AI and Formal Methods Meet](https://mlsanity.com/paper/2411.11451/) (2024)
- [Playing Games with your PET: Extending the Partial Exploration Tool to Stochastic Games](https://mlsanity.com/paper/2405.03885/) (2024)
- [Stopping Criteria for Value Iteration on Stochastic Games with Quantitative Objectives](https://mlsanity.com/paper/2304.09930/) (2023)
- [Graph-Based Reductions for Parametric and Weighted MDPs](https://mlsanity.com/paper/2305.05739/) (2023)
- [Constrained and Robust Policy Synthesis with Satisfiability-Modulo-Probabilistic-Model-Checking](https://mlsanity.com/paper/2511.08078/) (2025)
- [Formally Verified Approximate Policy Iteration](https://mlsanity.com/paper/2406.07340/) (2024)
- [Value Iteration with Guessing for Markov Chains and Markov Decision Processes](https://mlsanity.com/paper/2505.06769/) (2025)
- [Stopping Criteria for Value Iteration on Concurrent Stochastic Reachability and Safety Games](https://mlsanity.com/paper/2505.21087/) (2025)
- [dtControl2+varepsilon: Trading Optimality for Explainability in MDPs via Decision Trees](https://mlsanity.com/paper/2607.25925/) (2026)
- [Convex-Analytic View of Query Selection for Safety Verification of Markov Decision Processes](https://mlsanity.com/paper/2610.17541/) (2026)

## Abstract (arXiv)

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 optimisations 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.