Quantitative Solution of Omega-Regular Games
Abstract
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.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jul 01, 2001
- Accession Number
- ADA461490
Entities
People
- Luca De Alfaro
- Rupak Majumdar
Organizations
- University of California, Berkeley