One-Clock Synthesis Problems

There are many variants of timed games in the literature, depending on whether the players must enforce a non-Zeno play, who controls the elapse of time, concurrent actions, winning conditions, etc. [3, 22, 9, 38, 28, 4, 16, 14, 33, 21]. Following prior works [13, 32], we consider asymmetric (only one player can elapse time), infinite-duration turn-based games that can be considered as timed generalisation of Büchi-Landweber games [10]. There are two players, called $\mathrm{Timer}$ and $\mathrm{Monitor}$, who play taking turns in a strictly alternating fashion. In the $i$th round, $\mathrm{Timer}$ chooses a letter $a_i$ from a finite alphabet along with a nonnegative rational time delay ${\tau }_i$, and $\mathrm{Monitor}$ responds with a letter $b_i$ from a finite alphabet. Together, the players generate an infinite play $\pi =(a_1,b_1,{\tau }_1)(a_2,b_2,{\tau }_2)\mathrm{\cdots }$. The winning set of either $\mathrm{Timer}$ or $\mathrm{Monitor}$ is specified by a nondeterministic timed automaton. For comparison, the easier special case where the winning set is given by a deterministic or history deterministic timed automaton has been previously studied (e.g., [16, 7]). Given our undecidability results, we do not consider a more general symmetric variant in which both players may elapse time.

We investigate the timed reactive synthesis problem, which asks if a given player has a strategy ensuring that every play that conforms to the strategy is winning for that player. We distinguish four variants of this problem, depending on which player’s winning set is specified (note the lack of complement closure of NTA languages) and for which player the winning strategy is sought. We also study the timed Church synthesis problem, which asks if a given player has a winning finite-memory strategy (controller). For $\mathrm{Monitor}$, a controller is a DTA whose transitions output letters from $\mathrm{Monitor}$’s alphabet; for $\mathrm{Timer}$, it is a DFA whose transitions output letters from $\mathrm{Timer}$’s alphabet along with time delays.

This study of timed generalisations of Büchi–Landweber games was initiated in [13] in the setting where $\mathrm{Timer}$’s winning set is specified by an NTA, and the goal is to synthesise a controller for $\mathrm{Monitor}$. The main result of that work is the decidability of the resource-bounded timed Church synthesis problem, in which one seeks a controller using at most $k$ clocks, for a fixed $k$. Subsequently, [32] established the undecidability of the unrestricted (resource-unbounded) version, even when $\mathrm{Timer}$’s winning set is given by a two-clock NTA and $\mathrm{Monitor}$’s controller is sought. The decidability of this problem for ${\text{NTA}}_1$ (one-clock NTA) winning sets remained open, as did the status of other variants and of timed reactive synthesis. The present paper resolves all of these open questions in the negative.

Given as many as eight different decision problems, one could expect a complex decidability/complexity landscape. As our main technical contribution, we show that this is not the case: all eight decision problems are undecidable already in the simplest case where the winning sets are specified by ${\text{NTA}}_1$. These undecidability results significantly strengthen and generalise previously known lower bounds. They also demonstrate that restricting to ${\text{NTA}}_1$ does not lead to recovery of decidability of synthesis (game solving) problems, similarly as restricting to ${\text{NTA}}_1$ does not yield decidability of language universality and related problems over infinite words (as opposed to universality and related problems for ${\text{NTA}}_1$ languages of finite timed words [31]).

Proving undecidability for eight problems required four reductions. The cases where $\mathrm{Monitor}$’s winning set is specified by an ${\text{NTA}}_1$ are easily shown undecidable by reductions from the ${\text{NTA}}_1$ universality and sampled universality problems [1, 25]. Undecidability proofs in the other case, where $\mathrm{Timer}$’s winning set is specified, constitute the technical core of the paper, and proceed by reductions from two undecidable problems for lossy counter machines: boundedness and repeated reachability [29, 34].

Finally, we also address the question of when finite memory is sufficient to win, that is when existence of a strategy implies existence of a controller. On one hand, we prove this finite-memory property for the player whose winning set is specified: for all ${\text{NTA}}_1$ specifications if this player is $\mathrm{Monitor}$, and only for the restricted case of reachability ${\text{NTA}}_1$ specifications if this player is $\mathrm{Timer}$. On the other hand, we demonstrate that the finite-memory property fails in all other cases: it is not satisfied in general by $\mathrm{Timer}$ when his winning set is specified; and the property fails for both $\mathrm{Timer}$ and $\mathrm{Monitor}$ when the opponent’s winning set is specified, even in case of reachability ${\text{NTA}}_1$ specifications.

It is well known that NTA exhibit close similarity to nondeterministic register automata (NRA), known also as finite-memory automata [23] (see e.g. [20] for a formal connection between the models). Register automata input data values (in place of timestamps) and use registers (in place of clocks) to store data values ([35] is an excellent survey of automata models for data setting). For many language-related problems, like emptiness (reachability), universality or inclusion, register automata admit exactly the same (un)decidability results [15] that are known for timed automata [31, 25]. Language closure properties are also analogous in both settings. Confirming these deep similarities further, [32] proves undecidability of the timed Church synthesis problem for winning sets specified by NTA with two clocks, as well as undecidability of the data Church synthesis for winning sets specified by NRA with two registers. Similar studies of data generalisation of Büchi-Landweber games were also conducted independently in [17] and works cited therein [19, 18]. All our undecidability results transfer from the timed to the data setting: undecidability holds for all the eight variants of data reactive/Church synthesis problems, already when winning sets are specified by ${\text{NRA}}_1$ (NRA with one register). (These further results exceed the scope of the present paper and are planned to be included in the forthcoming full version of the paper.)

We start by defining the setting of timed games and the synthesis problems (Section 2). We also discuss the finite-memory property there. Section 3 is a warm-up where we deal with the easy cases of synthesis problems ($\mathrm{Monitor}$’s winning set is specified). Then in Section 4 we define the undecidable problems for lossy counter machines, to be used in the main technical part of the paper, Sections 5 and 6. In the two latter sections we provide the undecidability proofs in the hard case where $\mathrm{Timer}$’s winning set is specified. The last section contains final remarks. All omitted proofs can be found in the long version of this paper [26].

A non-deterministic timed automaton (NTA) $𝒜=⟨L,𝒳,\mathrm{\Sigma },L_i,L_f,\mathrm{\Delta }⟩$ consists of $L$, a finite set of locations with $L_i,L_f\subseteq L$ denoting the sets of initial and accepting locations, respectively; $𝒳$, a finite set of clocks; $\mathrm{\Sigma }$, a finite alphabet; and $\mathrm{\Delta }\subseteq L\times \mathrm{\Sigma }\times \mathrm{Guard}(𝒳)\times 2^{𝒳}\times L$, a finite set of transitions. A transition $(\mathrm{\ell },a,g,Y,{\mathrm{\ell }}^{\prime })\in \mathrm{\Delta }$ is written as $\mathrm{\ell }\stackrel{a,g,Y}{\to }{\mathrm{\ell }}^{\prime }$, omitting $g$ and $Y$ whenever they are $\top$ or $\mathrm{\varnothing }$, respectively. A set $A$ in place of $a$ specifies a set of transitions. The semantics of $𝒜\in \text{NTA}$ is a timed transition system $⟦𝒜⟧=(Q,Q_I,\to )$ such that: $Q=L\times {({\mathbb{Q}}_{\ge 0})}^{𝒳}$ is the set of configurations (i.e., location-valuation pairs), $Q_I=L_i\times \{0^{𝒳}\}$ is the set of initial configurations, and $\to$ is the set of edges. We have $(\mathrm{\ell },\nu )\stackrel{\delta ,\tau }{\to }({\mathrm{\ell }}^{\prime },{\nu }^{\prime })$ if and only if $\delta =(\mathrm{\ell },a,g,Y,{\mathrm{\ell }}^{\prime })\in \mathrm{\Delta }$ is a transition of $𝒜$ such that $\nu +\tau \vDash g$, and ${\nu }^{\prime }=(\nu +\tau )[Y≔0]$. A run $\rho$ in $𝒜$ is a sequence of edges $\rho =({\mathrm{\ell }}_1,{\nu }_1)\stackrel{{\delta }_1,{\tau }_1}{\to }({\mathrm{\ell }}_2,{\nu }_2)\stackrel{{\delta }_2,{\tau }_2}{\to }\mathrm{\dots }$ of $⟦𝒜⟧$ such that ${\mathrm{\ell }}_1\in L_i$. A timed word $w=(a_1,t_1)(a_1,t_2)\mathrm{\dots }$ over $\mathrm{\Sigma }$ labels a run $\rho$ of $𝒜$ when, for all $i\in {\mathbb{N}}_{>0}$, ${\delta }_i=({\mathrm{\ell }}_i,a_i,g,Y,{\mathrm{\ell }}_{i+1})$ and $t_i={\sum }_{j=1}^i{\tau }_j$. We adopt Büchi acceptance: a run is accepting if is visits an accepting location infinitely often, in which case we say that the word that labels that run is accepted by $𝒜$. The language of $𝒜\in \text{NTA}$, denoted $ℒ(𝒜)$, is the set of timed words accepted by $𝒜$.

