Research Projects

Stochastic Games

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 [1].

We study the strategy synthesis and complexity of perfect-information stochastic games with Muller conditions in [2].

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 [3].

[1]

K. Chatterjee, T. A. Henzinger, and N. Piterman, "Generalized Parity Games," FoSSaCS, Springer, LNCS, 2007.

[2]

K. Chatterjee, "Optimal Strategy Synthesis in Stochastic Muller Games," FoSSaCS, Springer, LNCS, 2007.

[3]

K. Chatterjee, T. A. Henzinger, and N. Piterman, "Strategy Logic," CONCUR, Springer, LNCS, 2007.