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

Timed automata [2] are extensions of finite automata with real-valued variables called clocks. Clocks increase at the same rate and measure the elapse of time between actions. Transitions are constrained by the values of clocks, and clocks can be reset on transitions. Timed automata are used to model real-time systems [4]. Not all paths of timed automata are meaningful; infinite paths that take a finite amount of time, called time-convergent paths, are often disregarded when checking properties of timed automata. Timed automata induce uncountable transition systems. However, many properties can be checked using the region abstraction, which is a finite quotient of the transition system.

Timed automaton games [25], or simply timed games, are games played on timed automata: one player represents the system and the other its environment. Players play an infinite amount of rounds: for each round, both players simultaneously present a delay and an action, and the play proceeds according to the fastest move (note that we use paths for automata and plays for games to refer to sequences of consecutive states and transitions). When defining winning conditions for players, convergent plays must be taken in account; we must not allow a player to achieve its objective by forcing convergence but cannot either require a player to force divergence (as it also depends on its opponent). Given an objective as a set of plays, following [20], we declare a play winning for a player if either it is time-divergent and belongs to the objective, or it is time-convergent and the player is not responsible for convergence.

The class of $\omega$-regular specifications is widely used (e.g., it can express liveness and safety), and parity conditions are a canonical way of representing them. In (timed) parity games, locations are labeled with a non-negative integer priority and the parity objective is to ensure the smallest priority occurring infinitely often along the path/play is even. Timed games with $\omega$-regular objectives given as parity automata are shown to be solvable in [20]. Furthermore, a reduction from timed parity games to classical turn-based parity games on a graph is established in [19].

The parity objective can be reformulated: for all odd priorities seen infinitely often, a smaller even priority must be seen infinitely often. One can see the odd priority as a request and the even one as a response. The parity objective does not specify any timing constraints between requests and responses. In applications however, this may not be sufficient: for example, a server should respond to requests in a timely manner.

We revisit the window mechanism introduced by Chatterjee et al. for mean-payoff and total-payoff games [17] and later applied to parity games [14] and to parity and mean-payoff objectives in Markov decision processes [12]: we provide the first (to the best of our knowledge) study of window objectives in the real-time setting. More precisely, we lift the (resp. direct) fixed window parity objective of [14] to its real-time counterpart, the (resp. direct) timed window parity objective, and study it in timed automata and games.

Intuitively, given a non-negative integer bound $\lambda$ on the window size, the direct timed window parity objective requires that at all times along a path/play, we see a window of size at most $\lambda$ such that the smallest priority in this window is even. While time was counted as steps in prior works (all in a discrete setting), we naturally measure window size using delays between configurations in real-time models. The (non-direct) timed window parity objective is simply a prefix-independent version of the direct one, thus more closely matching the spirit of classical parity: it asks that some suffix satisfies the direct objective.

We extend window parity objectives to a dense-time setting, and study both verification of timed automata and realizability in timed games. We consider adaptations of the fixed window parity objectives of [14], where the window size is given as a parameter. We establish that (a) verifying that all time-divergent paths of a timed automaton satisfy a timed window parity specification is PSPACE-complete; and that (b) checking the existence of a winning strategy for a window parity objective in timed games is EXPTIME-complete. These results (Theorem 6.8) hold for both the direct and prefix-independent variants, and they extend to multi-dimensional objectives, i.e., conjunctions of window parity.

All algorithms are based on a reduction to an expanded timed automaton (Definition 4.1). We establish that, similarly to the discrete case, it suffices to keep track of one window at a time (or one per objective in the multi-dimensional case) instead of all currently open windows, thanks to the so-called inductive property of windows (Lemma 3.3). A window can be summarized using its smallest priority and its current size: we encode the priorities in a window by extending locations with priorities and using an additional clock to measure the window’s size. The (resp. direct) timed window parity objective translates to a co-Büchi (resp. safety) objective on the expanded automaton. Locations to avoid for the co-Büchi (resp. safety) objective indicate a window exceeding the supplied bound without the smallest priority of the window being even — a bad window. To check that all time-divergent paths of the expanded automaton satisfy the safety (resp. co-Büchi) objective, we check for the existence of a time-divergent path visiting (resp. infinitely often) an unsafe location using the PSPACE algorithm of [2]. To solve the similarly-constructed expanded game, we use the EXPTIME algorithm of [20].