We also use reachability acceptance, where a run is accepting once it visits an accepting location at least once (like in the setting of finite words). With this acceptance, the language $L$ of infinite timed words accepted by an NTA is determined uniquely by the language $L^{\prime }$ of finite timed words having a run ending in an accepting location. We write $L=\mathrm{Reach}(L^{\prime })$. So defined reachability NTA can be seen as a (strict) subclass of NTA, denoted as reach-NTA.

Apart from reach-NTA, we consider also other subclasses of NTA. For instance ${\text{NTA}}_k$ consists of nondeterministic timed automata with a fixed number $k=|𝒳|$ of clocks. DTA is the class of deterministic timed automata, where $|L_i|=1$ and for all locations $\mathrm{\ell }\in L$ and letters $a\in \mathrm{\Sigma }$, the guards $g$ appearing in transitions of the form $(\mathrm{\ell },a,g,\mathrm{\_},\mathrm{\_})$ form a partition of ${\mathbb{Q}}_{\ge 0}^{|𝒳|}$. We also consider a superclass ${\text{NTA}}^{\text{res}}$ of 1-resetting timed automata (defined in Section 6), an extension by a limited form of $\epsilon$-transitions that reset a clock every time it equals 1. The class of NTA with $\epsilon$-transition is strictly more expressive than NTA [6]; we discuss this choice at the end of this section, and in Sections 6 and 7.

We combine the notation for sub- and superclasses and write ${\text{reach-}\text{NTA}}_1$, ${\text{reach-}\text{NTA}}_1^{\text{res}}$, for the one-clock automata from reach-NTA, and for the 1-resetting extension thereof.

Given $L$ a timed language, we denote by $\widehat{L}$ its complement. The universality problem asks, given $𝒜$, if $\widehat{ℒ(𝒜)}=\mathrm{\varnothing }$. This problem is known to be undecidable for ${\text{NTA}}_1$ [25].

In this paper we consider turn-based games between two players called here $\mathrm{Timer}$ and $\mathrm{Monitor}$, where a winning condition is given by an ${\text{NTA}}_1$ (resp. ${\text{NTA}}_1^{\text{res}}$).

Intuitively, $\mathrm{Owner}$ specifies the player who wins a play if it belongs to $ℒ(𝒜)$. As NTA are not stable by complement [2], the choice of the owner of the winning condition is not innocuous, and the winning condition of the opponent may no longer be an NTA language. We investigate decision problems asking about existence of a winning strategy of $\mathrm{Agent}$. Again, the choice of $\mathrm{Agent}$ is not innocuous, as we do not know if the games studied by us are determined. In view of our undecidability results, we do not consider a symmetric variant of timed games where both players would submit time delays, as this variant would generalise the above one.

A timed game proceeds in rounds. Each $i$th round ($i\in {\mathbb{N}}_{>0}$) starts by $\mathrm{Timer}$’s choice of $a_i\in \mathrm{T}$ and a delay ${\tau }_i\in {\mathbb{Q}}_{\ge 0}$, followed by a response $b_i\in \mathrm{M}$ of $\mathrm{Monitor}$. This results in a play which is a timed word $(a_1,b_1,t_1)(a_2,b_2,t_2)\mathrm{\cdots }$ over the alphabet $\mathrm{T}\times \mathrm{M}$, where $t_i={\sum }_{j=1}^i{\tau }_j$. $\mathrm{Owner}$ wins the play if it belongs to $ℒ(𝒜)$, otherwise its opponent wins.

A strategy for a player is a function that gives its next move as a function of the moves of its opponent up to now. Formally, a strategy for $\mathrm{Timer}$ is a function ${\sigma }_{\mathrm{T}}:{\mathrm{M}}^{\ast }\to \mathrm{T}\times {\mathbb{Q}}_{\ge 0}$ whereas a strategy for $\mathrm{Monitor}$ is a function ${\sigma }_{\mathrm{M}}:{(\mathrm{T}\times {\mathbb{Q}}_{\ge 0})}^{+}\to \mathrm{M}$. We say that a play $w=(a_1,b_1,t_1)(a_2,b_2,t_2)\mathrm{\dots }$ conforms to $\mathrm{Timer}$’s strategy ${\sigma }_{\mathrm{T}}$ (resp. $\mathrm{Monitor}$’s strategy ${\sigma }_{\mathrm{M}}$) if all (timed) letters in it conform to the strategy’s output: $(a_i,{\tau }_i)={\sigma }_{\mathrm{T}}(b_1\mathrm{\cdots }{b}_{i-1})$ for all $i\in {\mathbb{N}}_{>0}$ (resp., $b_i={\sigma }_{\mathrm{M}}((a_1,t_1)\mathrm{\cdots }(a_i,t_i))$ for all $i\in {\mathbb{N}}_{>0}$). A strategy is winning for a player if and only if every play $w$ that conforms to it is winning for that player (i.e., $w\in ℒ(𝒜)$ if and only if this player is the owner).

A controller is a finite-memory strategy represented by a DTA with outputs. Specifically, a $\mathrm{Monitor}$’s controller is a DTA with outputs from $\mathrm{M}$, whose transitions are of the form $\delta =(\mathrm{\ell },a,g,Y,{\mathrm{\ell }}^{\prime },b)$, where $b\in \mathrm{M}$ is the output. The controller induces the strategy ${\sigma }_{\mathrm{M}}$ that maps $w=(a_1,t_1)\mathrm{\cdots }(a_i,t_i)$ to the last output of the run over $w$. For $\mathrm{Timer}$, the notion of controller is more tricky since it needs to produce timestamps. We let $\mathrm{Timer}$’s controllers output pairs $(a,\tau )\in \mathrm{T}\times {\mathbb{Q}}_{\ge 0}$, where $\tau$ is interpreted as the next delay. Formally, it is defined as a DFA (DTA with no clocks) with outputs from $\mathrm{T}\times {\mathbb{Q}}_{\ge 0}$, whose transitions are of the form $\delta =(\mathrm{\ell },b,{\mathrm{\ell }}^{\prime },a,\tau )$, where $(a,\tau )\in \mathrm{T}\times {\mathbb{Q}}_{\ge 0}$ is the output, additionally equipped with an initial move $(a_1,{\tau }_1)\in \mathrm{T}\times {\mathbb{Q}}_{\ge 0}$. Note the apparent restriction of $\mathrm{Timer}$’s controllers, compared to general strategies, namely the set of delays used by a controller is finite. A controller induces the strategy ${\sigma }_{\mathrm{T}}$ that maps the empty word to $(a_1,{\tau }_1)$, and a nonempty word $b_1\mathrm{\cdots }{b}_i$ to the last output of the run over $w$.

We investigate decision problems to determine whether $\mathrm{Agent}$ wins, i.e., whether $\mathrm{Agent}$ has a winning strategy. We distinguish four cases, depending on the choice of $\mathrm{Owner}\in \{\mathrm{Timer},\mathrm{Monitor}\}$ and $\mathrm{Agent}\in \{\mathrm{Timer},\mathrm{Monitor}\}$. Furthermore, in each of the four cases we consider two distinct decision problems: given a timed game,

• $\mathrm{■}$

  the timed reactive synthesis asks if $\mathrm{Agent}$ has a winning strategy;

• $\mathrm{■}$

  the timed Church synthesis asks if $\mathrm{Agent}$ has a winning controller.

The problems coincide in some cases (see Table 1 for a summary). Most importantly, if $\mathrm{Monitor}$ is both the owner of the winning condition, and also the agent of the synthesis problem, then whenever it has a winning strategy it also has a controller. Likewise for $\mathrm{Timer}$, but only in the restricted case of ${\text{reach-}\text{NTA}}_1$ winning conditions:

In all the remaining cases the two synthesis problems do not coincide, namely existence of a winning strategy does not imply existence of a controller: first, when $\mathrm{Timer}$ is both the owner of the winning condition, and also the agent of the synthesis problem, but the winning condition is an arbitrary ${\text{NTA}}_1$ language; second, when the owner is different from the agent, even in the case of reachability ${\text{NTA}}_1$ winning conditions:

1. 1.

   We start with the case $\mathrm{Owner}=\mathrm{Timer}$ and $\mathrm{Agent}=\mathrm{Monitor}$. Let $\mathrm{Timer}$’s alphabet be trivial (singleton), and hence omitted below; $\mathrm{Timer}$ thus essentially chooses only timestamps. Let $\mathrm{Monitor}$’s alphabet $\mathrm{M}=\{a,b\}$, and let $\mathrm{Timer}$’s winning condition contain timed words containing some letter ($a$ or $b$) at distance 1, that is timed words that contain both $(a,t)$ and $(a,t+1)$, or both $(b,t)$ and $(b,t+1)$, for some $t\in {\mathbb{Q}}_{\ge 0}$. The condition is readily seen to be recognised by a reachability ${\text{NTA}}_1$. $\mathrm{Monitor}$ has a winning strategy in this game: it wins by always playing the same letter (say $a$) unless timestamp $t-1$ appeared earlier in the play, in which case it plays the opposite of the letter that was played there. On the other hand, $\mathrm{Monitor}$ has no winning controller, as winning requires storing unboundedly many different timestamps (together with letters used at them).

   For the case $\mathrm{Owner}=\mathrm{Monitor}$ and $\mathrm{Agent}=\mathrm{Timer}$, we choose both alphabets to be trivial (and hence omitted below). The play is thus just a monotonic sequence $t_1\le t_2\le \mathrm{\cdots }$ of timestamps, chosen by $\mathrm{Timer}$. Let $\mathrm{Monitor}$’s winning condition consist of those sequences which either exceed 1 at some point ($t_i>1$ for some $i\in {\mathbb{N}}_{>0}$), or repeat a timestamp ($t_i=t_{i+1}$ for some $i\in {\mathbb{N}}_{>0}$). Both conditions, and hence their union, are recognised by reachability ${\text{NTA}}_1$. Furthermore, $\mathrm{Timer}$ has a winning strategy by producing a Zeno word bounded by 1, but $\mathrm{Timer}$ has no winning controller. Indeed, in order to win, $\mathrm{Timer}$ should use strictly positive delays only, and therefore, since every controller uses only finitely many different delays, the bound 1 is inevitably exceeded.

