Timed parity games: complexity and robustness Conference Paper


Author(s): Chatterjee, Krishnendu; Henzinger, Thomas A; Prabhu, Vinayak S
Title: Timed parity games: complexity and robustness
Title Series: LNCS
Affiliation
Abstract: 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, limit-robust and bounded-robust strategies. Using a limit-robust strategy, the controller cannot choose an exact real-valued time delay but must allow for some nonzero jitter in each of its actions. If there is a given lower bound on the jitter, then the strategy is bounded-robust. We show that exact strategies are more powerful than limit-robust strategies, which are more powerful than bounded-robust strategies for any bound. For both kinds of robust strategies, we present efficient reductions to standard timed automaton games. These reductions provide algorithms for the synthesis of robust real-time controllers.
Conference Title: FORMATS: Formal Modeling and Analysis of Timed Systems
Volume: 5215
Conference Dates: September 15-17, 2008
Conference Location: Saint Malo, France
Publisher: Springer  
Location: Berlin, Heidelberg
Date Published: 2008-10-01
Start Page: 124
End Page: 140
Sponsor: This research was supported in part by the NSF grants CCR-0132780, CNS-0720884, and CCR-0225610, and by the European COMBEST project.
DOI: 10.1007/978-3-540-85778-5_10
Open access: no
IST Austria Authors
  1. Thomas A. Henzinger
    415 Henzinger
Related IST Austria Work