Quantitative solution of omega-regular games

We consider two-player games played for an infinite number of rounds, with -regular winning conditions. The games may be concurrent, in that the players choose their moves simultaneously and independently, and probabilistic, in that the moves determine a probability distribution for the successor state. We introduce quantitative game ?-calculus, and we show that the maximal probability of winning such games can be expressed as the fixpoint formulas in this calculus. We develop the arguments both for deterministic and for probabilistic concurrent games; as a special case, we solve probabilistic turn-based games with -regular winning conditions, which was also open. We also characterize the optimality, and the memory requirements, of the winning strategies. In particular, we show that while memoryless strategies suffice for winning games with safety and reachability conditions, B?uchi conditions require the use of strategies with infinite memory. The existence of optimal strategies, as ...

• Type: Conference
• Year: 2001
• Where: STOC
• Authors: Luca de Alfaro, Rupak Majumdar
• Keywords: -regular Winning Conditions, Algorithms, Probabilistic Concurrent Games, Safety Winning Conditions, STOC 2001