Timed Games with Bounded Window Parity Objectives

TL;DR

This paper studies bounded timed window parity objectives in timed automata and games, showing that verification is polynomial space and solving these games is exponential time, aligning with fixed objectives' complexity.

Contribution

It introduces the bounded timed window parity objective, analyzes its complexity, and compares it with fixed variants, extending the understanding of timed automata objectives.

Findings

Verification in polynomial space

Game solving in exponential time

Comparable complexity to fixed objectives

Abstract

The window mechanism, introduced by Chatterjee et al. for mean-payoff and total-payoff objectives in two-player turn-based games on graphs, refines long-term objectives with time bounds. This mechanism has proven useful in a variety of settings, and most recently in timed systems. In the timed setting, the so-called fixed timed window parity objectives have been studied. A fixed timed window parity objective is defined with respect to some time bound and requires that, at all times, we witness a time frame, i.e., a window, of size less than the fixed bound in which the smallest priority is even. In this work, we focus on the bounded timed window parity objective. Such an objective is satisfied if there exists some bound for which the fixed objective is satisfied. The satisfaction of bounded objectives is robust to modeling choices such as constants appearing in constraints, unlike fixed objectives, for which the choice of constants may affect the satisfaction for a given bound. We show that verification of bounded timed window objectives in timed automata can be performed in polynomial space, and that timed games with these objectives can be solved in exponential time, even for multi-objective extensions. This matches the complexity classes of the fixed case. We also provide a comparison of the different variants of window parity objectives.