Thomas A. Henzinger and Krishnendu Chatterjee
Stochastic games provide a uniform framework to model interaction between agents and components. These games are dynamic games, played over a state space and possibly for infinite rounds. Problems that arise in verification, planning, and control can be modeled as stochastic games played on state-transition graphs by one or two players whose conflicting goals are to form a path in the graph.
The class of ω-regular languages generalize classical regular languages to infinite strings and forms a robust specification language for verification. Classical notion of winning conditions that capture all ω-regular conditions are Rabin and Streett conditions, parity and Muller conditions.
We study perfection-information deterministic games with disjunction and conjunction of parity objectives and present efficient algorithms to solve such games in .
We study the strategy synthesis and complexity of perfect-information stochastic games with Muller conditions in .
We also introduce a logical framework that allow analysis of both zero-sum and non-zero-sum games in a concise and clean way in .
- K. Chatterjee, T. A. Henzinger, and N. Piterman, "Generalized Parity Games," FoSSaCS, Springer, LNCS, 2007.
- K. Chatterjee, "Optimal Strategy Synthesis in Stochastic Muller Games," FoSSaCS, Springer, LNCS, 2007.
- K. Chatterjee, T. A. Henzinger, and N. Piterman, "Strategy Logic," CONCUR, Springer, LNCS, 2007.