Expectation in Stochastic Games with Prefix-independent Objectives

TL;DR

This paper presents a reduction method for computing the expected value of prefix-independent objectives in stochastic games, linking it to almost-sure satisfaction problems and applying it to window mean-payoff measures.

Contribution

It introduces a generic reduction from expectation problems to almost-sure satisfaction problems and analyzes memory requirements for optimal strategies in stochastic games.

Findings

Reduction from expectation to almost-sure satisfaction problems

Memory bounds for optimal strategies in stochastic games

Decidability of expected window mean-payoff in certain cases

Abstract

Stochastic two-player games model systems with an environment that is both adversarial and stochastic. In this paper, we study the expected value of bounded quantitative prefix-independent objectives in the context of stochastic games. We show a generic reduction from the expectation problem to linearly many instances of the almost-sure satisfaction problem for threshold Boolean objectives. The result follows from partitioning the vertices of the game into so-called value classes where each class consists of vertices of the same value. Our procedure further entails that the memory required by both players to play optimally for the expectation problem is no more than the memory required by the players to play optimally for the almost-sure satisfaction problem for a corresponding threshold Boolean objective. We show the applicability of the framework to compute the expected window mean-payoff measure in stochastic games. The window mean-payoff measure strengthens the classical mean-payoff measure by computing the mean payoff over windows of bounded length that slide along an infinite path. We show that the decision problem to check if the expected window mean-payoff value is at least a given threshold is in UP $\cap$ coUP when the window length is given in unary.