Timed Parity Games: Complexity and Robustness
From MaRDI portal
Abstract: 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.
Recommendations
- Timed Parity Games: Complexity and Robustness
- Timed games with bounded window parity objectives
- Time and parallelizability results for parity games with bounded treewidth
- Probabilistic robust timed games
- Time and Parallelizability Results for Parity Games with Bounded Tree and DAG Width
- Reachability-Time Games on Timed Automata
- Robustness of structurally equivalent concurrent parity games
- Timeability of extensive-form games
- Reachability games and parity games
- A recursive approach to solving parity games in quasipolynomial time
Cited in
(24)- Logical time control of concurrent DES
- Timed games with bounded window parity objectives
- Timed network games
- A turn-based approach for qualitative time concurrent games
- Synthesising succinct strategies in safety games with an application to real-time scheduling
- Shrinking timed automata
- Synthesis of memory-efficient ``real-time controllers for safety objectives
- Robust reachability in timed automata: a game-based approach
- Probabilistic robust timed games
- Timed Control with Observation Based and Stuttering Invariant Strategies
- Efficient On-the-Fly Algorithms for Partially Observable Timed Games
- Trading Infinite Memory for Uniform Randomness in Timed Games
- Combining symbolic representations for solving timed games
- Synthesis of memory-efficient, clock-memory free, and non-Zeno safety controllers for timed systems
- Robust reachability in timed automata and games: a game-based approach
- Time and Parallelizability Results for Parity Games with Bounded Tree and DAG Width
- Timed network games with clocks
- Differential game logic
- CONCUR 2005 – Concurrency Theory
- Timed Parity Games: Complexity and Robustness
- The element of surprise in timed games.
- Parity games on temporal graphs
- The Church synthesis problem over continuous time
- Temporal explorability games
This page was built for publication: Timed Parity Games: Complexity and Robustness
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5895527)