Lower bounds (Lemma 6.6) are established by encoding safety objectives on timed automata as (resp. direct) timed window parity objectives. Checking safety properties over time-divergent paths in timed automata is PSPACE-complete [2] and solving safety timed games is EXPTIME-complete [22].

Window variants constitute conservative approximations of classical objectives (e.g., [17, 14, 12]), strengthening them by enforcing timing constraints. Complexity-wise, the situation is varied. In one-dimension turn-based games on graphs, window variants [17, 14] provide polynomial-time alternatives to the classical objectives, bypassing long-standing complexity barriers. However, in multi-dimension games, their complexity becomes worse than for the original objectives: in particular, fixed window parity games are EXPTIME-complete for multiple dimensions [14]. We show that timed games with multi-dimensional window parity objectives are in the same complexity class as untimed ones, i.e., dense time comes for free.

For classical parity objectives, timed games can be solved in exponential time [19, 20]. The approach of [19] is as follows: from a timed parity game, one builds a corresponding turn-based parity game on a graph, the construction being polynomial in the number of priorities and the size of the region abstraction. We recall that despite recent progress on quasi-polynomial-time algorithms (starting with [16]), no polynomial-time algorithm is known for parity games; the blow-up comes from the number of priorities. Overall, the two sources of blow-up — region abstraction and number of priorities — combine in a single-exponential solution for timed parity games. We establish that (multi-dimensional) window parity games can be solved in time polynomial in the size of the region abstraction, the number of priorities and the window size, and exponential in the number of dimensions. Thus even for conjunctions of objectives, we match the complexity class of single parity objectives of timed games, while avoiding the blow-up related to the number of priorities and enforcing time bounds between odd priorities and smaller even priorities via the window mechanism.

This work is organized as follows. Section 2 summarizes all prerequisite notions and vocabulary. In Section 3, we introduce the timed window parity objective, compare it to the classical parity objective, and establish some useful properties. Our reduction from window parity objectives to safety or co-Büchi objectives is presented in Section 4: the construction of the expanded timed automaton/game used in the reduction is provided in Section 4.1, Section 4.2 develops mappings between plays of a game and plays of its expansion such that a time-divergent play in one game satisfies the objective if and only if its image satisfies the objective of the other game and Section 4.3 shows how these mappings can be used to transfer winning strategies between a timed game and its expansion. The reduction is extended to the case of multiple window parity objectives in Section 5. Finally, Section 6 presents the complexity.

This paper is a full version of a preceding conference version [24]. This version presents in full details the contributions of the conference version, with detailed proofs.

In addition to the aforementioned foundational works, the window mechanism has seen diverse extensions and applications: e.g., [5, 3, 11, 15, 23, 27, 8]. Window parity games are strongly linked to the concept of finitary $\omega$-regular games: see, e.g., [18], or [14] for a complete list of references. The window mechanism can be used to ensure a certain form of (local) guarantee over paths: different techniques have been considered in stochastic models, notably variance-based [10] or worst-case-based [13, 7] methods. Finally, let us recall that game models provide a useful framework for controller synthesis [26], and that timed automata have been extended in a number of directions (see, e.g., [9] and references therein): applications of the window mechanism in such richer models could be of interest.

A clock variable, or clock, is a real-valued variable. Let $C$ be a set of clocks. A clock constraint over $C$ is a conjunction of formulae of the form $x\sim c$ with $x\in C$, $c\in\mathbb{N}$, and $\sim\in\{\leq,\geq,>,<\}$. We write $x=c$ as shorthand for the clock constraint $x\geq c\land x\leq c$. Let $\Phi(C)$ denote the set of clock constraints over $C$.

Let $\mathbb{R}_{\geq 0}$ denote the set of non-negative real numbers. We refer to functions $\nu\in\mathbb{R}_{\geq 0}^{C}$ as clock valuations over $C$. A clock valuation $\nu$ over a set $C$ of clocks satisfies a clock constraint of the form $x\sim c$ if $\nu(x)\sim c$ and a conjunction $g\land h$ if it satisfies both $g$ and $h$. Given a clock constraint $g$ and clock valuation $\nu$, we write $\nu\models g$ if $\nu$ satisfies $g$.

For a clock valuation $\nu$ and $d\geq 0$, we let $\nu+d$ be the valuation defined by $(\nu+d)(x)=\nu(x)+d$ for all $x\in C$. For any valuation $\nu$ and $D\subseteq C$, we define $\mathsf{reset}_{D}(\nu)$ to be the valuation agreeing with $\nu$ for clocks in $C\setminus D$ and that assigns $0$ to clocks in $D$. We denote by $\mathbf{0}^{C}$ the zero valuation, assigning 0 to all clocks in $C$.

