Stochastic Games with Synchronizing Objectives

TL;DR

This paper studies two-player stochastic games with synchronizing objectives, providing algorithms to determine winning states under various conditions, and establishing complexity bounds that extend known results from simpler models.

Contribution

It introduces algorithms for synchronizing objectives in stochastic games, analyzes their complexity, and handles the challenges posed by imperfect information and stochasticity.

Findings

Decidable algorithms for all synchronizing modes.

Complexity results: PSPACE-complete and PTIME-complete cases.

Finite-memory strategies are insufficient for some objectives.

Abstract

We consider two-player stochastic games played on a finite graph for infinitely many rounds. Stochastic games generalize both Markov decision processes (MDP) by adding an adversary player, and two-player deterministic games by adding stochasticity. The outcome of the game is a sequence of distributions over the states of the game graph. We consider synchronizing objectives, which require the probability mass to accumulate in a set of target states, either always, once, infinitely often, or always after some point in the outcome sequence; and the winning modes of sure winning (if the accumulated probability is equal to 1) and almost-sure winning (if the accumulated probability is arbitrarily close to 1). We present algorithms to compute the set of winning distributions for each of these synchronizing modes, showing that the corresponding decision problem is PSPACE-complete for synchronizing once and infinitely often, and PTIME-complete for synchronizing always and always after some point. These bounds are remarkably in line with the special case of MDPs, while the algorithmic solution and proof technique are considerably more involved, even for deterministic games. This is because those games have a flavour of imperfect information, in particular they are not determined and randomized strategies need to be considered, even if there is no stochastic choice in the game graph. Moreover, in combination with stochasticity in the game graph, finite-memory strategies are not sufficient in general (for synchronizing infinitely often).