## Quantitative Stochastic Parity Games

*Krishnendu Chatterjee, Marcin Jurdzinski, and
Thomas A. Henzinger*

We study perfect-information stochastic parity games. These are
two-player nonterminating games which are played on a graph with
turn-based probabilistic transitions. A play results in an infinite
path and the conflicting goals of the two players are omega-regular
path properties, formalized as parity winning conditions. The
*qualitative* solution of such a game amounts to computing the
set of vertices from which a player has a strategy to win with
probability 1 (or with positive probability). The *quantitative*
solution amounts to computing the value of the game in every vertex,
i.e., the highest probability with which a player can guarantee
satisfaction of his own objective in a play that starts from the
vertex.

For the important special case of one-player stochastic parity games
(parity Markov decision processes) we give polynomial-time algorithms
both for the qualitative and the quantitative solution. The running
time of the qualitative solution is *O(d · m*^{1.5})
for graphs with *m* edges and *d* priorities. The
quantitative solution is based on a linear-programming formulation.

For the two-player case, we establish the existence of optimal pure
memoryless strategies. This has several important ramifications.
First, it implies that the values of the games are rational. This is
in contrast to the *concurrent* stochastic parity games of de
Alfaro et al.; there, values are in general algebraic numbers, optimal
strategies do not exist, and epsilon-optimal strategies have to be
mixed and with infinite memory. Second, the existence of optimal pure
memoryless strategies together with the polynomial-time solution for
one-player case implies that the quantitative two-player stochastic
parity game problem is in NP ∩ coNP. This generalizes a result of
Condon for stochastic games with reachability objectives. It also
constitutes an exponential improvement over the best previous
algorithm, which is based on a doubly exponential procedure of de
Alfaro and Majumdar for concurrent stochastic parity games and
provides only epsilon-approximations of the values.

*Proceedings of the
15th Annual Symposium on Discrete Algorithms*
(SODA), ACM Press, 2004, pp. 114-123.

Download inofficial, sometimes updated
PostScript /
PDF document.
© 2004 ACM.