Krishnendu Chatterjee, Luca de Alfaro, Thomas A. Henzinger
04/04/2008 09:00 AM
Computer Engineering
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.