2. 2.

   Consider the case $\mathrm{Owner}=\mathrm{Agent}=\mathrm{Timer}$. We use the same idea as in the previous case: $\mathrm{Timer}$ can win only by producing a Zeno word. Let $\mathrm{Timer}$’s alphabet be trivial (hence omitted below); $\mathrm{Timer}$ thus essentially chooses only timestamps. Let $\mathrm{Monitor}$’s alphabet be $\mathrm{M}=\{\begin{array}{c}\text{<object type="image/svg+xml" data="custom\_symbols/check4.pdf2svg.svg" id="S2.I4.i2.p1.m6.1.g1nest" class="ltx\_graphics ltx\_img\_square" width="13" height="14" style="width: 18px; height: unset; max-width: 100\%"></object>}\end{array},\begin{array}{c}\text{<object type="image/svg+xml" data="custom\_symbols/cross2.pdf2svg.svg" id="S2.I4.i2.p1.m6.2.g1nest" class="ltx\_graphics ltx\_img\_square" width="12" height="14" style="width: 18px; height: unset; max-width: 100\%"></object>}\end{array}\}$, and let $\mathrm{Timer}$’s winning condition be the union of two sets: the timed words $w=(b_1,t_1)(b_2,t_2)\mathrm{\cdots }\in {(\mathrm{M}\times {\mathbb{Q}}_{\ge 0})}^{\omega }$ that never exceed 1 labelled exclusively by $\begin{array}{c}\text{<object type="image/svg+xml" data="custom\_symbols/check4.pdf2svg.svg" id="S2.I4.i2.p1.m9.1.g1nest" class="ltx\_graphics ltx\_img\_square" width="13" height="14" style="width: 18px; height: unset; max-width: 100\%"></object>}\end{array}$, i.e., and $b_i=\begin{array}{c}\text{<object type="image/svg+xml" data="custom\_symbols/check4.pdf2svg.svg" id="S2.I4.i2.p1.m11.1.g1nest" class="ltx\_graphics ltx\_img\_square" width="13" height="14" style="width: 18px; height: unset; max-width: 100\%"></object>}\end{array}$ for all $i\in {\mathbb{N}}_{>0}$; and the timed words such that for some $i\in {\mathbb{N}}_{>0}$ we have , $b_1=\mathrm{\cdots }=b_i=\begin{array}{c}\text{<object type="image/svg+xml" data="custom\_symbols/check4.pdf2svg.svg" id="S2.I4.i2.p1.m15.1.g1nest" class="ltx\_graphics ltx\_img\_square" width="13" height="14" style="width: 18px; height: unset; max-width: 100\%"></object>}\end{array}$ and $b_{i+1}=\begin{array}{c}\text{<object type="image/svg+xml" data="custom\_symbols/cross2.pdf2svg.svg" id="S2.I4.i2.p1.m16.1.g1nest" class="ltx\_graphics ltx\_img\_square" width="12" height="14" style="width: 18px; height: unset; max-width: 100\%"></object>}\end{array}$. $\mathrm{Timer}$ has a winning strategy by producing a strictly monotonic Zeno word bounded by 1. On the other hand a violation of strict monotonicity, namely the equality $t_i=t_{i+1}$, is punished by $\mathrm{Monitor}$ playing $b_{i+1}=\begin{array}{c}\text{<object type="image/svg+xml" data="custom\_symbols/cross2.pdf2svg.svg" id="S2.I4.i2.p1.m20.1.g1nest" class="ltx\_graphics ltx\_img\_square" width="12" height="14" style="width: 18px; height: unset; max-width: 100\%"></object>}\end{array}$. Therefore, $\mathrm{Timer}$ has no winning controller for the same reason as in the previous case.

$◀$

As our main contribution, we obtain undecidability in all cases of both the reactive and Church synthesis problems, even under the very restricted case where the timed winning condition is specified by an ${\text{NTA}}_1$ (or by a ${\text{reach-}\text{NTA}}_1^{\text{res}}$ in one of the variants, see Table 2 for a summary). Our reductions in the case of the reactive synthesis problem work uniformly, regardless of which player is the $\mathrm{Agent}$. Therefore Table 2 has six rather than eight entries. These six cases require four different reductions, and hence each table entry indicates the problem we reduce from. When $\mathrm{Timer}$ is the owner of the winning condition, some undecidable problems for lossy counter machines (LCM) turn out suitable for reductions, namely repeated reachability and boundedness [34] (these results are the core technical part); and when $\mathrm{Monitor}$ is the owner, we use two variants of universality of ${\text{NTA}}_1$ languages (these reductions are comparatively simpler).

The table specifies the class of winning conditions $𝒜$ for which we prove undecidability: $𝒜\in {\text{NTA}}_1$, except for one exception where we need 1-resetting reachability ${\text{NTA}}_1$, a slight extension of reachability ${\text{NTA}}_1$ that uses a limited form of $\epsilon$-transitions that reset the clock whenever it reaches value 1. We believe that resorting to ${\text{NTA}}_1^{\text{res}}$ does not weaken our results, for the following two reasons: first, while ${\text{NTA}}_1$ with $\epsilon$-transitions correspond to nondeterministic one-register automata (${\text{NRA}}_1$) with guessing (see [20]), ${\text{NTA}}_1^{\text{res}}$ still correspond to ${\text{NRA}}_1$ without guessing; second, all our undecidability results translate from the timed setting to the data setting, where the winning sets are specified by ${\text{NRA}}_1$ without guessing.

We reduce from the ${\text{NTA}}_1$ universality problem (does the language of a given $𝒜\in {\text{NTA}}_1$ contain all infinite timed words?) [25]. Given an ${\text{NTA}}_1$ $𝒜$ over alphabet $\mathrm{\Sigma }$, we construct a timed game where $\mathrm{Monitor}$’s alphabet is the singleton $\{\mathrm{\square }\}$, $\mathrm{Timer}$’s alphabet is $\mathrm{\Sigma }$, and the winning condition of $\mathrm{Monitor}$ is $ℒ(𝒜)$ (ignoring the letters “$\mathrm{\square }$”). Therefore, $\mathrm{Timer}$ wins if it produces a timed word over $\mathrm{\Sigma }$ that is not in $ℒ(𝒜)$. Thus, $\mathrm{Timer}$ has a winning strategy if $ℒ(𝒜)$ does not contain all timed words, and $\mathrm{Monitor}$ has a winning controller otherwise (the trivial memoryless one that keeps emitting “$\mathrm{\square }$”). $◀$

For undecidability of the timed Church synthesis problem when $\mathrm{Agent}=\mathrm{Timer}$, we turn to the sampled universality problem, a variant that assumes the sampled semantics ${ℒ}_{\delta }(\mathrm{\_})$ of timed automata. Given $\delta >0$, we say that a timed word has granularity $\delta$ if all its timestamps are multiplicities of $\delta$, and define ${ℒ}_{\delta }(𝒜)\subseteq ℒ(𝒜)$ as the language of all timed words of granularity $\delta$ in $ℒ(𝒜)$. Given an NTA $𝒜$, the sampled universality problem asks if for all $\delta >0$, the language ${ℒ}_{\delta }(𝒜)$ contains all timed words of granularity $\delta$. The problem (called universal sampled universality in [1]) is known to be undecidable for ${\text{NTA}}_1$ [1, Thm. 3].

We proceed similarly as in Theorem 4, but reduce from the ${\text{NTA}}_1$ sampled universality problem. Given an ${\text{NTA}}_1𝒜$ over alphabet $\mathrm{\Sigma }$, we construct the same timed game as in Theorem 4: $\mathrm{M}=\{\mathrm{\square }\}$, $\mathrm{T}=\mathrm{\Sigma }$, and the winning condition of $\mathrm{Monitor}$ is $ℒ(𝒜)$ (ignoring “$\mathrm{\square }$”).

If $\mathrm{Timer}$ has a winning controller $𝒞$ in this game, we take an arbitrary rational $\delta >0$ such that all positive delays used by $𝒞$ are multiplicities of $\delta$, and deduce that any infinite timed word output by $𝒞$ has granularity $\delta$ and is not in ${ℒ}_{\delta }(𝒜)$.

