Algorithm and Strategy Construction for Sure-Almost-Sure Stochastic Parity Games

TL;DR

This paper introduces a recursive algorithm for constructing winning strategies in complex stochastic parity games, improving understanding of their structure and providing new bounds for specific subclasses.

Contribution

It presents a novel recursive approach to strategy construction in stochastic parity games, addressing limitations of previous exponential enumeration methods.

Findings

Algorithm constructs winning strategies effectively.

Provides new complexity bounds for special game classes.

Deepens understanding of the structure of stochastic parity games.

Abstract

We consider turn-based stochastic two-player games with a combination of a parity condition that must hold surely, that is in all possible outcomes, and of a parity condition that must hold almost-surely, that is with probability 1. The problem of deciding the existence of a winning strategy in such games is central in the framework of synthesis beyond worst-case where a hard requirement that must hold surely is combined with a softer requirement. Recent works showed that the problem is coNP-complete, and infinite-memory strategies are necessary in general, even in one-player games (i.e., Markov decision processes). However, memoryless strategies are sufficient for the opponent player. Despite these comprehensive results, the known algorithmic solution enumerates all memoryless strategies of the opponent, which is exponential in all cases, and does not construct a winning strategy when one exists. We present a recursive algorithm, based on a characterisation of the winning region, that gives a deeper insight into the problem. In particular, we show how to construct a winning strategy to achieve the combination of sure and almost-sure parity, and we derive new complexity and memory bounds for special classes of the problem, defined by fixing the index of either of the two parity conditions.