Quantitative Solution of Omega-Regular Games
CALIFORNIA UNIV BERKELEY DEPT OF ELECTRICAL ENGINEERING AND COMPUTER SCIENCE
Pagination or Media Count:
We consider two-player games played for an infinite number of rounds with omega-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 mu-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 omega-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 Buchi conditions require the use of strategies with infinite memory. The existence of optimal strategies as opposed to epsilon-optimal, is only guaranteed in games with safety winning conditions.
- Statistics and Probability