Value Iteration for Stochastic Parity Games

Kittiphon Phalakarn; Ichiro Hasuo

Value Iteration for Stochastic Parity Games

Computer Science and Game Theory 2026-07-20 v1

Authors: Kittiphon Phalakarn , Ichiro Hasuo

Abstract

We present the first (bounded) value iteration algorithm for the quantitative analysis of stochastic parity games, a fundamental model for probabilistic verification with $\omega$ -regular objectives. Existing algorithms are based on strategy iteration, which repeatedly computes optimal strategies for one player while fixing the other, leading to high computational cost. Our algorithm instead operates directly on a lattice-theoretic characterization of winning probabilities, exploiting structural properties of (almost-sure qualitative) winning states under parity objectives. We prove correctness and convergence of the proposed algorithm.

Cite

@article{arxiv.2607.18355,
  title  = {Value Iteration for Stochastic Parity Games},
  author = {Kittiphon Phalakarn and Ichiro Hasuo},
  journal= {arXiv preprint arXiv:2607.18355},
  year   = {2026}
}