The Complexity of Quantitative Concurrent Parity Games
Abstract: We consider two-player infinite games played on graphs. The games are concurrent, in that at each state the players choose their moves simultaneously and independently, and stochastic, in that the moves determine a probability distribution for the successor state. The value of a game is the maximal probability with which a player can guarantee the satisfaction of her objective. We show that the values of concurrent games with omega-regular objectives expressed as parity conditions can be computed in NP cap coNP. This result substantially improves the best known previous bound of 3EXPTIME. It also shows that the full class of concurrent parity games is no harder than the special cases of turn-based deterministic parity games (Emerson-Jutla) and of turn-based stochastic reachability games (Condon), for both of which NP cap coNP is the best known bound.
While the previous, more restricted NP cap coNP results for graph games relied on the existence of particularly simple (pure memoryless) optimal strategies, in concurrent games with parity objectives optimal strategies may not exist, and epsilon-optimal strategies (which achieve the value of the game within a parameter epsilon > 0) require in general both randomization and infinite memory. Hence our proof must rely on a more detailed analysis of strategies and, in addition to the main result, yields two results that are interesting on their own. First, we show that there exist epsilon-optimal strategies that in the limit coincide with memoryless strategies; this parallels the celebrated result of Mertens-Neyman for concurrent games with limit-average objectives. Second, we complete the characterization of the memory requirements for epsilon-optimal strategies for concurrent omega-regular games, by showing that memoryless strategies suffice for epsilon-optimality for coBuchi conditions.