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

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 [Krishnendu Chatterjee et al., 2015]. It has since proved useful in a variety of settings, including parity objectives in games [Véronique Bruyère et al., 2016] and both mean-payoff and parity objectives in Markov decision processes [Thomas Brihaye et al., 2020]. 
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.