A timed automaton (TA) is a tuple $(L,\ell_{\mathsf{init}},C,\Sigma,I,E)$ where $L$ is a finite set of locations, $\ell_{\mathsf{init}}\in L$ is an initial location, $C$ a finite set of clocks containing a special clock $\gamma$ which keeps track of the total time elapsed, $\Sigma$ a finite set of actions, $I\colon L\to\Phi(C)$ an invariant assignment function and $E\subseteq L\times\Phi(C)\times\Sigma\times 2^{C\setminus\{\gamma\}}\times L$ an edge relation. We only consider deterministic timed automata, i.e., we assume that in any location $\ell$, there are no two outgoing edges $(\ell,g_{1},a,D_{1},\ell_{1})$ and $(\ell,g_{2},a,D_{2},\ell_{2})$ sharing the same action such that the conjunction $g_{1}\land g_{2}$ is satisfiable. For an edge $(\ell,g,a,D,\ell^{\prime})$, the clock constraint $g$ is called the guard of the edge.

A TA $\mathcal{A}=(L,\ell_{\mathsf{init}},C,\Sigma,I,E)$ gives rise to an uncountable transition system $\mathcal{T}(\mathcal{A})=(S,s_{\mathsf{init}},M,\to)$ with the state space $S=L\times\mathbb{R}_{\geq 0}^{C}$, the initial state $s_{\mathsf{init}}=(\ell_{\mathsf{init}},\mathbf{0}^{C})$, set of actions $M=\mathbb{R}_{\geq 0}\times(\Sigma\cup\{\bot\})$ and the transition relation $\to\subseteq S\times M\times S$ defined as follows: for any action $a\in\Sigma$ and delay $d\geq 0$, we have that $((\ell,\nu),(d,a),(\ell^{\prime},\nu^{\prime}))\in\to$ if and only if there is some edge $(\ell,g,a,D,\ell^{\prime})\in E$ such that $\nu+d\models g$, $\nu^{\prime}=\mathsf{reset}_{D}(\nu+d)$, $\nu+d\models I(\ell)$ and $\nu^{\prime}\models I(\ell^{\prime})$; for any delay $d\geq 0$, $((\ell,\nu)(d,\bot),(\ell,\nu+d))\in\to$ if and only if $\nu+d\models I(\ell)$. Let us note that the satisfaction set of clock constraints is convex: it is described by a conjunction of inequalities. Whenever $\nu\models I(\ell)$, the above conditions $\nu+d\models I(\ell)$ (the invariant holds after the delay) are equivalent to requiring $\nu+d^{\prime}\models I(\ell)$ for all $0\leq d^{\prime}\leq d$ (the invariant holds at each intermediate time step).

A move is any pair in $\mathbb{R}_{\geq 0}\times(\Sigma\cup\{\bot\})$ (i.e., an action in the transition system). For any move $m=(d,a)$ and states $s$, $s^{\prime}\in S$, we write $s\xrightarrow{m}s^{\prime}$ or $s\xrightarrow{d,a}s^{\prime}$ as shorthand for $(s,m,s^{\prime})\in\to$. Moves of the form $(d,\bot)$ are called delay moves. We say a move $m$ is enabled in a state $s$ if there is some $s^{\prime}$ such that $s\xrightarrow{m}s^{\prime}$. There is at most one successor per move in a state, as we do not allow two guards on edges labeled by the same action to be simultaneously satisfied.

A path in a TA $\mathcal{A}$ is a finite or infinite sequence $s_{0}(d_{0},a_{0})s_{1}\ldots\in S(MS)^{*}\cup(SM)^{\omega}$ such that for all $j$, $s_{j}$ is a state of $\mathcal{T}(\mathcal{A})$ and for all $j>0$, $s_{j-1}\xrightarrow{d_{j-1},a_{j-1}}s_{j}$ is a transition in $\mathcal{T}(\mathcal{A})$. A path is initial if $s_{0}=s_{\mathsf{init}}$. For clarity, we write $s_{0}\xrightarrow{d_{0},a_{0}}s_{1}\xrightarrow{d_{1},a_{1}}\cdots$ instead of $s_{0}(d_{0},a_{0})s_{1}(d_{1},a_{1})\ldots$.

