Krishnendu Chatterjee ; Thomas A. Henzinger ; Vinayak S. Prabhu - Timed Parity Games: Complexity and Robustness

lmcs:1102 - Logical Methods in Computer Science, December 14, 2011, Volume 7, Issue 4 -
Timed Parity Games: Complexity and Robustness

Authors: Krishnendu Chatterjee ; Thomas A. Henzinger ; Vinayak S. Prabhu

We consider two-player games played in real time on game structures with clocks where the objectives of players are described using parity conditions. The games are \emph{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 play strategies that ensure that the player cannot be responsible for causing a zeno run. First, we present an efficient reduction of these games to \emph{turn-based} (i.e., not concurrent) \emph{finite-state} (i.e., untimed) parity games. 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. The states of the resulting game are based on clock regions of the original game, and the state space of the finite game is linear in the size of the region graph. Second, we consider two restricted classes of strategies for the player that represents the controller in a real-time synthesis problem, namely, \emph{limit-robust} and \emph{bounded-robust} winning strategies. Using a limit-robust winning 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 winning. We show that exact strategies are more powerful than limit-robust strategies, which are more powerful than bounded-robust winning 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.

Volume: Volume 7, Issue 4
Published on: December 14, 2011
Accepted on: June 25, 2015
Submitted on: February 12, 2010
Keywords: Computer Science - Logic in Computer Science,F.4.1


Consultation statistics

This page has been seen 317 times.
This article's PDF has been downloaded 253 times.