## Simple Stochastic Parity Games

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

Many verification, planning, and control problems can be modeled as
games played on state-transition graphs by one or two players whose
conflicting goals are to form a path in the graph which satisfies a
given objective. The focus here is on simple stochastic parity games,
that is, two-player games with turn-based probabilistic transitions
and omega-regular objectives formalized as parity (Rabin chain)
winning conditions. An efficient translation from simple stochastic
parity games to nonstochastic parity games is given. As many
algorithms are known for solving the latter, the translation yields
efficient algorithms for computing the states of a simple stochastic
parity game from which a player can win with probability 1.

An important special case of simple stochastic parity games are the
Markov decision processes with Buchi objectives. For this special
case a first provably subquadratic algorithm is given for computing
the states from which the single player has a strategy to achieve a
Buchi objective with probability 1. For game graphs with *m*
edges the algorithm works in time *O(m*^{1.5}).
Interestingly, a similar technique sheds light on the question of the
computational complexity of solving simple Buchi games and yields the
first provably subquadratic algorithm, with a running time of
*O(n*^{2}/log n) for game graphs with *n* vertices
and *O(n)* edges.

*Proceedings of the
International Conference for Computer Science Logic*
(CSL),
Lecture Notes in Computer Science 2803,
Springer, 2003, pp. 100-113.

Download inofficial, sometimes updated
PostScript /
PDF document.
© 2003 Springer.