An infinite path $\pi=(\ell_{0},\nu_{0})\xrightarrow{d_{0},a_{0}}(\ell_{1},\nu_{1})\ldots$ is time-divergent if the sequence $(\nu_{j}(\gamma))_{j\in\mathbb{N}}$ is not bounded from above. A path which is not time-divergent is called time-convergent; time-convergent paths are traditionally ignored in analysis of timed automata [1, 2] as they model unrealistic behavior. This includes ignoring Zeno paths, which are time-convergent paths along which infinitely many actions appear. We write $\mathsf{Paths}(\mathcal{A})$ for the set of paths of $\mathcal{A}$.

A priority function is a function $p\colon L\to\{0,\ldots,d-1\}$ with $d\leq|L|$. We use priority functions to express parity objectives. A $k$-dimensional priority function is a function $p\colon L\to\{0,\ldots,d-1\}^{k}$ which assigns vectors of priorities to locations.

We consider two player games played on TAs. We refer to the players as player 1 ($\mathcal{P}_{1}$) for the system and player 2 ($\mathcal{P}_{2}$) for the environment. We use the notion of timed automaton games of [20].

A timed (automaton) game (TG) is a tuple $\mathcal{G}=(\mathcal{A},\Sigma_{1},\Sigma_{2})$ where $\mathcal{A}=(L,\ell_{\mathsf{init}},C,\Sigma,I,E)$ is a TA and $(\Sigma_{1},\Sigma_{2})$ is a partition of $\Sigma$. We refer to actions in $\Sigma_{i}$ as $\mathcal{P}_{i}$ actions for $i\in\{1,2\}$.

Recall a move is a pair $(d,a)\in\mathbb{R}_{\geq 0}\times(\Sigma\cup\{\bot\})$. Let $S$ denote the set of states of $\mathcal{T}(\mathcal{A})$. In each state $s=(\ell,\nu)\in S$, the moves available to $\mathcal{P}_{1}$ are the elements of the set $M_{1}(s)$ where

contains moves with $\mathcal{P}_{1}$ actions and delay moves that are enabled in $s$. The set $M_{2}(s)$ is defined analogously with $\mathcal{P}_{2}$ actions. We write $M_{1}$ and $M_{2}$ for the set of all moves of $\mathcal{P}_{1}$ and $\mathcal{P}_{2}$ respectively.

At each state $s$ along a play, both players simultaneously select a move $(d^{(1)},a^{(1)})\in M_{1}(s)$ and $(d^{(2)},a^{(2)})\in M_{2}(s)$. Intuitively, the fastest player gets to act and in case of a tie, the move is chosen non-deterministically. This is formalized by the joint destination function $\delta:S\times M_{1}\times M_{2}\to 2^{S}$, defined by

For $m^{(1)}=(d^{(1)},a^{(1)})\in M_{1}$ and $m^{(2)}=(d^{(2)},a^{(2)})\in M_{2}$, we write $\mathsf{delay}(m^{(1)},m^{(2)})=\min\{d^{(1)},d^{(2)}\}$ to denote the delay occurring when $\mathcal{P}_{1}$ and $\mathcal{P}_{2}$ play $m^{(1)}$ and $m^{(2)}$ respectively.

A play is defined similarly to a path: it is a finite or infinite sequence of the form $s_{0}(m_{0}^{(1)},m_{0}^{(2)})s_{1}(m_{1}^{(1)},m_{1}^{(2)})\ldots\in S((M_{1}\times M_{2})S)^{*}\cup(S(M_{1}\times M_{2}))^{\omega}$ where for all indices $j$, $m_{j}^{(i)}\in M_{i}(s_{j})$ for $i\in\{1,2\}$, and for $j>0$, $s_{j}\in\delta(s_{j-1},m_{j-1}^{(1)},m_{j-1}^{(2)})$. A play is initial if $s_{0}=s_{\mathsf{init}}$. For a finite play $\pi=s_{0}\ldots s_{n}$, we set $\mathsf{last}(\pi)=s_{n}$. For an infinite play $\pi=s_{0}\ldots$, we write $\pi_{|n}=s_{0}(m_{0}^{(0)},m_{0}^{(1)})\ldots s_{n}$. A play follows a path in the TA, but there need not be a unique path compatible with a play: if along a play, at the $n$th step, the moves of both players share the same delay and target state, either move can label the $n$th transition in a matching path.

