K. Chatterjee,
L. de Alfaro,
T.A. Henzinger.
Qualitative Concurrent Parity Games.
Technical Report UCSC-CRL-08-02, School of Engineering,
University of California, Santa Cruz, CA, USA. April 2008.
Abstract
PDF
Abstract
We consider 2-player games played on a finite state space for an
infinite number of rounds.
The games are
concurrent: in each round, the two players
choose their moves independently and simultaneously;
the current state and the two moves determine the successor state.
We consider omega-regular winning conditions specified as
parity objectives on the resulting infinite state sequence.
Both players are allowed to use randomization when choosing their
moves.
We study the computation of the
limit-winning set of states,
consisting of the states where the sup-inf value of the game for
player 1 is 1: in other words, a state is
limit-winning if
player 1 can ensure a probability of winning
arbitrarily close to 1.
We show that the limit-winning set can be computed in
O(n^{2m+2}) time,
where n is the size of the game structure and 2m is the number of
parities; membership of a state in the limit-winning set can be
decided in NP intersection coNP.
While this complexity is the same as for the simpler class of
turn-based parity games, where in each state only one of the
two players has a choice of moves, our algorithms are considerably
more
involved than those for turn-based games.
This is because concurrent games violate two of the most fundamental
properties of turn-based parity games.
First, in concurrent games limit-winning strategies require
randomization;
and second, they require infinite memory.