Solving simple stochastic tail games

Abstract

Infinite stochastic games are a natural model for open reactive processes: one player represents the controller and the other represents a hostile environment. The evolution of the system depends on the decisions of the players, supplemented by chance. There are two main algorithmic problems on such games: computing the values of the vertices (quantitative analysis) and deciding whether a player can win with probability one, or arbitrarily close to one (qualitative analysis). In this paper, we reduce the quantitative analysis of simple stochastic tail games (where both players have perfect information and the winner does not depend on finite prefixes) to the qualitative analysis: we provide an algorithm computing values which uses qualitative analysis as a sub-procedure. The correctness proof of this algorithm reveals several nice properties of perfect-information stochastic tail games, in particular the existence of optimal strategies. We apply these results to games whose winning conditions are boolean combinations of mean-payoff and Büchi conditions. Copyright © by SIAM.