Similarly to paths, an infinite play $\pi=(\ell_{0},\nu_{0})(m_{0}^{(1)},m_{0}^{(2)})\cdots$ is time-divergent if and only if $(\nu_{j}(\gamma))_{j\in\mathbb{N}}$ is not bounded from above. Otherwise, we say a play is time-convergent. We define the following sets: $\mathsf{Plays}(\mathcal{G})$ for the set of plays of $\mathcal{G}$; $\mathsf{Plays}_{\mathit{fin}}(\mathcal{G})$ for the set of finite plays of $\mathcal{G}$; $\mathsf{Plays}_{\infty}(\mathcal{G})$ for the set of time-divergent plays of $\mathcal{G}$. We also write $\mathsf{Plays}(\mathcal{G},s)$ to denote plays starting in state $s$ of $\mathcal{T}(\mathcal{A})$.

Note that our games are built on deterministic TAs. From a modeling standpoint, this is not restrictive, as we can simulate a non-deterministic TA through the actions of $\mathcal{P}_{2}$.

A strategy for $\mathcal{P}_{i}$ is a function describing which move a player should use based on a play history. Formally, a strategy for $\mathcal{P}_{i}$ is a function $\sigma_{i}\colon\mathsf{Plays}_{\mathit{fin}}(\mathcal{G})\to M_{i}$ such that for all $\pi\in\mathsf{Plays}_{\mathit{fin}}(\mathcal{G})$, $\sigma_{i}(\pi)\in M_{i}(\mathsf{last}(\pi))$. This last condition requires that each move given by a strategy be enabled in the last state of a play.

A play $s_{0}(m_{0}^{(1)},m_{0}^{(2)})s_{1}\ldots$ is said to be consistent with a $\mathcal{P}_{i}$-strategy $\sigma_{i}$ if for all indices $j$, $m_{j}^{(i)}=\sigma_{i}(\pi_{|j})$. Given a $\mathcal{P}_{i}$-strategy $\sigma_{i}$, we define $\mathsf{Outcome}_{i}(\sigma_{i})$ (resp. $\mathsf{Outcome}_{i}(\sigma_{i},s)$) to be the set of plays (resp. set of plays starting in state $s$) consistent with $\sigma_{i}$.

A $\mathcal{P}_{i}$-strategy $\sigma_{i}$ is move-independent if the move it suggests depends only on the sequence of states seen in the play. Formally, $\sigma_{i}$ is move-independent if for all finite plays $\pi=s_{0}(m_{0}^{(1)},m_{0}^{(2)})s_{1}\ldots s_{k}$ and $\tilde{\pi}=\tilde{s}_{0}(\tilde{m}_{0}^{(1)},\tilde{m}_{0}^{(2)})\tilde{s}_{1}\ldots\tilde{s}_{k}$ if $s_{n}=\tilde{s}_{n}$ for all $n\in\{0,\ldots,k\}$, then $\sigma_{i}(\pi)=\sigma_{i}(\tilde{\pi})$. We use move-independent strategies in the proof of our reduction to relabel some moves of a play without affecting the suggestions of the strategy.

An objective represents the property we desire on paths of a TA or a goal of a player in a TG. Formally, we define an objective as a set $\Psi\subseteq\mathsf{Paths}(\mathcal{A})$ of infinite paths (when studying TAs) or a set $\Psi\subseteq\mathsf{Plays}(\mathcal{G})$ of infinite plays (when studying TGs). An objective is state-based (resp. location-based) if it depends solely on the sequence of states (resp. of locations) in a path or play. Any location-based objective is state-based.

We use the following classical location-based objectives. A reachability objective for a set $F$ of locations is the set of plays that pass through a location in $F$. The complement of a reachability objective is a safety objective; given a set $F$, it is the set of plays that never visit a location in $F$. A Büchi objective for a set $F$ contains all plays that pass through locations in $F$ infinitely often and the complement co-Büchi objective consists of plays traversing locations in $F$ finitely often. The parity objective for a priority function $p$ over the set of locations requires that the smallest priority seen infinitely often is even.

Fix $F$ a set of locations and $p$ a priority function. The aforementioned objectives are formally defined as follows.

• •

  $\mathsf{Reach}(F)=\{(\ell_{0},\nu_{0})(m_{0}^{(1)},m_{0}^{(2)})\ldots\in\mathsf{Plays}(\mathcal{G})\mid\exists\,n,\,\ell_{n}\in F\}$;

