Time Flies When Looking out of the Window: Timed Games with Window Parity Objectives

TL;DR

This paper introduces and analyzes window parity objectives in timed automata and timed games, demonstrating their computational complexity and extending the window mechanism to real-time systems.

Contribution

It is the first to study window parity objectives in timed automata and games, providing complexity results and reasoning about time bounds.

Findings

Checking all time-divergent paths is polynomial space

Timed games with window parity objectives are solvable in exponential time

Multi-dimensional objectives do not increase complexity

Abstract

The window mechanism was introduced by Chatterjee et al. to reinforce mean-payoff and total-payoff objectives with time bounds in two-player turn-based games on graphs. It has since proved useful in a variety of settings, including parity objectives in games and both mean-payoff and parity objectives in Markov decision processes. We study window parity objectives in timed automata and timed games: given a bound on the window size, a path satisfies such an objective if, in all states along the path, we see a sufficiently small window in which the smallest priority is even. We show that checking that all time-divergent paths of a timed automaton satisfy such a window parity objective can be done in polynomial space, and that the corresponding timed games can be solved in exponential time. This matches the complexity class of timed parity games, while adding the ability to reason about time bounds. We also consider multi-dimensional objectives and show that the complexity class does not increase. To the best of our knowledge, this is the first study of the window mechanism in a real-time setting.