A Survey of Stochastic Omega-regular Games

Krishnendu Chatterjee and Thomas A. Henzinger

We summarize classical and recent results about two-player games played on graphs with omega-regular objectives. These games have applications in the verification and synthesis of reactive systems. Important distinctions are whether a graph game is turn-based or concurrent; deterministic or stochastic; zero-sum or not. We cluster known results and open problems according to these classifications.

Journal of Computer and System Sciences, to appear.

Download inofficial, sometimes updated PostScript / PDF document. © 2009 Elsevier.