A classic solution technique for Markov decision processes (MDP) and stochastic games (SG) is value iteration (VI). Due to its good practical performance, this approximative approach is typically preferred over exact techniques, even though no practical bounds on the imprecision of the result could be given until recently: Over the past decade, different works derived stopping criteria, indicating when the precision reaches the desired level, for various settings, however each specialized to a specific objective and often with ad-hoc solutions. We provide a unified theoretical solution to this problem by isolating objective-specific subroutines as well as identify objective-independent concepts. These structural concepts, while surprisingly simple, form the very essence of the unified solution: We simply need to ask "Should I stay or should I go?".

Moreover, we also implement and extend this theoretical foundation in version 2.0 of the Partial Exploration Tool (PET2), adding support for stochastic games. Thereby, PET2 is the first tool implementing a sound and efficient approach for solving stochastic games with reachability/safety and mean payoff objectives. We complement this approach by developing and implementing a partial-exploration based variant for all three objectives. Our experimental evaluation shows that PET2 offers the most efficient partial-exploration based algorithm and is the most viable tool on SGs, even outperforming unsound tools.

The theory was presented at LICS 2023 and the tool at CAV 2024 (tool paper, distinguished paper award). The presentation is intended to be given by both authors and aims to cover both theory and practice.