# Stopping Criteria for Value Iteration on Concurrent Stochastic Reachability and Safety Games

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 7 of its 52 references that are in the map.
- First posted on arXiv 27 May 2025.

## Builds on (most cited first, 7 of 7)

- [Verification of Markov Decision Processes using Learning Algorithms](https://mlsanity.com/paper/1402.2967/) (2014)
- [A Practitioner's Guide to MDP Model Checking Algorithms](https://mlsanity.com/paper/2301.10197/) (2023)
- [Value Iteration for Simple Stochastic Games: Stopping Criterion and Learning Algorithm](https://mlsanity.com/paper/1804.04901/) (2018)
- [Value Iteration for Long-run Average Reward in Markov Decision Processes](https://mlsanity.com/paper/1705.02326/) (2017)
- [Comparison of Algorithms for Simple Stochastic Games (Full Version)](https://mlsanity.com/paper/2008.09465/) (2020)
- [Stopping Criteria for Value Iteration on Stochastic Games with Quantitative Objectives](https://mlsanity.com/paper/2304.09930/) (2023)
- [Stopping Criteria for Value and Strategy Iteration on Concurrent Stochastic Reachability Games](https://mlsanity.com/paper/1909.08348/) (2019)

## Abstract (arXiv)

We consider two-player zero-sum concurrent stochastic games (CSGs) played on graphs with reachability and safety objectives. These include degenerate classes such as Markov decision processes or turn-based stochastic games, which can be solved by linear or quadratic programming; however, in practice, value iteration (VI) outperforms the other approaches and is the most implemented method. Similarly, for CSGs, this practical performance makes VI an attractive alternative to the standard theoretical solution via the existential theory of reals. VI starts with an under-approximation of the sought values for each state and iteratively updates them, traditionally terminating once two consecutive approximations are ε-close. However, this stopping criterion lacks guarantees on the precision of the approximation, which is the goal of this work. We provide bounded (a.k.a. interval) VI for CSGs: it complements standard VI with a converging sequence of over-approximations and terminates once the over- and under-approximations are ε-close.