Timed Parity Games: Complexity and Robustness

13 years 9 months ago
Timed Parity Games: Complexity and Robustness
We consider two-player games played in real time on game structures with clocks and parity objectives. The games are concurrent in that at each turn, both players independently propose a time delay and an action, and the action with the shorter delay is chosen. To prevent a player from winning by blocking time, we restrict each player to strategies that ensure that the player cannot be responsible for causing a zeno run. First, we present an efficient reduction of these games to turn-based (i.e., nonconcurrent) finite-state (i.e., untimed) parity games. The states of the resulting game are pairs of clock regions of the original game. Our reduction improves the best known complexity for solving timed parity games. Moreover, the rich class of algorithms for classical parity games can now be applied to timed parity games. Second, we consider two restricted classes of strategies for the player that represents the controller in a real-time synthesis problem, namely, limitrobust and bounded-...
Krishnendu Chatterjee, Thomas A. Henzinger, Vinaya
Added 26 Oct 2010
Updated 26 Oct 2010
Type Conference
Year 2008
Authors Krishnendu Chatterjee, Thomas A. Henzinger, Vinayak S. Prabhu
Comments (0)