In the opposite direction, suppose a timed word $w$ of granularity $\delta$ is not accepted by $𝒜$. Assume, w.l.o.g., that $𝒜$ has a run labeled by $w$. We build a word $w^{\prime }$ whose run visits only finitely many different configurations. Let $M$ be the maximal constant appearing in the guards of $𝒜$. If the valuations in the run labeled by $w$ never exceed $M$, i.e. if $𝒜$ always resets the clock when it goes over $M$, then we take $w^{\prime }=w$ and we are done because every valuation is always a multiplicity of $\delta$ and there are finitely many thereof between $0$ and $M$. Otherwise, let $t_M>M$ be the first valuation in the run that exceeds $M$. We obtain $w^{\prime }$ by modifying $w$ so that every time the valuation in the run is over $M$, it is exactly $t_M$ (using repeating timestamps if necessary), but the run is unchanged when the valuation is at most $M$. Since valuations over $M$ are indistinguishable by $𝒜$, $w^{\prime }$ is not accepted by $𝒜$. Therefore no accepting locations appear on the run from some point on, and hence the run necessarily forms some loop without accepting locations on it. We replace $w^{\prime }$ by the timed word $w^{\prime \prime }$ obtained by letting $𝒜$ repeat the loop infinitely. Like $w^{\prime }$, the word $w^{\prime \prime }$ has granularity $\delta$ and is not in ${ℒ}_{\delta }(𝒜)$, but $w^{\prime \prime }$ is additionally ultimately periodic when seen as a sequence of letter-delay pairs $w^{\prime \prime }=(a_1,{\tau }_1)(a_2,{\tau }_2)\mathrm{\cdots }$. In consequence, $\mathrm{Timer}$ has a winning controller that produces $w^{\prime \prime }$. $◀$

In the course of the game, $\mathrm{Timer}$ is tasked with producing an increasingly longer timed word supposed to be an encoding of a run of $ℳ$. However, $\mathrm{Timer}$ may also cheat and produce a timed word which contains an error and therefore is not a correct run encoding. We distinguish four types of errors. In order to prevent $\mathrm{Timer}$ from cheating, $\mathrm{Monitor}$ verifies if the encoding proposed by $\mathrm{Timer}$ is correct, and if it is not, $\mathrm{Monitor}$ has to declare the detected type of error correctly, and immediately, that is in the same round the error occurs. Therefore one way of winning by $\mathrm{Timer}$ is to see $s$ infinitely often while seeing no error declared by $\mathrm{Monitor}$ (using cheating or not); or to mislead $\mathrm{Monitor}$ about the correctness of encoding by cheating and either seeing no immediate error declaration, or seeing an error declaration of wrong type. On the other hand, when $\mathrm{Monitor}$ manages to declare immediately the correct type of error, the play is winning for it irrespectively of the continuation.

A central ingredient of our reduction is the encoding of runs of $ℳ$ as timed words. Let ${\mathrm{\Sigma }}_{ℳ}=𝒞\cup ℐ$. We first introduce the valuation encoding. For a valuation $\nu =(v_1,v_2,v_3,v_4)\in {\mathbb{N}}^{𝒞}$ define $\mathrm{enc}(\nu )=c_1^{v_1}{c}_2^{v_2}{c}_3^{v_3}{c}_4^{v_4}$, a finite untimed word consisting of four segments. The set of all such encodings is ${\mathrm{ValEnc}}_{ℳ}=c_1^{\ast }{c}_2^{\ast }{c}_3^{\ast }{c}_4^{\ast }$.

Next, we define the run encoding. The function $\mathrm{enc}:{\mathrm{Runs}}_{ℳ}\to {\mathrm{\Sigma }}_{ℳ}^{\omega }$ maps a run $\rho =(s_0,{\nu }_0)\stackrel{I_1}{\to }(s_1,{\nu }_1)\stackrel{I_2}{\to }\mathrm{\cdots }$ to the infinite untimed word $\mathrm{enc}(\rho )=\mathrm{enc}({\nu }_0)I_1\mathrm{enc}({\nu }_1)I_2\mathrm{\cdots }$. Let ${\mathrm{RunEnc}}_{ℳ}=\{\mathrm{enc}(\rho )\mid \rho \in {\mathrm{Runs}}_{ℳ}\}$ be the set of valid untimed encodings.

Intuitively, we exploit the timed structure of a word to enforce the correctness of run encodings (see Lemma 8). To this end, we define a timed language ${\mathrm{RunEnc}}_{ℳ}^{𝕋}$. We specify it using an untimed $\omega$-regular language ${\mathrm{Reg}}_{ℳ}$ which enforces the structural shape of runs of $ℳ$, and timed languages $A_{ℳ}^{𝕋}$, $B_{ℳ}^{𝕋}$ and $C_{ℳ}^{𝕋}$, which impose additional timed properties. Let ${\mathrm{Reg}}_{ℳ}$ consist of all (untimed) words $w\in {\mathrm{\Sigma }}_{ℳ}^{\omega }$ that satisfy the following regular conditions:

Block structure:

$w$ is an infinite interleaving of valuation encodings and instructions, i.e., $w$ is of the form $w=\mathrm{enc}({\nu }_0)I_1\mathrm{enc}({\nu }_1)I_2\mathrm{\cdots }\in {({\mathrm{ValEnc}}_{ℳ}ℐ)}^{\omega }$ with $I_1$ starting from $s_0$.

Instruction compatibility:

Each instruction’s target state is the source state of the next one, i.e., for every infix $I_i{𝒞}^{\ast }{I}_{i+1}$ we have $I_i=(\mathrm{\_},\mathrm{\_},s)$ and $I_{i+1}=(s_{,}\mathrm{\_},\mathrm{\_})$ for some $s$.

Consistency with zero tests:

every infix $I_i\mathrm{enc}({\nu }_i)I_{i+1}$ of $w$ with $I_{i+1}\in {ℐ}_{\mathrm{zt}}^c$ verifies $\mathrm{enc}({\nu }_i)\in {(𝒞\setminus \{c\})}^{\ast }$, i.e., the symbol $c$ does not appear in $\mathrm{enc}({\nu }_i)$.

Clearly ${\mathrm{Reg}}_{ℳ}\supseteq {\mathrm{RunEnc}}_{ℳ}$. Let ${\mathrm{Reg}}_{ℳ}^{𝕋}={\mathrm{untime}}^{-1}({\mathrm{Reg}}_{ℳ})$ contain all timed words whose untiming is in ${\mathrm{Reg}}_{ℳ}$. We define ${\mathrm{RunEnc}}_{ℳ}^{𝕋}$ as the intersection of four timed languages:

where $A_{ℳ}^{𝕋}$, $B_{ℳ}^{𝕋}$ and $C_{ℳ}^{𝕋}$ are languages of infinite timed words $w$ satisfying the conditions given below. For simplicity, we define the condition for $C_{ℳ}^{𝕋}$ (the most intricate), assuming that $w\in L={\mathrm{Reg}}_{ℳ}^{𝕋}\cap A_{ℳ}^{𝕋}\cap B_{ℳ}^{𝕋}$, as it is irrelevant how it treats words outside $L$.

Strict monotonicity ($A_{ℳ}^{𝕋}$):

$w$ is strictly monotonic (no timestamp repeats).

Blocks align to unit intervals ($B_{ℳ}^{𝕋}$):

symbols from $ℐ$ appear in $w$ with consecutive integer timestamps starting from $1$.

Well-alignment of valuations encodings ($C_{ℳ}^{𝕋}$):

every maximal infix of $w$ of the form $\mathrm{enc}({\nu }_i)$   $I_i\mathrm{enc}({\nu }_{i+1})$ verifies the following conditions, for all counters $c\in 𝒞$:

1. 1.

   if $I_i\notin {ℐ}_{\mathrm{dec}}^c\cup {ℐ}_{\mathrm{inc}}^c$ then ${\nu }_{i+1}(c)\le {\nu }_i(c)$, and a timed letter $(c,t)$ appears in $\mathrm{enc}({\nu }_{i+1})$ only if $(c,t-1)$ appears in $\mathrm{enc}({\nu }_i)$;

2. 2.

   if $I_i\in {ℐ}_{\mathrm{inc}}^c$, then ${\nu }_{i+1}(c)\le {\nu }_i(c)+1$, and the encoding verifies the case 1 except for a (potential) one extra letter $c$ appearing in the beginning of the $c$-segment in $\mathrm{enc}({\nu }_{i+1})$ within less than one unit of time from the first symbol $c$ of $\mathrm{enc}({\nu }_i)$.

3. 3.

   if $I_i\in {ℐ}_{\mathrm{dec}}^c$, then ${\nu }_{i+1}(c)\le {\nu }_i(c)-1$, and the encoding verifies the case 1 except for the first letter $c$ appearing in $\mathrm{enc}({\nu }_i)$ which can not appear in $\mathrm{enc}({\nu }_{i+1})$.

According to the definition of $C_{ℳ}^{𝕋}$, every increment (resp. decrement) of a counter $c$ results in adding (resp. removing) one letter $c$ in the beginning of the $c$-segment. An illustration is provided in Figure 1.