• •

  $\mathsf{Safe}(F)=\{(\ell_{0},\nu_{0})(m_{0}^{(1)},m_{0}^{(2)})\ldots\in\mathsf{Plays}(\mathcal{G})\mid\forall\,n,\,\ell_{n}\notin F\}$.

• •

  $\mathsf{B\ddot{u}chi}(F)=\{(\ell_{0},\nu_{0})(m_{0}^{(1)},m_{0}^{(2)})\ldots\in\mathsf{Plays}(\mathcal{G})\mid\forall\,j,\,\exists\,n\geq j,\,\ell_{n}\in F\}$;

• •

  $\mathsf{coB\ddot{u}chi}(F)=\{(\ell_{0},\nu_{0})(m_{0}^{(1)},m_{0}^{(2)})\ldots\in\mathsf{Plays}(\mathcal{G})\mid\exists\,j,\,\forall\,n\geq j,\,\ell_{n}\notin F\}$;

• •

  $\mathsf{Parity}(p)=\{(\ell_{0},\nu_{0})(m_{0}^{(1)},m_{0}^{(2)})\ldots\in\mathsf{Plays}(\mathcal{G})\mid(\liminf_{n\to\infty}p(\ell_{n}))\bmod 2=0\}$.

In games, we distinguish objectives and winning conditions. We adopt the definition of [20]. Let $\Psi$ be an objective. It is desirable to have victory be achieved in a physically meaningful way: for example, it is unrealistic to have a safety objective be achieved by stopping time. This motivates a restriction to time-divergent plays. However, this requires $\mathcal{P}_{1}$ to force the divergence of plays, which is not reasonable, as $\mathcal{P}_{2}$ can stall using delays with zero time units. Thus we also declare winning time-convergent plays where $\mathcal{P}_{1}$ is blameless. Let $\textsf{Blameless}_{1}$ denote the set of $\mathcal{P}_{1}$-blameless plays, which we define in the following way.

Let $\pi=s_{0}(m_{0}^{(1)},m_{0}^{(2)})s_{1}\ldots$ be a (possibly finite) play. We say $\mathcal{P}_{1}$ is not responsible (or not to be blamed) for the transition at step $n$ in $\pi$ if either $d_{n}^{(2)}<d_{n}^{(1)}$ ($\mathcal{P}_{2}$ is faster) or $d_{n}^{(1)}=d_{n}^{(2)}$ and $s_{n}\xrightarrow{d_{n}^{(1)},a_{n}^{(1)}}s_{n+1}$ does not hold in $\mathcal{T}(\mathcal{A})$ ($\mathcal{P}_{2}$’s move was selected and did not have the same target state as $\mathcal{P}_{1}$’s) where $m_{n}^{(i)}=(d_{n}^{(i)},a_{n}^{(i)})$ for $i\in\{1,2\}$. The set $\textsf{Blameless}_{1}$ is formally defined as the set of infinite plays $\pi$ such that there is some $j$ such that for all $n\geq j$, $\mathcal{P}_{1}$ is not responsible for the transition at step $n$ in $\pi$.

Given an objective $\Psi$, we set the winning condition $\mathsf{WC}_{1}(\Psi)$ for $\mathcal{P}_{1}$ to be the set of plays

Winning conditions for $\mathcal{P}_{2}$ are defined by exchanging the roles of the players in the former definition.

We consider that the two players are adversaries and have opposite objectives, $\Psi$ and $\neg\Psi$ (shorthand for $\mathsf{Plays}(\mathcal{G})\setminus\Psi$). Let us note that there may be plays $\pi$ such that $\pi\notin\mathsf{WC}_{1}(\Psi)$ and $\pi\notin\mathsf{WC}_{2}(\neg\Psi)$, e.g., any time-convergent play in which neither player is blameless.

A winning strategy for $\mathcal{P}_{i}$ for an objective $\Psi$ from a state $s_{0}$ is a strategy $\sigma_{i}$ such that $\mathsf{Outcome}_{i}(\sigma_{i},s_{0})\subseteq\mathsf{WC}_{i}(\Psi)$. Move-independent strategies are known to suffice for timed automaton games with state-based objectives [20].

We consider two different problems for an objective $\Psi$. The first is the verification problem for $\Psi$, which asks given a timed automaton whether all time-divergent initial paths satisfy the objective. Second is the realizability problem, which asks whether in a timed automaton game with objective $\Psi$, $\mathcal{P}_{1}$ has a winning strategy from the initial state.