EECS technical reports

Conditions of Use

Archive Home Page

The Complexity of Stochastic Rabin and Streett Games

Chatterjee, Krishnendu
de Alfaro, Luca
Henzinger, Thomas A.
Technical Report Identifier: CSD-04-1355
November 2004

Abstract: The foundation of modeling and synthesizing reactive processes is the theory of graph games with omega-regular winning conditions. In the case of stochastic reactive processes, the corresponding stochastic graph games have three players, two of them (System and Environment) behaving adversarially, and the third (Uncertainty) behaving probabilistically. We consider two solution problems for stochastic graph games: a qualitative problem, calling for the computation of the set of states from which a player can win with probability 1 (almost-sure winning), and a quantitative problem, calling for the computation of the maximal probability of winning (optimal winning) from each state. We show that, for Rabin winning conditions, both problems are in NP. As these problems were known to be NP-hard, it follows that they are NP-complete for Rabin conditions, and dually, coNP-complete for Streett conditions. The proof proceeds by showing that pure memoryless strategies suffice for qualitatively and quantitatively winning stochastic graph games with Rabin conditions. This fact was an open problem, and it is of interest in its own right, as it implies that controllers for Rabin objectives have simple implementations. We also prove that for any omega-regular objective optimal winning strategies are no more complex than almost-sure winning strategies.