Strategy Synthesis for Stochastic Rabin Games with Discounted Reward

TL;DR

This paper addresses the synthesis of optimal strategies in stochastic games with Rabin conditions and discounted rewards, showing conditions for finite-memory solutions and providing an algorithm for their computation.

Contribution

It introduces a method to synthesize epsilon-optimal strategies with finite or memoryless memory in stochastic Rabin games with discounted rewards.

Findings

Optimal strategies may require infinite memory.

Epsilon-optimal strategies can be finite-memory or memoryless.

An algorithm for computing memoryless epsilon-optimal strategies is proposed.

Abstract

Stochastic games are often used to model reactive processes. We consider the problem of synthesizing an optimal almost-sure winning strategy in a two-player (namely a system and its environment) turn-based stochastic game with both a qualitative objective as a Rabin winning condition, and a quantitative objective as a discounted reward. Optimality is considered only over the almost-sure winning strategies, i.e., system strategies that guarantee the satisfaction of the Rabin condition with probability 1 regardless of the environment's strategy. We show that optimal almost-sure winning strategies may need infinite memory, but epsilon-optimal almost-sure winning strategies can always be finite-memory or even memoryless. We identify a sufficient and necessary condition of the existence of memoryless epsilon-optimal almost-sure winning strategies and propose an algorithm to compute one when this condition is satisfied.