Strategy Synthesis for Stochastic Rabin Games with Discounted Reward
For researchers in formal methods and game theory, this work advances the understanding of strategy complexity in stochastic games with combined qualitative and quantitative objectives.
The paper tackles strategy synthesis in stochastic Rabin games with discounted reward, showing that optimal almost-sure winning strategies may require infinite memory, but epsilon-optimal strategies can be finite-memory or memoryless. It provides a necessary and sufficient condition for memoryless epsilon-optimal strategies and an algorithm to compute them.
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.