We define the timed synthesis game where $\mathrm{Timer}$’s actions are $\mathrm{T}={\mathrm{\Sigma }}_{ℳ}$ and $\mathrm{Monitor}$’s actions are $\mathrm{M}=\{\begin{array}{c}\text{<object type="image/svg+xml" data="custom\_symbols/check4.pdf2svg.svg" id="S5.SS0.SSS0.P0.SPx3.p1.m4.1.g1nest" class="ltx\_graphics ltx\_img\_square" width="13" height="14" style="width: 18px; height: unset; max-width: 100\%"></object>}\end{array},{\begin{array}{c}\text{<object type="image/svg+xml" data="custom\_symbols/cross2.pdf2svg.svg" id="S5.SS0.SSS0.P0.SPx3.p1.m4.2.g1nest" class="ltx\_graphics ltx\_img\_square" width="12" height="14" style="width: 18px; height: unset; max-width: 100\%"></object>}\end{array}}_{\mathrm{R}},{\begin{array}{c}\text{<object type="image/svg+xml" data="custom\_symbols/cross2.pdf2svg.svg" id="S5.SS0.SSS0.P0.SPx3.p1.m4.3.g1nest" class="ltx\_graphics ltx\_img\_square" width="12" height="14" style="width: 18px; height: unset; max-width: 100\%"></object>}\end{array}}_{\mathrm{A}},{\begin{array}{c}\text{<object type="image/svg+xml" data="custom\_symbols/cross2.pdf2svg.svg" id="S5.SS0.SSS0.P0.SPx3.p1.m4.4.g1nest" class="ltx\_graphics ltx\_img\_square" width="12" height="14" style="width: 18px; height: unset; max-width: 100\%"></object>}\end{array}}_{\mathrm{B}},{\begin{array}{c}\text{<object type="image/svg+xml" data="custom\_symbols/cross2.pdf2svg.svg" id="S5.SS0.SSS0.P0.SPx3.p1.m4.5.g1nest" class="ltx\_graphics ltx\_img\_square" width="12" height="14" style="width: 18px; height: unset; max-width: 100\%"></object>}\end{array}}_{\mathrm{C}}\}$. For the definition of the winning condition it is crucial that all the languages ${\mathrm{Reg}}_{ℳ}^{𝕋},A_{ℳ}^{𝕋},B_{ℳ}^{𝕋}$ and $C_{ℳ}^{𝕋}$ can be defined locally: an infinite word $w$ belongs to ${\mathrm{Reg}}_{ℳ}^{𝕋}$ exactly when all (finite) prefixes of $w$ belong to a certain local language ${\mathrm{Reg}}_{ℳ}^{𝕋,\mathrm{\ell }}\subseteq {({\mathrm{\Sigma }}_{ℳ}\times {\mathbb{Q}}_{\ge 0})}^{\ast }$ of finite timed words, which is moreover recognised by a ${\text{reach-}\text{NTA}}_1$; and likewise for the $A_{ℳ}^{𝕋}$, $B_{ℳ}^{𝕋}$ and $C_{ℳ}^{𝕋}$. Specifically:

• $\mathrm{■}$

  ${\mathrm{Reg}}_{ℳ}^{𝕋,\mathrm{\ell }}$: the finite prefix satisfies the defining conditions of ${\mathrm{Reg}}_{ℳ}$.

• $\mathrm{■}$

  $A_{ℳ}^{𝕋,\mathrm{\ell }}$: the last two timestamps are nonequal (or the word is of length 1, the border case).

• $\mathrm{■}$

  $B_{ℳ}^{𝕋,\mathrm{\ell }}$: if the last letter is from $ℐ$, then no $ℐ$ appears in the last open unit interval, and $ℐ$ appears exactly one time unit before the last timestamp; and if the last letter is not from $ℐ$, some $ℐ$ occurs less that one unit before the last timestamp. (We omit the border case.)

• $\mathrm{■}$

  $C_{ℳ}^{𝕋,\mathrm{\ell }}$: the last timed letter of the word, if it is $(c,t)\in 𝒞\times {\mathbb{Q}}_{\ge 0}$, appears also one unit of time before as $(c,t-1)$, except when it is the first letter in the $c$-segment and the last instruction is an increment of $c$. Moreover, when $(c,t)$ is the first letter in the $c$-segment and the last instruction is a decrement of $c$, the language $C_{ℳ}^{𝕋,\mathrm{\ell }}$ requires that the first letter in the previous $c$-segment was removed, i.e., its timestamp is strictly smaller that $t-1$. As before, we conveniently assume that the word is in $L={\mathrm{Reg}}_{ℳ}^{𝕋,\mathrm{\ell }}\cap A_{ℳ}^{𝕋,\mathrm{\ell }}\cap B_{ℳ}^{𝕋,\mathrm{\ell }}$, as it is irrelevant which words from $\widehat{L}=\widehat{{\mathrm{Reg}}_{ℳ}^{𝕋,\mathrm{\ell }}}\cup \widehat{A_{ℳ}^{𝕋,\mathrm{\ell }}}\cup \widehat{B_{ℳ}^{𝕋,\mathrm{\ell }}}$ belong to $C_{ℳ}^{𝕋,\mathrm{\ell }}$.

Note that $C_{ℳ}^{𝕋,\mathrm{\ell }}$ is the most difficult one, and the only one for which we will need non-determinism.

The winning condition is also defined mostly locally, by a combination of restrictions imposed on $\mathrm{Timer}$’s or $\mathrm{Monitor}$’s moves. To this aim we use the projections of finite words, ${\mathrm{proj}}_{\mathrm{M}}:{(\mathrm{T}\times \mathrm{M}\times {\mathbb{Q}}_{\ge 0})}^{\ast }\to {\mathrm{M}}^{\ast }$ and ${\mathrm{proj}}_{\mathrm{T},𝕋}:{(\mathrm{T}\times \mathrm{M}\times {\mathbb{Q}}_{\ge 0})}^{\ast }\to {(\mathrm{T}\times {\mathbb{Q}}_{\ge 0})}^{\ast }$, as well as their inverses ${\mathrm{proj}}_{\mathrm{M}}^{-1}$ and ${\mathrm{proj}}_{\mathrm{T},𝕋}^{-1}$. We define $\mathrm{Timer}$’s winning set as

where $\mathrm{Inf}(s)$ is the (untimed) regular language “the location $s$ appears infinitely often”, $\mathrm{Reach}(V_{ℳ}^{𝕋})$ stands for the language of those infinite timed words which have some prefix in $V_{ℳ}^{𝕋}$, and $V_{ℳ}^{𝕋}$ itself is the following union of languages of finite timed words:

Thus, $\mathrm{Timer}$ wins if $s$ is occurring infinitely often and $\mathrm{Monitor}$ declares no error, i.e., plays exclusively $\begin{array}{c}\text{<object type="image/svg+xml" data="custom\_symbols/check4.pdf2svg.svg" id="S5.SS0.SSS0.P0.SPx3.p3.m16.1.g1nest" class="ltx\_graphics ltx\_img\_square" width="13" height="14" style="width: 18px; height: unset; max-width: 100\%"></object>}\end{array}$ moves, or some finite prefix of play is in $V_{ℳ}^{𝕋}$, namely $\mathrm{Monitor}$ declares a wrong type of error. Specifically, $\mathrm{Monitor}$ declares ${\begin{array}{c}\text{<object type="image/svg+xml" data="custom\_symbols/cross2.pdf2svg.svg" id="S5.SS0.SSS0.P0.SPx3.p3.m20.1.g1nest" class="ltx\_graphics ltx\_img\_square" width="12" height="14" style="width: 18px; height: unset; max-width: 100\%"></object>}\end{array}}_{\mathrm{R}}$, ${\begin{array}{c}\text{<object type="image/svg+xml" data="custom\_symbols/cross2.pdf2svg.svg" id="S5.SS0.SSS0.P0.SPx3.p3.m21.1.g1nest" class="ltx\_graphics ltx\_img\_square" width="12" height="14" style="width: 18px; height: unset; max-width: 100\%"></object>}\end{array}}_{\mathrm{A}}$ or ${\begin{array}{c}\text{<object type="image/svg+xml" data="custom\_symbols/cross2.pdf2svg.svg" id="S5.SS0.SSS0.P0.SPx3.p3.m22.1.g1nest" class="ltx\_graphics ltx\_img\_square" width="12" height="14" style="width: 18px; height: unset; max-width: 100\%"></object>}\end{array}}_{\mathrm{B}}$ in the round when the corresponding local condition holds, or ${\begin{array}{c}\text{<object type="image/svg+xml" data="custom\_symbols/cross2.pdf2svg.svg" id="S5.SS0.SSS0.P0.SPx3.p3.m23.1.g1nest" class="ltx\_graphics ltx\_img\_square" width="12" height="14" style="width: 18px; height: unset; max-width: 100\%"></object>}\end{array}}_{\mathrm{C}}$ in the round when either the local condition $C_{ℳ}^{𝕋,\mathrm{\ell }}$ holds, or some of the other three local conditions fails. Intuitively, ${\begin{array}{c}\text{<object type="image/svg+xml" data="custom\_symbols/cross2.pdf2svg.svg" id="S5.SS0.SSS0.P0.SPx3.p3.m25.1.g1nest" class="ltx\_graphics ltx\_img\_square" width="12" height="14" style="width: 18px; height: unset; max-width: 100\%"></object>}\end{array}}_{\mathrm{R}}$, ${\begin{array}{c}\text{<object type="image/svg+xml" data="custom\_symbols/cross2.pdf2svg.svg" id="S5.SS0.SSS0.P0.SPx3.p3.m26.1.g1nest" class="ltx\_graphics ltx\_img\_square" width="12" height="14" style="width: 18px; height: unset; max-width: 100\%"></object>}\end{array}}_{\mathrm{A}}$ or ${\begin{array}{c}\text{<object type="image/svg+xml" data="custom\_symbols/cross2.pdf2svg.svg" id="S5.SS0.SSS0.P0.SPx3.p3.m27.1.g1nest" class="ltx\_graphics ltx\_img\_square" width="12" height="14" style="width: 18px; height: unset; max-width: 100\%"></object>}\end{array}}_{\mathrm{B}}$ are prioritised over ${\begin{array}{c}\text{<object type="image/svg+xml" data="custom\_symbols/cross2.pdf2svg.svg" id="S5.SS0.SSS0.P0.SPx3.p3.m28.1.g1nest" class="ltx\_graphics ltx\_img\_square" width="12" height="14" style="width: 18px; height: unset; max-width: 100\%"></object>}\end{array}}_{\mathrm{C}}$: in order to win by declaring an error, $\mathrm{Monitor}$ must declare ${\begin{array}{c}\text{<object type="image/svg+xml" data="custom\_symbols/cross2.pdf2svg.svg" id="S5.SS0.SSS0.P0.SPx3.p3.m30.1.g1nest" class="ltx\_graphics ltx\_img\_square" width="12" height="14" style="width: 18px; height: unset; max-width: 100\%"></object>}\end{array}}_{\mathrm{R}}$, ${\begin{array}{c}\text{<object type="image/svg+xml" data="custom\_symbols/cross2.pdf2svg.svg" id="S5.SS0.SSS0.P0.SPx3.p3.m31.1.g1nest" class="ltx\_graphics ltx\_img\_square" width="12" height="14" style="width: 18px; height: unset; max-width: 100\%"></object>}\end{array}}_{\mathrm{A}}$ or ${\begin{array}{c}\text{<object type="image/svg+xml" data="custom\_symbols/cross2.pdf2svg.svg" id="S5.SS0.SSS0.P0.SPx3.p3.m32.1.g1nest" class="ltx\_graphics ltx\_img\_square" width="12" height="14" style="width: 18px; height: unset; max-width: 100\%"></object>}\end{array}}_{\mathrm{B}}$ if the corresponding local condition fails, and may only declare ${\begin{array}{c}\text{<object type="image/svg+xml" data="custom\_symbols/cross2.pdf2svg.svg" id="S5.SS0.SSS0.P0.SPx3.p3.m33.1.g1nest" class="ltx\_graphics ltx\_img\_square" width="12" height="14" style="width: 18px; height: unset; max-width: 100\%"></object>}\end{array}}_{\mathrm{C}}$ otherwise.

We prove the following lemma:

Due to a well-quasi-order on configurations and the lossy semantics, if $ℳ$ repeatedly reaches $s$ then $ℳ$ has a lasso run repeatedly reaching $s$ [34]: a run that is cyclic from some point on. The run is thus bounded by some $k\in \mathbb{N}$, and $\mathrm{Timer}$ has a winning controller that produces an encoding of this run of granularity at most $\delta =1/4\left(k+1\right)$. Indeed, with this granularity, $\mathrm{Timer}$ can encode all potential valuations by using $k$ “slots” in an interval of length $1/4$ for each of the segments.

Conversely, if $ℳ$ does not repeatedly reach $s$ then whenever $\mathrm{Timer}$ produces a correct run it necessarily visits $s$ finitely often. Then $\mathrm{Monitor}$ has a winning strategy that records all the history and keeps playing $\begin{array}{c}\text{<object type="image/svg+xml" data="custom\_symbols/check4.pdf2svg.svg" id="S5.SS0.SSS0.P0.SPx5.p2.m6.1.g1nest" class="ltx\_graphics ltx\_img\_square" width="13" height="14" style="width: 18px; height: unset; max-width: 100\%"></object>}\end{array}$ as long as $\mathrm{Timer}$ is not cheating, and is able to detect all kinds of errors produced by $\mathrm{Timer}$ in case $\mathrm{Timer}$ cheats. $◀$

In this case, we need a slight extension of ${\text{NTA}}_1$ to define winning conditions and controllers: NTA with 1 clock and very limited form of $\epsilon$-transitions that reset the clock every time it equals 1. Let $𝔽={\mathbb{Q}}_{\ge 0}\cap [0,1)$ denote the set of fractional parts. For any time value $t\in {ℝ}_{\ge 0}$, let $\mathrm{frac}(t)$ denote its fractional part, i.e., the unique value in $𝔽$ such that $t=n+\mathrm{frac}(t)$ for some $n\in \mathbb{N}$. If $\nu$ is a valuation, $\mathrm{frac}(\nu )$ denotes the valuation $\{x\mapsto \mathrm{frac}(\nu (x))\}$.

A 1-resetting ${\text{<em class="ltx\_emph ltx\_font\_smallcaps">NTA</em>}}_1$ (${\text{NTA}}_1^{\text{res}}$) is an ${\text{NTA}}_1$ as defined in Section 2 with only the following modification: $(\mathrm{\ell },\nu )\stackrel{\delta ,\tau }{\to }({\mathrm{\ell }}^{\prime },{\nu }^{\prime })$ (with $a\in \mathrm{\Sigma }$) if and only if $\delta =(\mathrm{\ell },a,g,Y,{\mathrm{\ell }}^{\prime })\in \mathrm{\Delta }$ is a transition of $𝒜$ such that $\mathrm{frac}(\nu +\tau )\vDash g$, and ${\nu }^{\prime }=\mathrm{frac}(\nu +\tau )[Y≔0]$. The 1-resetting ${\text{NTA}}_1$ can be simulated using ${\text{NTA}}_1$ with $\epsilon$-transitions: in every location $\mathrm{\ell }\in L$ add a self-loop $(\mathrm{\ell },\epsilon ,x=1,\{x\},\mathrm{\ell })$.

Intuitively speaking, $\mathrm{Timer}$ is tasked with simulating a run of $ℳ$, and $\mathrm{Monitor}$ can point out when they think that $\mathrm{Timer}$ made a mistake in the simulation. More specifically, $\mathrm{Timer}$ will play instructions of $ℳ$, and the time values will be used to encode the valuations of counters, as described below (the encoding is different from the one in the previous section). After each move by $\mathrm{Timer}$, $\mathrm{Monitor}$ can either say that the simulation is correct so far, or that $\mathrm{Timer}$ made a mistake in their last move. In the former case, if $\mathrm{Timer}$ actually made a mistake then $\mathrm{Timer}$ wins ($\mathrm{Monitor}$ must point out any mistake), and if there was no mistake then the game continues (if the game continues like this forever, $\mathrm{Monitor}$ wins). In the latter case, the game is essentially immediately over: either $\mathrm{Monitor}$ is right and $\mathrm{Timer}$ made a mistake, which will be winning for $\mathrm{Monitor}$, or $\mathrm{Monitor}$ is wrong and $\mathrm{Timer}$’s last move was correct, in which case $\mathrm{Timer}$ will be winning.

The way time is used to encode counter valuations is the following. The fractional part of a timestamp acts as an identifier which allows an increment to be later matched with a corresponding decrement. For instance, an increment at time 2.314 can be later matched with a decrement at time 7.314. With this, the valuation of a counter is simply the number of increments/fractional parts that have not been matched with a later decrement with the same fractional part. See Figure 2 for an illustration.

An obvious implementation of this idea would require, in the case where a fractional part is used for the first time ever in an incrementing instruction, checking that it is fresh using unrestricted “guessing” $\epsilon$-transition (i.e., guess the fractional part before the first instruction, then check it never appears until the very last position). To avoid this, we introduce a pool of fractional parts at the start of the run encoding, denoted by the symbol “$\mathrm{\square }$”. The idea is that $\mathrm{Timer}$ must include at the beginning a number of relevant fractional parts that will be used later in the run encoding. Then, we can eliminate time guessing by instead non-deterministically choosing a position in the pool, resetting the clock at that point and then every time it equals 1. If the last position in the word is the only position seen with the clock exactly at zero, then we know this fractional part was never used before.

We define a timed word encoding of runs of $ℳ$ in three parts. First, we capture the regular properties of their projection onto $\mathrm{T}$. Let ${\mathrm{proj}}_{\mathrm{T}}:{(\mathrm{T}\times \mathrm{M}\times {\mathbb{Q}}_{\ge 0})}^{\ast }\to {\mathrm{T}}^{\ast }$ be the natural projection. Define ${\mathrm{Reg}}_{ℳ}\subseteq {(\mathrm{T}\times \mathrm{M}\times {\mathbb{Q}}_{\ge 0})}^{\ast }$ as the set of all finite timed words $w$ such that ${\mathrm{proj}}_{\mathrm{T}}(w)={\mathrm{\square }}^k{I}_1{I}_2\mathrm{\cdots }{I}_n$, instruction $I_1$ starts from the initial location, and each $I_i$ is compatible with $I_{i+1}$ in the sense defined earlier.

