# Sound Value Iteration

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

## Key facts

- Cited by 6 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 13 Apr 2018.

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

- [Robust Markov Decision Processes: A Place Where AI and Formal Methods Meet](https://mlsanity.com/paper/2411.11451/) (2024)
- [Probabilistic Shielding for Safe Reinforcement Learning](https://mlsanity.com/paper/2503.07671/) (2025)
- [Under-Approximating Expected Total Rewards in POMDPs](https://mlsanity.com/paper/2201.08772/) (2022)
- [Stopping Criteria for Value Iteration on Stochastic Games with Quantitative Objectives](https://mlsanity.com/paper/2304.09930/) (2023)
- [Value Iteration with Guessing for Markov Chains and Markov Decision Processes](https://mlsanity.com/paper/2505.06769/) (2025)
- [Convex-Analytic View of Query Selection for Safety Verification of Markov Decision Processes](https://mlsanity.com/paper/2610.17541/) (2026)

## Abstract (arXiv)

Computing reachability probabilities is at the heart of probabilistic model checking. All model checkers compute these probabilities in an iterative fashion using value iteration. This technique approximates a fixed point from below by determining reachability probabilities for an increasing number of steps. To avoid results that are significantly off, variants have recently been proposed that converge from both below and above. These procedures require starting values for both sides. We present an alternative that does not require the a priori computation of starting vectors and that converges faster on many benchmarks. The crux of our technique is to give tight and safe bounds - whose computation is cheap - on the reachability probabilities. Lifting this technique to expected rewards is trivial for both Markov chains and MDPs. Experimental results on a large set of benchmarks show its scalability and efficiency.