It remains to state the role of timestamps, on positions with a symbol in $ℐ$, in maintaining the valuations of $ℳ$. Consider a finite timed word $w\in {(\mathrm{T}\times \mathrm{M}\times {\mathbb{Q}}_{\ge 0})}^{\ast }$. We say that a fractional part $f\in 𝔽$ is active for counter $c$ in $w$ if the last timed letter $(I,t)$ with $I\in {ℐ}^c$ and $\mathrm{frac}(t)=f$ increments $c$ ($I\in {ℐ}_{\mathrm{inc}}^c$) and appears after the last zero-test of $c$. Conversely, $f$ is inactive for $c$ in $w$ if since the last zero-test of $c$ there is no occurrence of $f$ with an instruction $I\in {ℐ}^c$ involving $c$ or if the last such occurrence is in ${ℐ}_{\mathrm{dec}}^c$. For any prefix $w$ of a run encoding, the corresponding valuation of counter $c$ is the number of distinct fractional parts that are active for $c$. Let $\mathrm{val}(w)$ denote this valuation.

Recall the form of runs of $ℳ$: $\rho =(s_0,{\nu }_0)\stackrel{I_1}{\to }(s_1,{\nu }_1)\stackrel{I_2}{\to }\mathrm{\cdots }$, as an alternating sequence of configurations and instructions, with ${\nu }_0=0^{𝒞}$. We inductively define $\rho (w)$, a finite alternating sequence of configurations and instructions associated with any $w\in {\mathrm{Reg}}_{ℳ}$:

Note that $\rho (w)$ need not be a run of $ℳ$ for two reasons. First, valuations need not be correlated with the instructions (e.g., a run may feature an incrementing instruction while the corresponding valuation remains unchanged or decreases). Second, a decrementing instruction may occur even when the valuation of the corresponding counter is zero. Conversely, if valuations are updated correctly and decrementing instructions occur only when the valuation is non-zero, then ${\mathrm{Reg}}_{ℳ}$ ensures that $\rho (w)$ is a valid run of $ℳ$. To enforce validity, we introduce rules that must be satisfied by the timestamp $t$ of every instruction $I$ occurring in $w$:

Rule 1:

If $I\in {ℐ}_{\mathrm{inc}}^c$, then the fractional part of $t$ must be inactive for $c$.

Rule 2:

If $I\in {ℐ}_{\mathrm{dec}}^c$, then the fractional part of $t$ must be active for $c$.

It is easy to see that following both rules guarantees maintaining the correct counter valuations. Moreover, it prevents one from adding a decrementing instruction when the counter valuation is zero, as there would be no active fractional part to pick. Note that there are no constraints on zero-test instructions, their timestamps are irrelevant.

For each of the two rules, we now define a language of finite timed words that requires that the rule is satisfied by the last letter, and another one that requires that the rule is broken. Let ${\mathrm{Err}}_{ℳ}^{\mathrm{R1}}$ be the language of finite timed words where the last letter is an increment instruction that breaks Rule 1. Moreover, let ${\mathrm{Ok}}_{ℳ}^{\mathrm{R1}}$ be the language of words where the last letter satisfies Rule 1 and the last fractional part is in the pool. Note that any timed word ending in either a decrementing or zero-test instruction is in ${\mathrm{Ok}}_{ℳ}^{\mathrm{R1}}$, and is not in ${\mathrm{Err}}_{ℳ}^{\mathrm{R1}}$. ${\mathrm{Err}}_{ℳ}^{\mathrm{R1}}$ is recognised by the 1-resetting reachability ${\text{NTA}}_1$ given in Figure 3, while ${\mathrm{Ok}}_{ℳ}^{\mathrm{R1}}$ is recognised by the 1-resetting reachability ${\text{NTA}}_1$ given in Figure 4.

The languages ${\mathrm{Err}}_{ℳ}^{\mathrm{R1}}$ and ${\mathrm{Ok}}_{ℳ}^{\mathrm{R1}}$ are readily seen to be disjoint. Note however that the languages are not complements. Indeed, a word that satisfies Rule 1 but whose last fractional part does not appear in the pool at the beginning belongs to neither language.

The definitions and automata for ${\mathrm{Err}}_{ℳ}^{\mathrm{R2}}$ and ${\mathrm{Ok}}_{ℳ}^{\mathrm{R2}}$ mirror those of ${\mathrm{Ok}}_{ℳ}^{\mathrm{R1}}$ and ${\mathrm{Err}}_{ℳ}^{\mathrm{R1}}$ respectively, with ${\mathrm{Err}}_{ℳ}^{\mathrm{R2}}$ being the language of words breaking Rule 2 where the last fractional part is in the pool, and ${\mathrm{Ok}}_{ℳ}^{\mathrm{R2}}$ being the language of words where the last letter satisfies Rule 2. Again, a word not ending in a decrement is automatically in ${\mathrm{Ok}}_{ℳ}^{\mathrm{R2}}$ and not in ${\mathrm{Err}}_{ℳ}^{\mathrm{R2}}$.

Let ${\mathrm{Err}}_{ℳ}={\mathrm{Reg}}_{ℳ}\cap \left({\mathrm{Err}}_{ℳ}^{\mathrm{R1}}\cup {\mathrm{Err}}_{ℳ}^{\mathrm{R2}}\right)$ and ${\mathrm{Ok}}_{ℳ}={\mathrm{Reg}}_{ℳ}\cap {\mathrm{Ok}}_{ℳ}^{\mathrm{R1}}\cap {\mathrm{Ok}}_{ℳ}^{\mathrm{R2}}$. We define $\mathrm{Timer}$’s winning condition as the following language of infinite timed words:

Intuitively, $\mathrm{Timer}$ wins if at any point $\mathrm{Monitor}$ makes a mistake in its claim by playing $\begin{array}{c}\text{<object type="image/svg+xml" data="custom\_symbols/cross2.pdf2svg.svg" id="S6.SS0.SSS0.P0.SPx4.p4.m6.1.g1nest" class="ltx\_graphics ltx\_img\_square" width="12" height="14" style="width: 18px; height: unset; max-width: 100\%"></object>}\end{array}$ when the sequence given by $\mathrm{Timer}$ is actually correct or playing $\begin{array}{c}\text{<object type="image/svg+xml" data="custom\_symbols/check4.pdf2svg.svg" id="S6.SS0.SSS0.P0.SPx4.p4.m8.1.g1nest" class="ltx\_graphics ltx\_img\_square" width="13" height="14" style="width: 18px; height: unset; max-width: 100\%"></object>}\end{array}$ when there is an error. However the play continues after this point, $\mathrm{Timer}$ will be winning. On the other hand, $\mathrm{Monitor}$ wins if either it plays $\begin{array}{c}\text{<object type="image/svg+xml" data="custom\_symbols/cross2.pdf2svg.svg" id="S6.SS0.SSS0.P0.SPx4.p4.m11.1.g1nest" class="ltx\_graphics ltx\_img\_square" width="12" height="14" style="width: 18px; height: unset; max-width: 100\%"></object>}\end{array}$ at a point in which the play is not in ${\mathrm{Ok}}_{ℳ}$, and then any continuation will be outside of $W_{ℳ}$, or if it plays $\begin{array}{c}\text{<object type="image/svg+xml" data="custom\_symbols/check4.pdf2svg.svg" id="S6.SS0.SSS0.P0.SPx4.p4.m14.1.g1nest" class="ltx\_graphics ltx\_img\_square" width="13" height="14" style="width: 18px; height: unset; max-width: 100\%"></object>}\end{array}$ forever while the play is never in ${\mathrm{Err}}_{ℳ}$. Note that the case where $\mathrm{Timer}$ plays outside of ${\mathrm{Reg}}_{ℳ}$ is covered both by not being in ${\mathrm{Ok}}_{ℳ}$, so $\mathrm{Monitor}$ can play $\begin{array}{c}\text{<object type="image/svg+xml" data="custom\_symbols/cross2.pdf2svg.svg" id="S6.SS0.SSS0.P0.SPx4.p4.m20.1.g1nest" class="ltx\_graphics ltx\_img\_square" width="12" height="14" style="width: 18px; height: unset; max-width: 100\%"></object>}\end{array}$ if this happens and win, or by not being in ${\mathrm{Err}}_{ℳ}$, so $\mathrm{Monitor}$ can play $\begin{array}{c}\text{<object type="image/svg+xml" data="custom\_symbols/check4.pdf2svg.svg" id="S6.SS0.SSS0.P0.SPx4.p4.m23.1.g1nest" class="ltx\_graphics ltx\_img\_square" width="13" height="14" style="width: 18px; height: unset; max-width: 100\%"></object>}\end{array}$ if this happens and win as well.

Both ${\mathrm{Err}}_{ℳ}$ and ${\mathrm{Ok}}_{ℳ}$ are recognisable by 1-resetting reachability ${\text{NTA}}_1$s. For ${\mathrm{Err}}_{ℳ}$ this follows from the closure of ${\text{reach-}\text{NTA}}_1^{\text{res}}$ under union of languages, and intersection with ${\mathrm{Reg}}_{ℳ}$ does not add clocks. As for ${\mathrm{Ok}}_{ℳ}$, although intersection typically adds up the numbers of clocks, we can branch based on the final letter to simulate either ${\mathrm{Ok}}_{ℳ}^{\mathrm{R1}}$ or ${\mathrm{Ok}}_{ℳ}^{\mathrm{R2}}$, requiring only one clock. $◀$

Before stating correctness of the reduction, let us give some intuition about the pool at the beginning of the play. It is in $\mathrm{Timer}$’s best interest to accurately list as many fractional parts that will be used later, but only finitely many. The finite part is obvious: if $\mathrm{Timer}$ only plays $\mathrm{\square }$ forever then $\mathrm{Monitor}$ just plays $\begin{array}{c}\text{<object type="image/svg+xml" data="custom\_symbols/check4.pdf2svg.svg" id="S6.SS0.SSS0.P0.SPx6.p1.m5.1.g1nest" class="ltx\_graphics ltx\_img\_square" width="13" height="14" style="width: 18px; height: unset; max-width: 100\%"></object>}\end{array}$ forever and wins, so $\mathrm{Timer}$ must start the real run encoding at some point. The incentive for $\mathrm{Timer}$ to play many fractional parts comes from its winning condition: it wins if $\mathrm{Monitor}$ makes a mistake. For example, if $\mathrm{Timer}$ plays an increment transition with some inactive fractional part $f$ and $\mathrm{Monitor}$ answers with $\begin{array}{c}\text{<object type="image/svg+xml" data="custom\_symbols/cross2.pdf2svg.svg" id="S6.SS0.SSS0.P0.SPx6.p1.m12.1.g1nest" class="ltx\_graphics ltx\_img\_square" width="12" height="14" style="width: 18px; height: unset; max-width: 100\%"></object>}\end{array}$, $\mathrm{Timer}$ wins iff the play is in ${\mathrm{Ok}}_{ℳ}^{\mathrm{R1}}$. But ${\mathrm{Ok}}_{ℳ}^{\mathrm{R1}}$ accepts only if the last fractional part occurs in the pool. So if $f$ is not in the pool, the play is not in ${\mathrm{Ok}}_{ℳ}$ (despite being a correct encoding of a run), and $\mathrm{Monitor}$ wins by playing $\begin{array}{c}\text{<object type="image/svg+xml" data="custom\_symbols/cross2.pdf2svg.svg" id="S6.SS0.SSS0.P0.SPx6.p1.m19.1.g1nest" class="ltx\_graphics ltx\_img\_square" width="12" height="14" style="width: 18px; height: unset; max-width: 100\%"></object>}\end{array}$. On the other hand, there is no possible disadvantage to adding more fractional parts to the pool, even some that will never be used later, and so this is $\mathrm{Timer}$’s incentive for filling the pool as much as possible.

1. 1.

   By induction on prefixes of $w$. The base case, for prefixes where $\mathrm{Timer}$ has only played $\mathrm{\square }$ letters so far, is trivial. Let $w^{\prime }$ be a prefix of $w$. Since ${\mathrm{Runs}}_{ℳ}$ is prefix-closed and $\rho (w^{\prime })$ is a prefix of $\rho (w)$, $\rho (w^{\prime })\in {\mathrm{Runs}}_{ℳ}$. Assume by induction hypothesis that all strict prefixes of $w^{\prime }$ are not in ${\mathrm{Err}}_{ℳ}$. Let $w^{\prime }=w^{\prime \prime }\cdot (I,m,t)$ with $I\in ℐ$, $m\in \mathrm{M}$, and let $f=\mathrm{frac}(t)\in 𝔽$. We look at the different cases for $I$ to show that $w^{\prime }\notin {\mathrm{Err}}_{ℳ}$.

   • $\mathrm{■}$

     Suppose $I\in {ℐ}_{\mathrm{inc}}^c$. We have $\rho (w^{\prime })\in {\mathrm{Runs}}_{ℳ}$, $\rho (w^{\prime \prime })\in {\mathrm{Runs}}_{ℳ}$, and $\rho (w^{\prime })=\rho (w^{\prime \prime })\stackrel{𝐼}{\to }(s,\mathrm{val}(w^{\prime }))$. Thus $\mathrm{val}(w^{\prime })=\mathrm{val}(w^{\prime \prime })[c++]$, and from this we have that $f$ is inactive for $c$ in $w^{\prime \prime }$. This does not mean that $w^{\prime }\in {\mathrm{Ok}}_{ℳ}^{\mathrm{R1}}$ as $f$ could be missing from the pool, but it does mean that $w^{\prime }\notin {\mathrm{Err}}_{ℳ}^{\mathrm{R1}}$ as ${\mathrm{Err}}_{ℳ}^{\mathrm{R1}}$ can only accept if the last fractional part is already active. Thus $w^{\prime }\notin {\mathrm{Err}}_{ℳ}$.

   • $\mathrm{■}$

     Suppose $I\in {ℐ}_{\mathrm{dec}}^c$. Since the run is correct, we have that $\mathrm{val}(w^{\prime \prime })(c)>0$ and $\mathrm{val}(w^{\prime })=\mathrm{val}(w^{\prime \prime })[c--]$, so $f$ must be active for $c$ in $w^{\prime \prime }$. Then $w^{\prime }\in {\mathrm{Ok}}_{ℳ}^{\mathrm{R2}}$ which implies $w^{\prime }\notin {\mathrm{Err}}_{ℳ}$.

   • $\mathrm{■}$

     If $I\in {ℐ}_{\mathrm{zt}}^c$ then $w^{\prime }$ is trivially accepted by ${\mathrm{Ok}}_{ℳ}^{\mathrm{R1}}$ and ${\mathrm{Ok}}_{ℳ}^{\mathrm{R2}}$ thus $w^{\prime }\notin {\mathrm{Err}}_{ℳ}$.

2. 2.

   If $\rho (w)\notin {\mathrm{Runs}}_{ℳ}$, there is some prefix $w^{\prime }=w^{\prime \prime }\cdot (I,m,t)$ of $w$ such that $\rho (w^{\prime })\notin {\mathrm{Runs}}_{ℳ}$ and $\rho (w^{\prime \prime })\in {\mathrm{Runs}}_{ℳ}$. This is because at least all prefixes of the form ${(\mathrm{\square },m,t)}^{\ast }$ are encoding the empty run, which belongs to ${\mathrm{Runs}}_{ℳ}$.

   We look at the different cases for $I$ to show that $w^{\prime }\notin {\mathrm{Ok}}_{ℳ}$. Again, we let $f=\mathrm{frac}(t)\in 𝔽$.

   • $\mathrm{■}$

     Suppose $I\in {ℐ}_{\mathrm{inc}}^c$. We have $\rho (w^{\prime })\notin {\mathrm{Runs}}_{ℳ}$, $\rho (w^{\prime \prime })\in {\mathrm{Runs}}_{ℳ}$, and $\rho (w^{\prime })=\rho (w^{\prime \prime })\stackrel{𝐼}{\to }(s,\mathrm{val}(w^{\prime }))$. This means that $\mathrm{val}(w^{\prime })$ is not the correct valuation, that is $\mathrm{val}(w^{\prime })\ne \mathrm{val}(w^{\prime \prime })[c++]$. From this, we deduce that $f$ is active for $c$ in $w^{\prime \prime }$, otherwise $\mathrm{val}(w^{\prime })$ would be correct. Therefore $w^{\prime }\in {\mathrm{Err}}_{ℳ}^{\mathrm{R1}}$, which implies $w^{\prime }\notin {\mathrm{Ok}}_{ℳ}$.

   • $\mathrm{■}$

     Suppose $I\in {ℐ}_{\mathrm{dec}}^c$. There are two possible reasons for $\rho (w^{\prime })$ not to be in ${\mathrm{Runs}}_{ℳ}$: either $\mathrm{val}(w^{\prime })$ is wrong, or $\mathrm{val}(w^{\prime \prime })(c)=0$. In the first case, we deduce similarly to the increment case that $f$ is inactive for $c$ in $w^{\prime \prime }$. In the second case, it means that there are no active fractional part for $c$ in $w^{\prime \prime }$, therefore $f$ can only be inactive also. In both cases, $f$ being inactive does not mean that $w^{\prime }\in Er{r}_2$, as $f$ might be missing from the pool. However, this still means that $w^{\prime }\notin {\mathrm{Ok}}_{ℳ}^{\mathrm{R2}}$ because ${\mathrm{Ok}}_{ℳ}^{\mathrm{R2}}$ only accepts if the last fractional part is active. Then we have that $w^{\prime }\notin {\mathrm{Ok}}_{ℳ}$.

   • $\mathrm{■}$

     If $I\in {ℐ}_{\mathrm{zt}}^c$ then we immediately get a contradiction because by definition $\mathrm{val}(w^{\prime })$ will be correct so $\rho (w^{\prime })$ must be in ${\mathrm{Runs}}_{ℳ}$.