1829 LABEL:LastPageApr. 09, 2021May 10, 2022 *This paper is an extended
version of the conference paper [CLP20a].

# Determinisability of register and timed automata*

Lorenzo Clemente 0000-0003-0578-9103  ,  Sławomir Lasota 0000-0001-8674-4470
and  Radosław Piórkowski 0000-0002-9643-182X  University of Warsaw, Poland
<EMAIL_ADDRESS><EMAIL_ADDRESS>https://sites.google.com/view/lorenzoclementehttps://www.mimuw.edu.pl/~sl,
https://www.mimuw.edu.pl/~rp

###### Abstract.

The deterministic membership problem for timed automata asks whether the timed
language given by a nondeterministic timed automaton can be recognised by a
deterministic timed automaton. An analogous problem can be stated in the
setting of register automata. We draw the complete decidability/complexity
landscape of the deterministic membership problem, in the setting of both
register and timed automata. For register automata, we prove that the
deterministic membership problem is decidable when the input automaton is a
nondeterministic one-register automaton (possibly with epsilon transitions)
and the number of registers of the output deterministic register automaton is
fixed. This is optimal: We show that in all the other cases the problem is
undecidable, i.e., when either (1) the input nondeterministic automaton has
two registers or more (even without epsilon transitions), or (2) it uses
guessing, or (3) the number of registers of the output deterministic automaton
is not fixed. The landscape for timed automata follows a similar pattern. We
show that the problem is decidable when the input automaton is a one-clock
nondeterministic timed automaton without epsilon transitions and the number of
clocks of the output deterministic timed automaton is fixed. Again, this is
optimal: We show that the problem in all the other cases is undecidable, i.e.,
when either (1) the input nondeterministic timed automaton has two clocks or
more, or (2) it uses epsilon transitions, or (3) the number of clocks of the
output deterministic automaton is not fixed.

###### Key words and phrases:

Timed automata, register automata, determinisation, deterministic membership
problem

L. Clemente was partially supported by the Polish NCN grant
2017/26/D/ST6/00201. S. Lasota was partially supported by the Polish NCN grant
2019/35/B/ST6/02322 and by the ERC grant LIPA, agreement no. 683080. R.
Piórkowski was partially supported by the Polish NCN grant
2017/27/B/ST6/02093.

##  1\. Introduction

###  1.1. Automata over infinite alphabets

##### Timed automata.

_Nondeterministic timed automata_ (nta) are one of the most widespread models
of real-time reactive systems. They are an extension of finite automata with
real-valued clocks which can be reset and compared by inequality constraints.
The nonemptiness problem for nta is decidable and, in fact, PSpace-complete,
as shown by Alur and Dill in their landmark 1994 paper [AD94]. This paved the
way for the automatic verification of timed systems, leading to mature tools
such as UPPAAL [BDL+06], UPPAAL Tiga (timed games) [CDF+05], and PRISM
(probabilistic timed automata) [KNP11]. The reachability problem is still a
very active research area these days [FJ15, HSW16, AGK18, GMS18, GMS19,
GHSW19], as are expressive generalisations thereof, such as the binary
reachability problem [CJ99, Dim02, KP05, FQSW20]. As a testimony to the
model’s importance, the authors of [AD94] received the 2016 Church Award
[chu16] for the invention of timed automata.

_Deterministic timed automata_ (dta) form a strict subclass of nta where the
successive configuration is uniquely determined from the current one and the
timed input symbol. The class of dta enjoys stronger properties than nta, such
as decidable universality/equivalence/inclusion problems, and closure under
complementation [AD94]. Moreover, the more restrictive nature of dta is needed
for several applications of timed automata, such as test generation [NS03],
fault diagnosis [BCD05], and learning [VdWW07, TALL19], winning conditions in
timed games [AM99, JT07, BHPR07], and in a notion of recognisability of timed
languages [MP04]. For these reasons, and for the more general quest of
understanding the nature of the expressive power of nondeterminism in timed
automata, many researchers have focused on defining determinisable classes of
timed automata, such as strongly non-Zeno nta [AMPS98], event-clock nta
[AFH99], and nta with integer-resets [SPKM08]. The classes above are not
exhaustive, in the sense that there are nta recognising deterministic timed
languages not falling into any of the classes above.

Another remarkable subclass of nta is obtained by requiring the presence of
just one clock (without epsilon transitions). The resulting class of
${\textsf{\sc nta}_{1}}$ is incomparable with dta: For instance, ${\textsf{\sc
nta}_{1}}$ are not closed under complement (unlike dta), and there are very
simple dta languages that are not recognisable by any ${\textsf{\sc
nta}_{1}}$. Nonetheless, ${\textsf{\sc nta}_{1}}$, like dta, have decidable
inclusion, equivalence, and universality problems [OW04, LW08], although the
complexity is non-primitive recursive [LW08, Corollary 4.2] (see also [OW07,
Theorem 7.2] for an analogous lower bound for the satisfiability problem of
metric temporal logic). Moreover, the nonemptiness problem for ${\textsf{\sc
nta}_{1}}$ is NLogSpace-complete (vs. PSpace-complete for unrestricted nta and
dta, already with two clocks [FJ15]), and the binary reachability relation of
${\textsf{\sc nta}_{1}}$ can be computed as a formula of existential linear
arithmetic of polynomial size, which is not the case in general [CHT19].

##### Register automata.

The theory of register automata shares many similarities with that of timed
automata. _Nondeterministic register automata_ (nra) have been introduced by
Kaminski and Francez around the same time as timed automata. They were defined
as an extension of finite automata with finitely many registers that can store
input values and be compared with equality and disequality constraints. The
authors have shown, amongst other things, that nonemptiness is decidable
[KF94, Theorem 1]. It was later realised that the problem is, in fact, PSpace-
complete [DL09, Theorems 4.3 and Theorem 5.1]. The class of nra recognisable
languages is not closed under complementation [KF94, Proposition 5]; moreover,
universality (and thus equivalence and inclusion) of nra is undecidable
[NSV04, Theorem 5.1] (already for nra with two registers [DL09, Theorem 5.4]).

One way to regain decidability is to consider _deterministic register
automata_ (dra), which are effectively closed under complement and thus have a
decidable inclusion (and thus universality and equivalence) problem111In fact,
even the inclusion problem $L(A)\subseteq L(B)$ with $A$ an nra and $B$ a dra
is decidable.. dra also provide the foundations of learning algorithms for
data languages [MSS+17]. A recent result completing the theory of register
automata has shown that a data language is dra recognisable if, and only if,
both this language and its complement are nra recognisable [KLT21].

As in the case of timed automata, it has been observed that restricting the
number of registers results in algorithmic gains. Already in the seminal work
of Kaminski and Francez, it has been proved that the inclusion problem
$L(A)\subseteq L(B)$ is decidable when $A$ is an nra and $B$ is an nra with
one register [KF94, Appendix A], albeit the complexity is non-primitive
recursive in this case [DL09, Theorem 5.2].

###  1.2. The deterministic membership problem

##### Timed automata.

The _dta membership problem_ asks, given an nta, whether there exists a dta
recognising the same language. There are two natural variants of this problem,
which are obtained by restricting the resources available to the sought dta .
Let $k\in\mathbb{N}$ be a bound on the number of clocks, and let
$m\in\mathbb{N}$ be a bound on the maximal absolute value of numerical
constants. The _${\textsf{\sc dta}_{k}}$_ and _${\textsf{\sc dta}_{k,m}}$
membership problems_ are the restriction of the problem above where the dta is
required to have at most $k$ clocks, resp., at most $k$ clocks and the
absolute value of maximal constant bounded by $m$. Notice that we do not bound
the number of control locations of the dta, which makes the problem non-
trivial. (Indeed, there are finitely many dta with a bounded number of clocks,
control locations, and maximal constant.)

Since untimed regular languages are deterministic, the ${\textsf{\sc
dta}_{k}}$ membership problem can be seen as a quantitative generalisation of
the regularity problem. For instance, the ${\textsf{\sc dta}_{0}}$ membership
problem is precisely the regularity problem since a timed automaton with no
clocks is the same as a finite automaton. We remark that the regularity
problem is usually undecidable for nondeterministic models of computation
generalising finite automata, e.g., context-free grammars/pushdown automata
[Sha08, Theorem 6.6.6], labelled Petri nets under reachability semantics
[VVN81], Parikh automata [CFM11], etc. One way to obtain decidability is to
either restrict the input model to be deterministic (e.g., [Val75, VVN81,
BLS06]), or to consider more refined notions of equivalence, such as
bisimulation (e.g., [GP20]).

This negative situation is generally confirmed for timed automata. For every
number of clocks $k\in\mathbb{N}$ and maximal constant $m$, the dta,
${\textsf{\sc dta}_{k}}$, and ${\textsf{\sc dta}_{k,m}}$ membership problems
are known to be undecidable when the input nta has $\geq 2$ clocks, and for
1-clock nta with epsilon transitions [Fin06, Tri06]. To the best of our
knowledge, the deterministic membership problem was not studied before when
the input automaton is ${\textsf{\sc nta}_{1}}$ without epsilon transitions.

##### Register automata.

The situation for register automata is similar to, and simpler than, timed
automata. The _${\textsf{\sc dra}_{k}}$ membership problem_ asks, given an
nra, whether there exists a dra with $k$ registers recognising the same
language, and the _dra membership problem_ is the same problem with no apriori
bound on the number of registers of the deterministic acceptor. Deterministic
membership problems for register automata do not seem to have been considered
before in the literature.

###  1.3. Contributions

We complete the study of the decidability border for the deterministic
membership problem initiated for timed automata in [Fin06, Tri06], and we
extend these results to register automata.

##### Upper bounds.

Our main result is the following.

######  Theorem 1.

The ${\textsf{\sc dta}_{k}}$ and ${\textsf{\sc dta}_{k,m}}$ membership
problems are decidable for ${\textsf{\sc nta}_{1}}$ languages.

Our decidability result contrasts starkly with the abundance of undecidability
results for the regularity problem. We establish decidability by showing that
if a ${\textsf{\sc nta}_{1,m}}$ recognises a ${\textsf{\sc dta}_{k}}$
language, then, in fact, it recognises a ${\textsf{\sc dta}_{k,m}}$ language
and, moreover, there is a computable bound on the number of control locations
of the deterministic acceptor (c.f. Lemma 21). This provides a decision
procedure since there are finitely many different dta once the number of
clocks, the maximal constant, and the number of control locations are fixed.

In our technical analysis, we find it convenient to introduce the so-called
_always resetting_ subclass of ${\textsf{\sc nta}_{k}}$. These automata are
required to reset at least one clock at every transition and are thus of
expressive power intermediate between ${\textsf{\sc nta}_{k-1}}$ and
${\textsf{\sc nta}_{k}}$. Always resetting ${\textsf{\sc nta}_{2}}$ are
strictly more expressive than ${\textsf{\sc nta}_{1}}$: For instance, the
language of timed words of the form $(a,t_{0})(a,t_{1})(a,t_{2})$ s.t.
$t_{2}-t_{0}>2$ and $t_{2}-t_{1}<1$ can be recognised by an always resetting
${\textsf{\sc nta}_{2}}$ but by no ${\textsf{\sc nta}_{1}}$. Despite their
increased expressive power, always resetting ${\textsf{\sc nta}_{2}}$ still
have a decidable universality problem (the well-quasi order approach of [OW04]
goes through), which is not the case for ${\textsf{\sc nta}_{2}}$. Thanks to
this restricted form, we are able to provide in Lemma 21 an elegant
characterisation of those ${\textsf{\sc nta}_{1}}$ languages which are
recognised by an always resetting ${\textsf{\sc dta}_{k}}$.

We prove a result analogous to Theorem 1 in the setting of register automata.

######  Theorem 2.

The ${\textsf{\sc dra}_{k}}$ membership problem is decidable for ${\textsf{\sc
nra}_{1}}$ languages.

Thanks to the effective elimination of $\varepsilon$-transition rules from
${\textsf{\sc nra}_{1}}$ (c.f. Lemma 8), the decidability result above also
holds for data languages presented as ${\textsf{\sc nra}_{1}}$ with
$\varepsilon$-transition rules.

##### Lower bounds.

We complement the decidability results above by showing that the deterministic
membership problem becomes undecidable if we do not restrict the number of
clocks/registers of the deterministic acceptor.

######  Theorem 3.

The dta and ${\textsf{\sc dta}_{\textnormal{\\_},m}}$ ($m>0$) membership
problems are undecidable for ${\textsf{\sc nta}_{1}}$ without epsilon
transitions.

Theorem 3 improves on an analogous result from [Fin06, Theorem 1] for
${\textsf{\sc nta}_{2}}$. We obtain a similar undecidability result in the
setting of register automata:

######  Theorem 4.

The dra membership problem is undecidable for ${\textsf{\sc nra}_{1}}$.

The following lower bounds further refine the analysis from [Fin06] in the
case of a fixed number of clocks of a deterministic acceptor.

######  Theorem 5.

For every fixed $k,m\in\mathbb{N}$, the ${\textsf{\sc dta}_{k}}$ and
${\textsf{\sc dta}_{k,m}}$ membership problems are:

  * •

undecidable for ${\textsf{\sc nta}_{2}}$,

  * •

undecidable for ${\textsf{\sc nta}_{1}^{\varepsilon}}$ (with epsilon
transitions),

  * •

HyperAckermann-hard for ${\textsf{\sc nta}_{1}}$.

A similar landscape holds for register automata, where the deterministic
membership problem for a fixed number of registers of the deterministic
acceptor remains undecidable when given in input either a ${\textsf{\sc
nra}_{2}}$ or a ${\textsf{\sc nra}_{1}}$ with guessing. (Register automata
with guessing are a more expressive family of automata where a register can be
updated with a data value not necessarily coming from the input word, i.e., it
can be _guessed_. We omit a formal definition since we will not need to
explicitly manipulate such automata in this paper.) In the decidable case of a
${\textsf{\sc nra}_{1}}$ input, the problem is nonetheless not primitive
recursive.

######  Theorem 6.

Fix a $k\geq 0$. The ${\textsf{\sc dra}_{k}}$ membership problem is:

  1. (1)

undecidable for ${\textsf{\sc nra}_{2}}$,

  2. (2)

undecidable for ${\textsf{\sc nra}_{1}^{\mathrm{g}}}$ (${\textsf{\sc
nra}_{1}}$ with guessing), and

  3. (3)

not primitive recursive (Ackermann-hard) for ${\textsf{\sc nra}_{1}}$.

##### Related research.

Many works have addressed the construction of a dta equivalent to a given nta
(see [BSJK15] and references therein). However, since the general problem is
undecidable, one has to either sacrifice termination, or consider
deterministic under/over-approximations. In a related line of work, we have
shown that the _deterministic separability problem_ is decidable for the full
class of nta, when the number of clocks of the separator is given in the input
[CLP20b]. This contrasts with the undecidability of the corresponding
membership problem. The deterministic separability problem for register
automata has not been studied in the literature. Decidability of the
deterministic separability problem when the number of clocks/registers of the
separator is not provided remains a challenging open problem.

##  2\. Automorphisms, orbits, and invariance

This section contains preliminary definitions needed both for register and
timed automata.

##### Atoms.

Let $\mathbb{A}$ be a structure (whose elements are called _atoms_) providing
a data domain on which register and timed automata operate. In the case of
register automata, we will primarily be concerned with _equality atoms_
$(\mathbb{A},=)$, where $\mathbb{A}$ is a countable set, and the signature
contains the equality symbol only. However—as we discuss at the end of Section
7—our positive results generalise to other atoms, for instance to densely
ordered atoms $({\mathbb{R}},\leq)$, where ${\mathbb{R}}$ is the set of real
numbers with the natural order “$\leq$”. In the case of timed automata, we
will consider _timed atoms_ $({\mathbb{R}},\leq,{+1})$, which extend densely
ordered atoms with the increment function “${+1}$”.

##### Automorphisms.

Let $S\subseteq\mathbb{A}$ be a (possibly empty) finite set of atoms. An _$S$
-automorphism_ is a bijection $\pi:\mathbb{A}\to\mathbb{A}$ that is the
identity on $S$, i.e., $\pi(a)=a$ for every $a\in S$, and which preserves the
atom structure. The latter condition is trivially satisfied for equality
atoms. In the case of densely ordered atoms, it also demands monotonicity:
$a\leq b$ implies $\pi(a)\leq\pi(b)$. For instance, a non-trivial automorphism
of densely ordered atoms is $\pi(a)=2\cdot a$, which is also a
$\\{0\\}$-automorphism since $\pi(0)=0$. In the case of timed atoms
automorphisms need to additionally preserve integer differences:
$\pi(a+1)=\pi(a)+1$, for every $a,b\in{\mathbb{R}}$. For instance, if
$\pi(3.4)=4.5$, then the last condition necessarily implies $\pi(5.4)=6.5$ and
$\pi(-3.6)=-2.5$. When $S=\emptyset$, we just say that $\pi$ is an
automorphism. Let $\textrm{Aut}_{S}(\mathbb{A})$ denote the set of all
$S$-automorphisms of $\mathbb{A}$, and let
$\textrm{Aut}(\mathbb{A})=\textrm{Aut}_{\emptyset}(\mathbb{A})$.

Informally speaking, by _sets with atoms_ we mean sets whose elements are
either sets or atoms (for a formal definition of the hierarchy thereof, we
refer to [Boj]). If $X$ is a set with atoms, then $\pi(X)$ is the set with
atoms which is obtained by replacing every atom $a\in\mathbb{A}$ occurring in
$X$ by $\pi(a)\in\mathbb{A}$. We present some commonly occurring concrete
examples, relying on standard set-theoretic encodings of tuples, functions,
etc. Let $\Sigma$ be a finite alphabet. A _data word_ is a finite sequence

$\displaystyle
w=(\sigma_{0},a_{0})\cdots(\sigma_{n},a_{n})\in(\Sigma\times\mathbb{A})^{*}$
(1)

of pairs $(\sigma_{i},a_{i})$ consisting of an input symbol
$\sigma_{i}\in\Sigma$ and an atom $a_{i}\in\mathbb{A}$. An automorphism $\pi$
acts on a data word $w$ as above point-wise:
$\pi(w)=(\sigma_{0},\pi(a_{0}))\cdots(\sigma_{n},\pi(a_{n}))$.

Let $\mathtt{X}$ be a finite set of register names and let
$\mathbb{A}_{\bot}=\mathbb{A}\cup\\{\bot\\}$, where $\bot\not\in\mathbb{A}$
represents an undefined value. A _register valuation_ is a mapping
$\mu:\mathbb{A}_{\bot}^{\mathtt{X}}$ assigning an atom (or $\bot$) $\mu(x)$ to
every register $x\in\mathtt{X}$. An automorphism $\pi$ acts on a register
valuation $\mu$ as $\pi(\mu)(x)=\pi(\mu(x))$ for every $x\in\mathtt{X}$, i.e.,
$\pi(\mu)=\pi\circ\mu$, where we assume that $\pi(\bot)=\bot$.

More generally, if $X$ is a set with atoms, then $\pi$ acts on $X$ pointwise
as $\pi(X)=\\{\pi(x)\;|\;x\in X\\}$.

##### Orbits and invariance.

A set with atoms $X$ is _$S$ -invariant_ if $\pi(X)=X$ for every
$S$-automorphism $\pi\in\textrm{Aut}_{S}(\mathbb{A})$. Notice that $\pi$ does
not need to be the identity on $X$ for $X$ to be $S$-invariant. A set $X$ is
_invariant_ 222The term _equivariant_ is also often used in the literature
instead of invariant. Also, in the case of an $S$-invariant set $X$, one can
also find the term _$S$ -supported_, and call $S$ a _support_ of $X$; see e.g.
[Boj, BKL14]. if it is $S$-invariant with $S=\emptyset$. The _$S$ -orbit_ of
an element $x\in X$ (which can be an arbitrary object on which the action of
automorphisms is defined) is the set

$\text{\sc orbit}_{S}(x)=\\{\pi(x)\in
X\;|\;\pi\in\textrm{Aut}_{S}(\mathbb{A})\\}$

of all elements $\pi(x)$ which can be obtained by applying some
$S$-automorphism $\pi$ to $x$. The _orbit_ of $x$ is just its $S$-orbit with
$S=\emptyset$, written $\text{\sc orbit}(x)$. Clearly $x,y\in X$ have the same
$S$-orbit $\text{\sc orbit}_{S}(x)=\text{\sc orbit}_{S}(y)$ if, and only if,
$\pi(x)=y$ for some $\pi\in\textrm{Aut}_{S}(\mathbb{A})$.

The _$S$ -orbit closure_ of a set $X$ (or just _$S$ -closure_) is the union of
the $S$-orbits of its elements:

$\textrm{Cl}_{S}(X)=\bigcup_{x\in X}\text{\sc orbit}_{S}(x).$

In particular, the $S$-orbit of $x$ is the $S$-closure of the singleton set
$\\{x\\}$: $\text{\sc orbit}_{S}(x)=\textrm{Cl}_{S}(\\{x\\})$. The
$\emptyset$-closure $\textrm{Cl}(X)$ we briefly call the _closure_ of $X$. The
following fact characterises invariance in term of closures.

######  Fact 7.

A set $X$ is $S$-invariant if, and only if, $\textrm{Cl}_{S}(X)=X$.

######  Proof 2.1.

The “only if” direction follows the definition of $S$-invariance. For the “if”
direction, observe that $\textrm{Cl}_{S}(X)=X$ implies $\pi(X)\subseteq X$.
The opposite inclusion stems from $S$-automorphisms’ closure under inverse:
$\pi^{-1}(X)\subseteq X$, hence $X\subseteq\pi(X)$.

##  3\. Register automata

In this section, we define register automata over equality atoms
$(\mathbb{A},=)$. However, all the definitions below can naturally be
generalised to any atoms satisfying some mild assumptions, as explained later
in Section 4.2.

##### Constraints.

A _constraint_ is a quantifier-free formula $\varphi$ generated by the grammar

$\displaystyle\varphi,\psi\ ::\equiv\ \mathbf{true}\ |\ \mathbf{false}\ |\
\mathtt{x}=\mathtt{y}\ |\ \mathtt{x}=\bot\ |\ \neg\varphi\ |\
\varphi\land\psi\ |\ \varphi\lor\psi,$ (2)

where $\mathtt{x},\mathtt{y}$ are variables and $\bot$ is a special constant
denoting an undefined data value. A _valuation_ is a function
$\mu\in\mathbb{A}_{\bot}^{\mathtt{X}}$ assigning a data value (or $\bot$)
$\mu(\mathtt{x})$ to every variable $\mathtt{x}\in\mathtt{X}$. The
satisfaction relation $\mu\models\varphi$ holds whenever the valuation $\mu$
satisfies the formula $\varphi$, and it is defined in the standard way. The
_semantics_ of a constraint $\varphi(\mathtt{x}_{1},\dots,\mathtt{x}_{n})$
with $n$ free variables $\mathtt{X}=\\{\mathtt{x}_{1},\dots,\mathtt{x}_{n}\\}$
is the set of valuations satisfying it:
$\llbracket\varphi\rrbracket=\\{\mu\in\mathbb{A}_{\bot}^{\mathtt{X}}\;|\;\mu\models\varphi\\}$.
Using [Boj, Lemma 7.5] we easily deduce: Subsets of
$\mathbb{A}_{\bot}^{\mathtt{X}}$ definable by constraints are exactly the
invariant subsets of $\mathbb{A}_{\bot}^{\mathtt{X}}$.

##### Register automata.

Let $\Sigma$ be a finite alphabet, and let
$\Sigma_{\varepsilon}=\Sigma\cup\\{\varepsilon\\}$ be $\Sigma$ with the
addition of the empty word $\varepsilon$. A (nondeterministic) _register
automaton_ (nra) is a tuple
$A=(\mathtt{X},\Sigma,\mathtt{L},\mathtt{L}_{I},\mathtt{L}_{F},\Delta)$ where
$\mathtt{X}=\\{\mathtt{x}_{1},\dots,\mathtt{x}_{k}\\}$ is a finite set of
register names, $\Sigma$ is a finite alphabet, $\mathtt{L}$ is a finite set of
_control locations_ , of which we distinguish those which are _initial_
$\mathtt{L}_{I}\subseteq\mathtt{L}$, resp., _final_
$\mathtt{L}_{F}\subseteq\mathtt{L}$, and $\Delta$ is a set of _transition
rules_. We have two kinds of transition rules. A _non-
$\varepsilon$-transition rule_ is of the form

$\displaystyle(p,\sigma,\varphi,\mathtt{Y},q)\in\Delta$ (3)

and it means that from control location $p\in\mathtt{L}$ we can go to
$q\in\mathtt{L}$ by reading input symbol $\sigma\in\Sigma$, provided that the
transition constraint
$\varphi(\mathtt{x}_{1},\dots,\mathtt{x}_{k},\mathtt{y})$ holds between the
current registers $\mathtt{x}_{1},\dots,\mathtt{x}_{k}$ and the input data
value $\mathtt{y}$ being currently read; finally, all registers in
$\mathtt{Y}\subseteq\mathtt{X}$ are updated to store the input data value
$\mathtt{y}$. An _$\varepsilon$ -transition rule_ is of the form
$(p,\varepsilon,\varphi,q)\in\Delta$ and it means that from control location
$p\in\mathtt{L}$ we can go to $q\in\mathtt{L}$, but no input is read, provided
that the transition constraint $\varphi(\mathtt{x}_{1},\dots,\mathtt{x}_{k})$
holds between the current registers $\mathtt{x}_{1},\dots,\mathtt{x}_{k}$.

Formally, the semantics of a register automaton $A$ as above is provided in
terms of an infinite transition system $\llbracket
A\rrbracket=(C,C_{I},C_{F},\to)$, where
$C=\mathtt{L}\times\mathbb{A}_{\bot}^{\mathtt{X}}$ is the set of
_configurations_ , which are pairs $(p,\mu)$ consisting of a control location
$p\in\mathtt{L}$ and a register valuation
$\mu\in\mathbb{A}_{\bot}^{\mathtt{X}}$. Amongst them,
$C_{I}=\mathtt{L}_{I}\times\\{\lambda\mathtt{x}\cdot\bot\\}\subseteq C$ is the
set of _initial configurations_ , i.e., configurations of the form $(p,\mu)$
with $p\in\mathtt{L}_{I}$ and $\mu(\mathtt{x})=\bot$ for all registers
$\mathtt{x}$, and $C_{F}=\mathtt{L}_{F}\times\mathbb{A}_{\bot}^{\mathtt{X}}$
is the set of _final configurations_ , i.e., configurations of the form
$(p,\mu)$ with $p\in\mathtt{L}_{F}$ (without any further restriction on
$\mu$). The set of transitions “$\to$” is determined as follows. For a
valuation $\mu\in\mathbb{A}_{\bot}^{\mathtt{X}}$, a set of registers
$\mathtt{Y}\subseteq\mathtt{X}$, and an atom333It suffices to consider
non-$\bot$ values $a\neq\bot$ since we never need to reset a register to the
undefined value $\bot$. $a\in\mathbb{A}$, let $\mu[\mathtt{Y}\mapsto a]$ be
the valuation which is $a$ on $\mathtt{Y}$ and agrees with $\mu$ on
$\mathtt{X}\setminus\mathtt{Y}$. Every non-$\varepsilon$-transition rule (3)
induces a transition between configurations

$\displaystyle(p,\mu)\xrightarrow{\sigma,a}(q,\mu[\mathtt{Y}\mapsto a])$

labelled by $(\sigma,a)\in\Sigma\times\mathbb{A}$, provided that the current
valuation $\mu$ satisfies the constraint $\varphi$ when variable $\mathtt{y}$
holds the input atom $a$, i.e., $\mu[\mathtt{y}\mapsto
a]\models\varphi(\mathtt{x}_{1},\dots,\mathtt{x}_{k},\mathtt{y})$. Similarly,
an $\varepsilon$-transition rule $(p,\varepsilon,\varphi,q)\in\Delta$ induces
an $\varepsilon$-labelled transition $(p,\mu)\xrightarrow{\varepsilon}(q,\mu)$
whenever $\mu\models\varphi(\mathtt{x}_{1},\dots,\mathtt{x}_{k})$. Finally, in
order to deal with $\varepsilon$-transitions, we stipulate that whenever we
have transitions $(p,\mu)\xrightarrow{b}\\_\xrightarrow{\varepsilon}(q,\nu)$,
$(p,\mu)\xrightarrow{\varepsilon}\\_\xrightarrow{b}(q,\nu)$, or
$(p,\mu)\xrightarrow{\varepsilon}\\_\xrightarrow{b}\\_\xrightarrow{\varepsilon}(q,\nu)$
with $b\in(\Sigma\times\mathbb{A})\cup\\{\varepsilon\\}$, then we also have
the transition $(p,\mu)\xrightarrow{b}(q,\nu)$. A _run_ of $A$ _over_ a data
word $w$ as in (1) _starting_ in configuration $(p,\mu)$ and _ending_ in
configuration $(q,\nu)$ is a labelled path $\rho$ in $\llbracket A\rrbracket$
of the form

$\displaystyle\rho=(p,\mu)\xrightarrow{\sigma_{0},a_{0}}(p_{0},\mu_{0})\xrightarrow{\sigma_{1},a_{1}}\cdots\xrightarrow{\sigma_{n},a_{n}}(q,\nu).$
(4)

The run $\rho$ is accepting if its ending configuration is accepting. The
language _recognised_ by configuration $(p,\mu)$ is the set of data words
labelling accepting runs:

$\displaystyle L(p,\mu)=\\{w\in(\Sigma\times\mathbb{A})^{*}\;|\;\llbracket
A\rrbracket\text{ has an accepting run over }w\text{ starting in }(p,\mu)\\}.$

The language recognised by the automaton $A$ is the union of the languages
recognised by its initial configurations, $L(A)=\bigcup_{c\in C_{I}}L(c)$. A
configuration is _reachable_ if it is the ending configuration in a run
starting in an initial configuration.

######  Remark 8.

Register automata, as defined above, are _without guessing_ , i.e. an
automaton can only store in a register an atom appearing in the input.

It turns out that nra with $\varepsilon$-transition rules are as expressive as
nra without $\varepsilon$-transition rules.

[Excercise 2 in [Boj]] For every $k\in\mathbb{N}$ and ${\textsf{\sc nra}_{k}}$
one can effectively build an ${\textsf{\sc nra}_{k}}$ without
$\varepsilon$-transition rules recognising the same language.

For this reason, from this point on, we deal exclusively with nra without
$\varepsilon$-transition rules, and we tacitly assume that an nra does not
contain $\varepsilon$-transition rules.

##### Deterministic register automata.

A register automaton $A$ is _deterministic_ (dra) if it has precisely one
initial location $\mathtt{L}_{I}=\\{p_{I}\\}$ and, for every two rules
$(p,\sigma,\varphi,\mathtt{Y},q)$ and
$(p,\sigma,\varphi^{\prime},\mathtt{Y}^{\prime},q^{\prime})$ starting in the
same location $p$, over the same input symbol $\sigma$ and with jointly
satisfiable guards
$\left\llbracket\varphi\land\varphi^{\prime}\right\rrbracket\neq\emptyset$, we
necessarily have $\mathtt{Y}=\mathtt{Y}^{\prime}$ and $q=q^{\prime}$. Hence
$A$ has at most one run over every data word $w$. A dra can be easily
transformed into a _total_ one, i.e., one where for every location
$p\in\mathtt{L}$ and input symbol $\sigma\in\Sigma$, the sets defined by the
constraints
$\\{\left\llbracket\varphi\right\rrbracket\;|\;\exists\mathtt{Y},q\cdot
p\xrightarrow{\sigma,\varphi,\mathtt{Y}}q\\}$ are a partition of all
valuations $\mathbb{A}_{\bot}^{\mathtt{X}\cup\\{\mathtt{y}\\}}$. Thus, a total
dra has exactly one run over every timed word $w$.

There are other syntactical constraints, more or less restrictive, which would
guarantee uniqueness of runs. Our choice is motivated by the fact that every
nra which has unique runs can be transformed into an equivalent dra, albeit
this may cause an exponential increase in the number of control locations.
Nonetheless, since we deal with computational problems which are either
undecidable or non-primitive recursive, this shall not be a concern in the
rest of the paper.

We write ${\textsf{\sc nra}_{k}}$, resp. ${\textsf{\sc dra}_{k}}$, for the
class of $k$-register nra, resp. dra, and we say that a data language is an
nra language, dra language, ${\textsf{\sc dra}_{k}}$ language, etc., if it is
recognised by a register automaton of the respective type.

Let $\Sigma=\\{\sigma\\}$ be a unary alphabet. As an example of a language $L$
recognised by an ${\textsf{\sc nra}_{1}}$, but not by any dra, consider the
set of data words where the last atom reappears earlier, i.e., words of the
form: $(\sigma,a_{1})\cdots(\sigma,a_{n})$ where $a_{i}=a_{n}$ for some $1\leq
i<n$. The language $L$ is recognised by the ${\textsf{\sc nra}_{1}}$
$A=(\mathtt{X},\Sigma,\mathtt{L},\mathtt{L}_{I},\mathtt{L}_{F},\Delta)$ with
one register $\mathtt{X}=\\{\mathtt{x}\\}$ and three locations
$\mathtt{L}=\\{p,q,r\\}$, of which $\mathtt{L}_{I}=\\{p\\}$ is initial and
$\mathtt{L}_{F}=\\{r\\}$ is final, and transition rules

$\displaystyle(p,\sigma,\mathbf{true},\emptyset,p)\qquad(p,\sigma,\mathbf{true},\\{\mathtt{x}\\},q)\qquad(q,\sigma,\mathtt{x}\neq\mathtt{y},\emptyset,q)\qquad(q,\sigma,\mathtt{x}=\mathtt{y},\emptyset,r).$

Intuitively, the automaton waits in $p$ until it guesses that the next input
$a_{i}$ will be appearing at the end of the word as well, at which point it
moves to $q$ by storing $a_{i}$ in the register. From $q$, the automaton can
accept by going to $r$ exactly when the atom stored in the register reappears
in the input. The language $L$ is not recognised by any dra since,
intuitively, any deterministic acceptor needs to store unboundedly many
different atoms $a_{i}$.

##### One-register automata.

Nondeterministic register automata with just one register enjoy stronger
algorithmic properties than the full class of nondeterministic register
automata. It was already observed in Kaminski and Francez’s seminal paper that
the inclusion problem becomes decidable444A _window_ in the terminology of
[KF94] corresponds to a register in this paper’s terminology. [KF94, Appendix
A] shows that the inclusion problem $L(A)\subseteq L(B)$ is decidable when $B$
is a two-window automaton. Due to the semantics of window reassignment of
[KF94], two-window automata are of intermediate expressive power between one-
register automata and two-register automata..

######  Theorem 9 (c.f. [KF94, Appendix A]).

For $A\in\mbox{\sc nra}$ and $B\in{\textsf{\sc nra}_{1}}$ the language
inclusion problem $L(A)\subseteq L(B)$ is decidable.

We immediately obtain the following corollary, which we will use in Section 4.

######  Corollary 10.

For $A\in\mbox{\sc dra}$ and $B\in{\textsf{\sc nra}_{1}}$ the language
equality problem $L(A)=L(B)$ is decidable.

######  Proof 3.1.

The inclusion $L(A)\subseteq L(B)$ can be checked as a special instance of
Theorem 9. The reverse inclusion $L(B)\subseteq L(A)$ reduces to checking
emptiness of a product construction of $B$ with the complement of $A$.

##### Invariance of register automata.

The following lemma expresses the fundamental invariance properties of
register automata. Given a valuation $\mu$ of registers $\mathtt{X}$, by
$\mu(\mathtt{X})\subseteq\mathbb{A}$ we mean the set of atoms stored in
registers: $\mu(\mathtt{X})=\\{\mu(\mathtt{x})\;|\;\mathtt{x}\in\mathtt{X},\
\mu(\mathtt{x})\in\mathbb{A}\\}$. Automorphisms act on configurations by
preserving the control location: $\pi(p,\mu)=(p,\pi(\mu))=(p,\pi\circ\mu)$.

######  Lemma 11 (Invariance of nra).

  1. (1)

The transition system $\llbracket A\rrbracket$ is invariant: If
$c\xrightarrow{\sigma,a}d$ in $\llbracket A\rrbracket$ and $\pi$ is an
automorphism, then $\pi(c)\xrightarrow{\sigma,\pi(a)}\pi(d)$ in $\llbracket
A\rrbracket$.

  2. (2)

The function $L(\\_)$ mapping a configuration $c$ to the language $L(c)$ it
recognises from $c$ is invariant: For all automorphisms $\pi$,
$L(\pi(c))=\pi(L(c))$.

  3. (3)

The language $L(p,\mu)$ recognised from a configuration $(p,\mu)$ is
$\mu(\mathtt{X})$-invariant: For all $\mu(\mathtt{X})$-automorphims $\pi$,
$\pi(L(p,\mu))=L(p,\mu)$.

We refrain from proving Lemma 11, since proofs of analogous invariance
properties, in the more involved setting of timed automata, are provided later
(Facts 15–17 in Section 6). For the proof of (1) in the setting of equality
atoms, we refer the reader to [Boj, Sect.1.1]; the other points are readily
derivable from (1).

##### Deterministic membership problems.

Let $\mathcal{X}$ be a subclass of nra . We are interested in the following
family of decision problems:

$\mathcal{X}$ membership problem.
Input:  A register automaton $A\in$ nra .
Output:  Does there exist a $B\in\mathcal{X}$ s.t. $L(A)=L(B)$?

We study the decidability status of the $\mathcal{X}$ membership problem where
$\mathcal{X}$ ranges over dra and ${\textsf{\sc dra}_{k}}$ (for every fixed
number of registers $k$). Example 3 shows that there are nra languages that
cannot be accepted by any dra . Moreover, there is no computable bound for the
number of registers $k$ which suffice to recognise a ${\textsf{\sc nra}_{1}}$
language by a ${\textsf{\sc dra}_{k}}$ (when such a number exists), which
follows from the following three observations:

  1. (1)

the dra membership problem is undecidable for ${\textsf{\sc nra}_{1}}$
(Theorem 4),

  2. (2)

the problem of deciding equivalence of a given ${\textsf{\sc nra}_{1}}$ to a
given dra is decidable by Corollary 10 and

  3. (3)

if an ${\textsf{\sc nra}_{1}}$ is equivalent to some ${\textsf{\sc dra}_{k}}$
then it is in fact equivalent to some ${\textsf{\sc dra}_{k}}$ with computably
many control locations (by Lemma 12 from the next section).

##  4\. Decidability of ${\textsf{\sc dra}_{k}}$ membership for ${\textsf{\sc
nra}_{1}}$

In this section we prove our main decidability result for register automata,
which we now recall. See 2 The technical development of this section will also
serve as a preparation for the more involved case of timed automata from
Sections 5 and 6. The key ingredient used in the proof of Theorem 2 is the
following characterisation of those ${\textsf{\sc nra}_{1}}$ languages which
are also ${\textsf{\sc dra}_{k}}$ languages. In particular, this
characterisation provides a bound on the number of control locations of a
${\textsf{\sc dra}_{k}}$ equivalent to a given ${\textsf{\sc nra}_{1}}$ (if
any exists).

######  Lemma 12.

Let $A$ be a ${\textsf{\sc nra}_{1}}$ with $n$ control locations, and let
$k\in\mathbb{N}$. The following conditions are equivalent:

  1. (1)

$L(A)=L(B)$ for some ${\textsf{\sc dra}_{k}}$ $B$.

  2. (2)

For every data word $w$, there is $S\subseteq\mathbb{A}$ of size at most $k$
s.t. the left quotient $w^{-1}L(A)=\\{v\;|\;w\cdot v\in L(A)\\}$ is
$S$-invariant.

  3. (3)

$L(A)=L(B)$ for some ${\textsf{\sc dra}_{k}}$ $B$ with at most
$f(k,n)=(k+1)!\cdot 2^{n\cdot(k+1)}$ control locations.

Using the above lemma we derive a proof of Theorem 2:

######  Proof 4.1 (Proof of Theorem 2).

Given a ${\textsf{\sc nra}_{1}}$ $A$, the decision procedure enumerates all
${\textsf{\sc dra}_{k}}$ $B$ with at most $f(k,n)$ locations and checks
whether $L(A)=L(B)$, using Corollary 10. If no such ${\textsf{\sc dra}_{k}}$
$B$ is found, the procedure answers negatively. Note that the fact that $A$ is
${\textsf{\sc nra}_{1}}$ is crucial here, since otherwise the equivalence
check above would not be decidable. In fact, this is the only place where the
one register restriction really plays a rôle: A generalisation of Lemma 12 for
$A$ being a ${\textsf{\sc nra}_{l}}$ for $l\geq 1$ could be stated and proved;
however we prefer to avoid the additional notational complications of dealing
with the general case since we need Lemma 12 only in the case $l=1$.

######  Remark 13 (Complexity).

The decision procedure for ${\textsf{\sc nra}_{1}}$ invokes the Ackermann
subroutine to check equivalence between a ${\textsf{\sc nra}_{1}}$ and a
candidate dra . This is in a sense unavoidable, since we show in Theorem 6
that the ${\textsf{\sc dra}_{k}}$ membership problem is Ackermann-hard for
${\textsf{\sc nra}_{1}}$.

The proof of Lemma 12 is presented below in Sec. 4.1. We remark that the lemma
partially follows from the literature of automata theory in sets with atoms.
For instance, the most interesting implication (2)$\Rightarrow$(3), even for
$A$ an arbitrary ${\textsf{\sc nra}_{l}}$ with $l\geq 1$, minus the concrete
bound $f(k,n)$ on control locations of $B$, follows from the following known
facts: (a) $L(A)$ is recognised by a nondeterministic equivariant orbit-finite
automaton [Boj, Theorem 5.11], (b) the assumption (2) implies that the Myhill-
Nerode equivalence of $L$ has orbit-finite index, (c) thus by [Boj, Theorem
5.14] $L(A)$ is recognised by a deterministic orbit-finite automaton
$B^{\prime}$, and (d) we can construct from $B^{\prime}$ some language-
equivalent ${\textsf{\sc dra}_{k^{\prime}}}$ $B$. However, this would not
yield (1) the fact that we can even take $k^{\prime}=k$ (i.e., the number of
registers of $B$ can be taken to be the size $k$ of the supports $S$ in the
assumption), and (2) the concrete bound $f(k,n)$ on the number of control
locations of $B$ (a computable such bound is necessary in the automata
enumeration procedure in the proof of Theorem 2). For these reasons, we
provide a full proof of the lemma.

###  4.1. Proof of Lemma 12

Let us fix a ${\textsf{\sc nra}_{1}}$
$A=(\mathtt{X},\Sigma,\mathtt{L},\mathtt{L}_{I},\mathtt{L}_{F},\Delta)$ and
$k\in\mathbb{N}$. Let $n=|{\mathtt{L}}|$ be the number of control locations of
$A$. The implication (3)$\Rightarrow$(1) holds trivially. The implication
(1)$\Rightarrow$(2) holds just because every left quotient $w^{-1}L(A)$ is the
same as $w^{-1}L(B)$ by the assumption $L(A)=L(B)$ for a ${\textsf{\sc
dra}_{k}}$ $B$, and, since $B$ is deterministic, the latter quotient
$w^{-1}L(B)$ equals $L_{B}(c)$ for some configuration $c=(p,\mu)$. The latter
is $\mu(\mathtt{X})$-invariant by Lemma 11(3), and clearly
$|{\mu(\mathtt{X})}|\leq k$. (Notice that $A$ did not play a rôle here.)

It thus remains to prove the implication (2)$\Rightarrow$(3), which is the
content of the rest of the section. Assuming (2), we are going to define a
${\textsf{\sc dra}_{k}}$ $B^{\prime}$ with registers
$\mathtt{X}=\\{\mathtt{x}_{1},\dots,\mathtt{x}_{k}\\}$ and with at most
$f(k,n)$ locations such that $L(B^{\prime})=L(A)$. We start from the
transition system $\mathcal{X}$ obtained by the finite powerset construction
underlying the determinisation of $A$. Next, after a series of language-
preserving transformations, we will obtain a transition system isomorphic to
the reachable part of $\left\llbracket B^{\prime}\right\rrbracket$ for some
${\textsf{\sc dra}_{k}}$ $B^{\prime}$. As the last step, we extract from this
deterministic transition system a syntactic definition of $B^{\prime}$. This
is achievable due to the invariance properties witnessed by the transition
systems in the course of the transformation.

##### Macro-configurations.

For simplicity, we will abuse the notation and write $c=(p,a)$ for a
configuration $c=(p,\\{\mathtt{x}_{1}\mapsto a\\})$ of $A$, where
$p\in\mathtt{L}$ and $a\in\mathbb{A}\cup\\{\bot\\}$. A _macro-configuration_
is a (not necessarily finite) set $X$ of configurations $(p,a)$ of $A$. We use
the notation $L_{A}(X):=\bigcup_{c\in X}L_{A}(c)$.

Let $\text{\sc succ}_{\sigma,a}(X):=\\{c^{\prime}\in\left\llbracket
A\right\rrbracket\;|\;c\xrightarrow{\sigma,a}c^{\prime}\text{ for some }c\in
X\\}$ be the set of successors of configurations in $X$ which can be reached
by reading $(\sigma,a)\in\Sigma\times\mathbb{A}$. We define a deterministic
transition system $\mathcal{X}$ consisting of the macro-configurations
reachable in the course of determinisation of $A$. Let $\mathcal{X}$ be the
smallest set of macro-configurations and transitions such that

  * •

$\mathcal{X}$ contains the initial macro-configuration:
$X_{0}=\\{(p,\bot)\;|\;p\in\mathtt{L}_{I}\\}\in\mathcal{X}$;

  * •

$\mathcal{X}$ is closed under successor: for every $X\in\mathcal{X}$ and
$(\sigma,a)\in\Sigma\times\mathbb{A}$, there is a transition
$X\xrightarrow{\sigma,a}\text{\sc succ}_{\sigma,a}(X)$ in $\mathcal{X}$.

Due to the fact that $\left\llbracket A\right\rrbracket$ is finitely
branching, i.e. $\text{\sc succ}_{\sigma,a}(\\{c\\})$ is finite for every
fixed $(\sigma,a)$, all macro-configurations $X\in\mathcal{X}$ are finite. Let
the final configurations of $\mathcal{X}$ be
$F_{\mathcal{X}}=\\{X\in\mathcal{X}\;|\;X\cap F\neq\emptyset\\}$ where
$F\subseteq\left\llbracket A\right\rrbracket$ is the set of final
configurations of $A$. $L_{A}(X)=L_{\mathcal{X}}(X)$ for every
$X\in\mathcal{X}$. In particular $L(A)=L_{\mathcal{X}}(X_{0})$. For a macro-
configuration $X$ we write $\text{\sc Val}(X):=\\{a\in\mathbb{A}\;|\;\exists
p{\;\cdot\;}(p,a)\in X\\}$ to denote the set of atoms appearing in $X$.

##### Pre-states.

By assumption (2), for every macro-configuration $X\in\mathcal{X}$, $L_{A}(X)$
is $S$-invariant for some $S$ of size at most $k$, but the macro-configuration
$X$ itself needs not be $S$-invariant in general. Indeed, a finite macro-
configuration $X\in\mathcal{X}$ is $S$-invariant if, and only if, $\text{\sc
Val}(X)\subseteq S$, which is impossible in general when $X$ is arbitrarily
large while the size of $S$ is bounded (by $k$). Intuitively, in order to
assure $S$-invariance we will replace $X$ by its $S$-closure
$\textrm{Cl}_{S}(X)$ (recall Fact 7).

The _least support_ of a set with atoms $X$ is the least
$S\subseteq\mathbb{A}$ w.r.t. set inclusion s.t. $X$ is $S$-invariant. In the
case of equality atoms every set with atoms has the least support, which is
moreover finite (see [BKL14, Cor. 9.4] or [Boj, Thm. 6.1]). By assumption, the
least finite support of every macro-configuration $X$ in $\mathcal{X}$ has
size at most $k$.

A _pre-state_ is a pair $Y=(X,S)$, where $X$ is a macro-state whose least
finite support is $S$. Thus $X$ is $S$-invariant which, together with the fact
that $S$ has size at most $k$, implies that there are only finitely many pre-
states up to automorphism. We define the deterministic transition system
$\mathcal{Y}$ as the smallest set of pre-states and transitions between them
such that:

  * •

$\mathcal{Y}$ contains the initial pre-state:
$Y_{0}=(X_{0},\emptyset)\in\mathcal{Y}$;

  * •

$\mathcal{Y}$ is closed under the closure of successor: For every
$(X,S)\in\mathcal{Y}$ and $(\sigma,a)\in\Sigma\times\mathbb{A}$, the pre-state
$(X^{\prime},S^{\prime})$ is in $\mathcal{Y}$ together with transition
$(X,S)\xrightarrow{\sigma,a}(X^{\prime},S^{\prime})$, where $S^{\prime}$ is
the least finite support of the language
$L^{\prime}=(\sigma,a)^{-1}L_{A}(X)=L_{A}(\text{\sc succ}_{\sigma,a}(X))$, and
$X^{\prime}=\textrm{Cl}_{S^{\prime}}(\text{\sc succ}_{\sigma,a}(X))$.

Suppose that $k=3$, a successor of some macro-configuration $X$ has the shape
$\text{\sc
succ}_{\sigma,a_{1}}(X)=\\{(p,a_{1}),(q,a_{1}),(r,a_{2}),(s,a_{3})\\}$ and the
least finite support $S^{\prime}$ of $L^{\prime}$ is $\\{a_{1},a_{3}\\}$,
where $a_{1},a_{2},a_{3}\in\mathbb{A}$ are pairwise-different. Then
$X^{\prime}=\\{(p,a_{1}),(q,a_{1})\\}\cup\\{(r,a)\mid
a\in\mathbb{A}\setminus\\{a_{1},a_{3}\\}\\}\cup\\{(s,a_{3})\\}$.

By assumption, $L^{\prime}$ is $T$-invariant for some $T\subseteq\mathbb{A}$
with $|{T}|\leq k$. Since $X$ is $S$-invariant, $L^{\prime}$ is also
$(S\cup\\{a\\})$-invariant. By the least finite support property of equality
atoms, finite supports are closed under intersection, and hence
$S^{\prime}\subseteq(S\cup\\{a\\})\cap T$, which implies $|{S^{\prime}}|\leq
k$.

By Lemma 11 we deduce: [Invariance of $\mathcal{Y}$] For every two transitions

$(X_{1},S_{1})\xrightarrow{\sigma,a_{1}}(X^{\prime}_{1},S^{\prime}_{1})\qquad\text{and}\qquad(X_{2},S_{2})\xrightarrow{\sigma,a_{2}}(X^{\prime}_{2},S^{\prime}_{2})$

in $\mathcal{Y}$ and an automorphism $\pi$, if $\pi(X_{1})=X_{2}$ and
$\pi(S_{1})=S_{2}$ and $\pi(a_{1})=a_{2}$, then we have
$\pi(X^{\prime}_{1})=X^{\prime}_{2}$ and $\pi(S^{\prime}_{1})=S^{\prime}_{2}$.
Let the final configurations of $\mathcal{Y}$ be
$F_{\mathcal{Y}}=\\{(X,S)\in\mathcal{Y}\;|\;X\cap\mathtt{L}_{F}\neq\emptyset\\}$.
By induction on the length of data words it is easy to show:
$L_{\mathcal{X}}(X_{0})=L_{\mathcal{Y}}(Y_{0})$.

##### States.

We now introduce _states_ , which are designed to be in one-to-one
correspondence with configurations of the forthcoming ${\textsf{\sc dra}_{k}}$
$B^{\prime}$. Intuitively, a state differs from a pre-state $(X,S)$ only by
allocating the values from (some superset of) $S$ into $k$ registers. Thus,
while a pre-state contains a set $S$, the corresponding state contains a
register assignment $\mu:\mathbb{A}_{\bot}^{\mathtt{X}}$ with image
$\mu(\mathtt{X})\supseteq S$.

Let $\mathtt{X}=\\{\mathtt{x}_{1},\dots,\mathtt{x}_{k}\\}$ be a set of $k$
registers. A _state_ is a pair $Z=(X,\mu)$, where $X$ is a macro-
configuration, $\mu:\mathbb{A}_{\bot}^{\mathtt{X}}$ is a register assignment,
and $X$ is $\mu(\mathtt{X})$-invariant. Thus every state $(X,\mu)$ determines
uniquely a corresponding pre-state $\tau(X,\mu)=(X,S)$ where
$S\subseteq\mu(\mathtt{X})$ is the least finite support of $X$.

We continue Example 4.1. States corresponding to the pre-state
$(X^{\prime},S^{\prime})$ feature the macro-configuration $X^{\prime}$, but
can have different register valuations. One of them is
$(X^{\prime},\mu^{\prime})$, where $\mu^{\prime}=\\{\mathtt{x}_{1}\mapsto
a_{1},\mathtt{x}_{2}\mapsto a_{3},\mathtt{x}_{3}\mapsto a_{1}\\}$.

We now define a deterministic transition system $\mathcal{Z}$. Its states are
all those $(X,\mu)$ satisfying $\tau(X,\mu)\in\mathcal{Y}$, and transitions
are determined as follows: $\mathcal{Z}$ contains a transition
$(X,\mu)\xrightarrow{\sigma,a}(X^{\prime},\mu^{\prime})$ if $\mathcal{Y}$
contains the corresponding transition
$\tau(X,\mu)\xrightarrow{\sigma,a}\tau(X^{\prime},\mu^{\prime})=(X^{\prime},S^{\prime})$,
and $\mu^{\prime}=\mu[\mathtt{Y}\mapsto a]$, where

$\displaystyle\mathtt{Y}\ =\
\\{\mathtt{x}_{i}\in\mathtt{X}\;|\;\mu(\mathtt{x}_{i})\notin S^{\prime}\text{
or }\mu(\mathtt{x}_{i})=\mu(\mathtt{x}_{j})\text{ for some }j>i\\}.$ (5)

The equation (5) defines a deterministic update policy555There are in general
many correct deterministic update policies, but for our purposes it suffices
to define one such deterministic update policy. of the register assignment
$\mu$ that amounts to updating with the current input atom $a$ all registers
$\mathtt{x}_{i}$ whose value is either no longer needed (because
$\mu(\mathtt{x}_{i})\notin S^{\prime}$), or is shared with some other register
$x_{j}$, for $j>i$ and is thus redundant. It is easy to see that the above
register update policy guarantees that
$S^{\prime}\subseteq\mu^{\prime}(\mathtt{X})\subseteq S^{\prime}\cup\\{a\\}$.
Using Claim 4.1 we derive: [Invariance of $\mathcal{Z}$] For every two
transitions

$(X_{1},\mu_{1})\xrightarrow{\sigma,a_{1}}(X^{\prime}_{1},\mu^{\prime}_{1})\qquad\text{and}\qquad(X_{2},\mu_{2})\xrightarrow{\sigma,a_{2}}(X^{\prime}_{2},\mu^{\prime}_{2})$

in $\mathcal{Z}$ and an automorphism $\pi$, if $\pi(X_{1})=X_{2}$ and
$\pi{\circ}{\mu_{1}}=\mu_{2}$ and $\pi(a_{1})=a_{2}$, then we have
$\pi(X^{\prime}_{1})=X^{\prime}_{2}$ and
$\pi{\circ}{\mu^{\prime}_{1}}=\mu^{\prime}_{2}$. Let the initial state be
$Z_{0}=(X_{0},\lambda\mathtt{x}.\bot)$, and let final states be
$F_{\mathcal{Z}}=\\{(X,\mu)\in\mathcal{Z}\;|\;X\cap F\neq\emptyset\\}$. By
induction on the length of data words one proves:
$L_{\mathcal{Y}}(Y_{0})=L_{\mathcal{Z}}(Z_{0})$. In the sequel we restrict
$\mathcal{Z}$ to states reachable from $Z_{0}$.

##### Orbits of states.

Recall that the action of automorphisms on macro-configurations and reset-
point assignments is extended to states as
$\pi(X,\mu)=(\pi(X),\pi{\circ}\mu)$, and that the orbit of a state $Z$ is
defined as $\text{\sc
orbit}(Z)=\\{\pi(Z)\;|\;\pi\in\textrm{Aut}(\mathbb{A})\\}$.

While a state is designed to correspond to a configuration of the forthcoming
${\textsf{\sc dra}_{k}}$ $B^{\prime}$, its orbit is designed to play the rôle
of control location of $B^{\prime}$. We therefore need to prove that the set
of orbits $\\{\text{\sc orbit}(Z)\;|\;Z\in\mathcal{Z}\\}$ is finite and its
size is bounded by $f(k,n)$.

Let $M_{k}$ denote the number of orbits of register valuations
$\mathbb{A}_{\bot}^{\mathtt{X}}$, which is the same as the number of orbits of
$k$-tuples $\mathbb{A}_{\bot}^{k}$. In case of equality atoms we have
$M_{k}\leq(k+1)!$ Indeed, at the first position there are two possibilities,
$\bot$ or an atom; at the second position there are at most three
possibilities: $\bot$, the same atom at the one at the first position, or a
fresh atom; and so on, until the last position where there are at most $k+1$
possibilities.

Every $l$-element subset $S=\\{a_{1},a_{2},\ldots,a_{l}\\}\subseteq\mathbb{A}$
of atoms induces, in the case of equality atoms, exactly $l+1$ different
$S$-orbits of atoms:

$S\text{-\sc orbits}\ =\ \\{\text{\sc orbit}_{S}(a)\;|\;a\in\mathbb{A}\\}\ =\
\\{\\{a_{1}\\},\\{a_{2}\\},\ldots,\\{a_{l}\\},\mathbb{A}-S\\}.$

Therefore, each $S\subseteq\mathbb{A}$ of size at most $k$ induces at most
$N_{k}:=k+1$ different $S$-orbits of atoms.

Consider a state $Z=(X,\mu)$ and let $S=\mu(\mathtt{X})$. We define the
characteristic function $\text{char}_{Z}:S\text{-\sc
orbits}\to{\mathcal{P}}(\mathtt{L})$ as follows:

$\text{char}_{Z}(o)=\\{l\in\mathtt{L}\;|\;(l,a)\in X\text{ for some }a\in
o\\}.$

Since $X$ is $S$-invariant, the choice of the atom $a\in o$ is irrelevant, and
we conclude: Every state $Z=(X,\mu)$ is uniquely determined by its register
valuation $\mu$ and by the characteristic function $\text{char}_{Z}$.

The size of $\\{\text{\sc orbit}(Z)\;|\;Z\in\mathcal{Z}\\}$ is at most
$M_{k}\cdot 2^{n\cdot N_{k}}$.

######  Proof 4.2.

We show that there are at most $M_{k}\cdot(2^{n})^{N_{k}}$ different orbits of
states. Consider two states $Z=(X,\mu)$ and $Z^{\prime}=(X^{\prime},\mu)$ and
let $S=\mu(\mathtt{X})$ and $S^{\prime}=\mu^{\prime}(\mathtt{X})$. Suppose
that the register valuations $\mu$ and $\mu^{\prime}$ are in the same orbit:
$\pi\circ\mu=\mu^{\prime}$ for some automorphism $\pi$. Thus
$\pi(S)=S^{\prime}$, and moreover $\pi$ induces a bijection $\widetilde{\pi}$
between $S\text{-\sc orbits}$ and $S^{\prime}\text{-\sc orbits}$. Note that,
once $S$ is fixed, there are at most $(2^{n})^{N_{k}}$ possible characteristic
functions of $Z$, and likewise for $S^{\prime}$ and $Z^{\prime}$. Supposing
further that the characteristic functions agree, i.e., satisfy
$\text{char}_{Z}=\text{char}_{Z^{\prime}}\circ\widetilde{\pi}$, using Claim
4.1 we derive $\pi(Z)=Z^{\prime}$, i.e., $Z$ and $Z^{\prime}$ are in the same
orbit. Therefore, since the number of orbits of register valuations
$\mu,\mu^{\prime}$ is at most $M_{k}$, and for each such orbit the number of
different characteristic functions is at most $(2^{n})^{N_{k}}$, the number of
different orbits of states is bounded as required.

For future use we observe that every state is uniquely determined by its
register valuation and its orbit: Let $Z=(X,\mu)$ and
$Z^{\prime}=(X^{\prime},\mu)$ be two states in $\mathcal{Z}$ with the same
register valuation. If $\pi(X)=X^{\prime}$ and $\pi{\circ}\mu=\mu$ for some
automorphism $\pi$ then $X=X^{\prime}$.

######  Proof 4.3.

Indeed, $X$ is $\mu(X)$-invariant and hence $\pi(X)=X$, which implies
$X=X^{\prime}$.

In the terminology of automata in sets with atoms, we have proved that
$\mathcal{Z}$ is a _deterministic orbit-finite automaton_ (c.f. [Boj, Sec.
5.2] for a definition), with the concrete bound on the number of orbits given
by Lemma 4.1.

##### Construction of the dra.

As the last step we define a ${\textsf{\sc dra}_{k}}$
$B^{\prime}=(\mathtt{X},\Sigma,\mathtt{L}^{\prime},\\{o_{0}\\},\mathtt{L}^{\prime}_{F},\Delta^{\prime})$
such that the reachable part of $\left\llbracket B^{\prime}\right\rrbracket$
is isomorphic to $\mathcal{Z}$. Let locations
$\mathtt{L}^{\prime}=\\{\text{\sc orbit}(Z)\;|\;Z\in\mathcal{Z}\\}$ be the
orbits of states from $\mathcal{Z}$, the initial location be the orbit $o_{0}$
of $Z_{0}$, and final locations $\mathtt{L}^{\prime}_{F}=\\{\text{\sc
orbit}(Z)\;|\;Z\in F_{\mathcal{Z}}\\}$ be orbits of final states. Let each
transition
$Z=(X,\mu)\xrightarrow{\sigma,a}(X^{\prime},\mu^{\prime})=Z^{\prime}$ in
$\mathcal{Z}$ induce a transition rule in $B^{\prime}$

$\displaystyle(o,\sigma,\psi,\mathtt{Y},o^{\prime})\in\Delta^{\prime}$ (6)

where $o=\text{\sc orbit}(Z)$, $o^{\prime}=\text{\sc orbit}(Z^{\prime})$,
$\mathtt{Y}=\\{\mathtt{x}\in\mathtt{X}\;|\;\mu^{\prime}(\mathtt{x})=a\\}$, and
the constraint $\psi(\mathtt{x}_{1},\ldots,\mathtt{x}_{k},\mathtt{y})$ defines
the orbit of $(\mu(\mathtt{x}_{1}),\dots,\mu(\mathtt{x}_{k}),a)$ (here we rely
on Claim 3). We argue that the automaton $B^{\prime}$ is deterministic:
Suppose that $B^{\prime}$ has two transition rules
$o\xrightarrow{\sigma,\psi_{1},\mathtt{Y}_{1}}o^{\prime}_{1}$ and
$o\xrightarrow{\sigma,\psi_{2},\mathtt{Y}_{2}}o^{\prime}_{2}$ with the same
source location $o$ and jointly satisfiable constraints
($\left\llbracket\psi_{1}\land\psi_{2}\right\rrbracket\neq\emptyset$). Then
the target locations are equal ($o^{\prime}_{1}=o^{\prime}_{2}$), and the same
registers are updated ($\mathtt{Y}_{1}=\mathtt{Y}_{2}$).

######  Proof 4.4.

Since the constraints are jointly satisfiable, both transition rules are
enabled in some configuration $c=(o,\mu)$ and for some input atom
$a\in\mathbb{A}$. By Claim 4.1, $c$ determines a corresponding state
$Z=(X,\mu)$ with $o=\text{\sc orbit}(Z)$ and, since the system $\mathcal{Z}$
is deterministic, both transition rules are induced by a common transition
$(X,\mu)\xrightarrow{\sigma,a}(X^{\prime},\mu^{\prime})$ in $\mathcal{Z}$.
This in turn implies $o_{1}=o_{2}$ and $\mathtt{Y}_{1}=\mathtt{Y}_{2}$, as
required.

$\mathcal{Z}$ is isomorphic to the reachable part of $\left\llbracket
B^{\prime}\right\rrbracket$.

######  Proof 4.5.

For a state $Z=(X,\mu)$, let $\iota(Z)=(\text{\sc orbit}(Z),\mu)$. Let
$\mathcal{Z}^{\prime}$ denote the reachable part of $\left\llbracket
B^{\prime}\right\rrbracket$. By Claim 4.1, the mapping $\iota(\\_)$ is a
bijection between $\mathcal{Z}$ and its image
$\iota(\mathcal{Z})\subseteq\left\llbracket B^{\prime}\right\rrbracket$. We
aim at proving $\iota(\mathcal{Z})=\mathcal{Z}^{\prime}$.

By the very definition (6), the image $\iota(\mathcal{Z})$ is a subsystem of
$\mathcal{Z}^{\prime}$: $\iota(\mathcal{Z})\subseteq\mathcal{Z}^{\prime}$. For
the converse inclusion, recall that $\mathcal{Z}$ is total: for every
$(\sigma_{1},a_{1})\dots(\sigma_{n},a_{n})\in(\Sigma\times\mathbb{A})^{*}$,
there is a sequence of transitions
$(X_{0},\mu_{0})\xrightarrow{\sigma_{1},a_{1}}\cdots\xrightarrow{\sigma_{n},a_{n}}(X_{n},\mu_{n})$
in $\mathcal{Z}$. Therefore $\iota(\mathcal{Z})$ is total too and, since
$\mathcal{Z}^{\prime}$ is deterministic and reachable, the subsystem
$\iota(\mathcal{Z})\subseteq\mathcal{Z}^{\prime}$ necessarily equals
$\mathcal{Z}^{\prime}$.

Claims 4.1, 4.1, 4.1, and 4.1 jointly imply $L(A)=L(B^{\prime})$, which
completes the proof of Lemma 12.

###  4.2. Other atoms

The proof of Theorem 2 straightforwardly generalises to any relational
structure of atoms $\mathbb{A}$ satisfying the following conditions:

  * •

$\mathbb{A}$ is homogeneous [Fra53];

  * •

$\mathbb{A}$ preserves well-quasi orders (wqo): finite induced substructures
of $\mathbb{A}$ labelled by elements of an arbitrary wqo, ordered by label-
respecting embedding, are again a wqo (for details we refer the reader to
[Las16, item (A3), Sect.5]);

  * •

$\mathbb{A}$ is effective: it is decidable, if a given finite structure over
the vocabulary of $\mathbb{A}$ is an induced substructure thereof;

  * •

$\mathbb{A}$ has the least finite support property.

As an example, the structure of densely ordered atoms
$\mathbb{A}=({\mathbb{R}},\leq)$ satisfies all the conditions and hence
Theorem 2 holds for register automata over this structure of atoms.

We briefly discuss the adjustments needed. The syntax of constraints (2) is
extended by adding atomic constraints for all relations in $\mathbb{A}$, and
Claim 3 holds by homogeneity of $\mathbb{A}$. The decision procedure checking
equivalence of a ${\textsf{\sc nra}_{1}}$ and a dra from Corollary 10, invoked
in the proof of Theorem 2, works assuming that $\mathbb{A}$ preserves wqo and
is effective. The least finite support assumption is required in the
definition of pre-states. Finally, again due to homogeneity of $\mathbb{A}$
the bounds $M_{k}$ and $N_{k}$ used in Claim 4.1 are finite (but dependent on
$\mathbb{A}$).

##  5\. Timed automata

The register-based model which is the closest to timed automata is based on
timed atoms $({\mathbb{R}},\leq,{+1})$ [BL12]. However, due to the syntactic
and semantic restrictions which are traditionally imposed on timed automata
(such as monotonicity of time, nonnegative timestamps, the special status of
the initial timestamp 0, and the concrete syntax of transition constraints),
the latter can be seen only as as a strict subclass of the corresponding
register model. For this reason, we present our results on the deterministic
membership probem in the syntax and semantics of timed automata.

##### Timed words and languages.

Fix a finite alphabet $\Sigma$. Let ${\mathbb{R}}$ and ${\mathbb{R}}_{\geq 0}$
denote the reals, resp., the nonnegative reals666Equivalently, the rationals
$\mathbb{Q}$ could be considered in place of reals.. Timed words are obtained
by instantiating data words to timed atoms, and imposing additional
conditions: non-negativeness and monotonicity: A _timed word_ over $\Sigma$ is
any sequence of the form

$\displaystyle w\ =\ (\sigma_{1},t_{1})\,\dots\,(\sigma_{n},t_{n})\ \in\
(\Sigma\times{\mathbb{R}}_{\geq 0})^{*}$ (7)

which is _monotonic_ , in the sense that the timed atoms (called _timestamps_
henceforth) $t_{i}$’s satisfy $0\leq t_{1}\leq t_{2}\leq\dots\leq t_{n}$. For
$w$ a timed word as in (7) and an increment $\delta\in{\mathbb{R}}_{\geq 0}$,
let $w+\delta=(\sigma_{1},t_{1}+\delta)\,\dots\,(\sigma_{n},t_{n}+\delta)$ be
the timed word obtained from $w$ by increasing all timestamps by $\delta$. Let
$\mathbb{T}(\Sigma)$ be the set of all timed words over $\Sigma$, and let
$\mathbb{T}_{\geq{t}}(\Sigma)$ be, for $t\in{\mathbb{R}}_{\geq 0}$, the set of
timed words with $t_{1}\geq t$. A _timed language_ is any subset of
$\mathbb{T}(\Sigma)$.

The concatenation $w\cdot v$ of two timed words $w$ and $v$ is defined only
when the first timestamp of $v$ is greater or equal than the last timestamp of
$w$. Using this partial operation, we define, for a timed word
$w\in\mathbb{T}(\Sigma)$ and a timed language $L\subseteq\mathbb{T}(\Sigma)$,
the left quotient $w^{-1}L:=\\{v\in\mathbb{T}(\Sigma)\;|\;w\cdot v\in L\\}$.
Clearly $w^{-1}L\subseteq\mathbb{T}_{\geq{t_{n}}}(\Sigma)$.

##### Clock constraints and regions.

Let $\mathtt{X}=\\{\mathtt{x}_{1},\dots,\mathtt{x}_{k}\\}$ be a finite set of
clocks. A _clock valuation_ is a function $\mu\in{\mathbb{R}}_{\geq
0}^{\mathtt{X}}$ assigning a non-negative real number $\mu(\mathtt{x})$ to
every clock $\mathtt{x}\in\mathtt{X}$. A _clock constraint_ is a quantifier-
free formula of the form

$\displaystyle\varphi,\psi\ ::\equiv\ \mathbf{true}\ |\ \mathbf{false}\ |\
\mathtt{x}_{i}-\mathtt{x}_{j}\sim z\ |\ \mathtt{x}_{i}\sim z\ |\ \neg\varphi\
|\ \varphi\land\psi\ |\ \varphi\lor\psi,$

where “$\sim$” is a comparison operator in $\\{=,<,\leq,>,\geq\\}$ and
$z\in\mathbb{Z}$. A clock valuation $\mu$ satisfies a constraint $\varphi$,
written $\mu\models\varphi$, if interpreting each clock $\mathtt{x}_{i}$ by
$\mu(\mathtt{x}_{i})$ makes $\varphi$ a tautology. Let
$\llbracket\varphi\rrbracket$ be the set of clock valuations
$\mu\in{\mathbb{R}}_{\geq 0}^{\mathtt{X}}$ s.t. $\mu\models\varphi$. If
$\llbracket\varphi\rrbracket$ is non-empty and it does not strictly include a
non-empty $\llbracket\psi\rrbracket\subsetneq\llbracket\varphi\rrbracket$ for
some constraint $\psi$, then we say that it is a _region_. For example, for
$\mathtt{X}=\\{\mathtt{x},\mathtt{y}\\}$ we have that $r_{0}=\llbracket
1<\mathtt{x}<2\land\mathtt{y}=3\rrbracket$ is a region, while
$r_{1}=\llbracket 1<\mathtt{x}\leq 2\land\mathtt{y}=3\rrbracket$ is not.
Nonetheless, the latter partitions into two regions
$r_{1}=r_{0}\cup\llbracket\mathtt{x}=2\land\mathtt{y}=3\rrbracket$, and we
will later see that this is a general phenomenon. A _$k,m$ -region_ is a
region $\left\llbracket\varphi\right\rrbracket$ where $\varphi$ has $k$ clocks
and absolute value of maximal constant bounded by $m$. For instance, the clock
constraint
$1<\mathtt{x}_{1}<2\;\wedge\;4<\mathtt{x}_{2}<5\;\wedge\;\mathtt{x}_{2}-\mathtt{x}_{1}<3$
defines a $2,5$-region consisting of an open triangle with nodes $(1,4)$,
$(2,4)$ and $(2,5)$. A region $\llbracket\varphi\rrbracket$ is _bounded_ if it
is bounded as a subset of ${\mathbb{R}}_{\geq 0}^{\mathtt{X}}$ in the
classical sense, i.e., there exists $M\in{\mathbb{R}}_{\geq 0}$ s.t.
$\llbracket\varphi\rrbracket\subseteq[0,M]^{\mathtt{X}}$.

##### Timed automata.

A (nondeterministic) _timed automaton_ is a tuple
$A=(\mathtt{X},\Sigma,\mathtt{L},\mathtt{L}_{I},\mathtt{L}_{F},\Delta)$, where
$\mathtt{X}$ is a finite set of clocks, $\Sigma$ is a finite input alphabet,
$\mathtt{L}$ is a finite set of control locations,
$\mathtt{L}_{I},\mathtt{L}_{F}\subseteq\mathtt{L}$ are the subsets of initial,
resp., final, control locations, and $\Delta$ is a finite set of transition
rules of the form

$\displaystyle(p,\sigma,\varphi,\mathtt{Y},q)$ (8)

with $p,q\in\mathtt{L}$ control locations, $\sigma\in\Sigma$, $\varphi$ a
clock constraint to be tested, and $\mathtt{Y}\subseteq\mathtt{X}$ the set of
clocks to be reset. We write nta for the class of all nondeterministic timed
automata, ${\textsf{\sc nta}_{k}}$ when the number $k$ of clocks is fixed,
${\textsf{\sc nta}_{\textnormal{\\_},m}}$ when the bound $m$ on constants is
fixed, and ${\textsf{\sc nta}_{k,m}}$ when both $k$ and $m$ are fixed.

An ${\textsf{\sc nta}_{\textnormal{\\_},m}}$ $A$ is _always resetting_ if
every transition rule resets some clock ($\mathtt{Y}\neq\emptyset$ in (8)),
and _greedily resetting_ if, for every clock $\mathtt{x}$, whenever $\varphi$
implies that the value of $\mathtt{x}$ belongs to
$\\{0,\ldots,m\\}\cup(m,\infty)$, then $\mathtt{x}\in\mathtt{Y}$. Intuitively,
a greedily reseting automaton resets every clock whose value is either an
integer, or exceeds the maximal constant $m$.

##### Reset-point semantics.

We introduce a semantics based on reset points instead of clock valuations. A
_reset-point assignment_ is a function $\mu\in{\mathbb{R}}_{\geq
0}^{\mathtt{X}}$ storing, for each clock $\mathtt{x}\in\mathtt{X}$, the
timestamp $\mu(\mathtt{x})$ when $\mathtt{x}$ was last reset. Reset-point
assignments and clock valuations have the same type ${\mathbb{R}}_{\geq
0}^{\mathtt{X}}$, however we find it technically more convenient to work with
reset points than with clock valuations. The reset-point semantics has already
appeared in the literature on timed automata [Fri98] and it is the foundation
of the related model of timed-register automata [BL12].

A _configuration_ of an nta $A$ is a tuple $(p,\mu,t_{0})$ consisting of a
control location $p\in\mathtt{L}$, a reset-point assignment
$\mu\in{\mathbb{R}}_{\geq 0}^{\mathtt{X}}$, and a “now” timestamp
$t_{0}\in{\mathbb{R}}_{\geq 0}$ satisfying $\mu(\mathtt{x})\leq t_{0}$ for all
clocks $\mathtt{x}\in\mathtt{X}$. Intuitively, $t_{0}$ is the last timestamp
seen in the input and, for every clock $\mathtt{x}$, $\mu(\mathtt{x})$ stores
the timestamp of the last reset of $\mathtt{x}$. A configuration is _initial_
if $p$ is so, $t_{0}=0$, and $\mu(\mathtt{x})=0$ for all clocks $\mathtt{x}$,
and it is _final_ if $p$ is so (without any further restriction on $\mu$ or
$t_{0}$). For a set of clocks $\mathtt{Y}\subseteq\mathtt{X}$ and a timestamp
$u\in{\mathbb{R}}_{\geq 0}$, let $\mu[\mathtt{Y}\mapsto u]$ be the assignment
which is $u$ on $\mathtt{Y}$ and agrees with $\mu$ on
$\mathtt{X}\setminus\mathtt{Y}$. A reset-point assignment $\mu$ together with
$t_{0}$ induces the clock valuation ${t_{0}}-{\mu}$ defined as
$({t_{0}}-{\mu})(\mathtt{x})=t_{0}-\mu(\mathtt{x})$ for all clocks
$\mathtt{x}\in\mathtt{X}$.

Every transition rule (8) induces a _transition_ between configurations

$(p,\mu,t_{0})\xrightarrow{\sigma,t}(q,\nu,t)$

labelled by $(\sigma,t)\in\Sigma\times{\mathbb{R}}_{\geq 0}$ whenever $t\geq
t_{0}$, ${t}-{\mu}\models\varphi$, and $\nu=\mu[\mathtt{Y}\mapsto t]$. The
_timed transition system_ induced by $A$ is $(\left\llbracket
A\right\rrbracket,\xrightarrow{},F)$, where $\left\llbracket
A\right\rrbracket$ is the set of configurations,
${\xrightarrow{}}\subseteq\left\llbracket
A\right\rrbracket\times\Sigma\times{\mathbb{R}}_{\geq 0}\times\left\llbracket
A\right\rrbracket$ is as defined above, and $F\subseteq\left\llbracket
A\right\rrbracket$ is the set of final configurations. Since there is no
danger of confusion, we use $\left\llbracket A\right\rrbracket$ to denote
either the timed transition system above, or its domain. A _run_ of $A$ _over_
a timed word $w$ as in (7) _starting_ in configuration $(p,\mu,t_{0})$ and
_ending_ in configuration $(q,\nu,t_{n})$ is a path $\rho$ in $\left\llbracket
A\right\rrbracket$ of the form
$\rho=(p,\mu,t_{0})\xrightarrow{\sigma_{1},t_{1}}\
\dots\xrightarrow{\sigma_{n},t_{n}}\ (q,\nu,t_{n})$. The run $\rho$ is
accepting if its last configuration satisfies $(q,\nu,t_{n})\in F$. The
language _recognised_ by configuration $(p,\mu,t_{0})$ is defined as:

$\displaystyle L_{\left\llbracket
A\right\rrbracket}(p,\mu,t_{0})=\\{w\in\mathbb{T}(\Sigma)\;|\;\left\llbracket
A\right\rrbracket\text{ has an accepting run over }w\text{ starting in
}(p,\mu,t_{0})\\}.$

Clearly $L_{\left\llbracket
A\right\rrbracket}(p,\mu,t_{0})\subseteq\mathbb{T}_{\geq{t_{0}}}(\Sigma)$. We
write $L_{A}(c)$ instead of $L_{\left\llbracket A\right\rrbracket}(c)$. The
language recognised by the automaton $A$ is $L(A)=\bigcup_{c\text{
initial}}L_{A}(c)$.

A configuration is _reachable_ if it is the ending configuration in a run
starting in an initial configuration. In an always resetting ${\textsf{\sc
nta}_{\textnormal{\\_},m}}$, every reachable configuration $(p,\mu,t_{0})$
satisfies $t_{0}\in\mu(\mathtt{X})$, where
$\mu(\mathtt{X})=\\{\mu(\mathtt{x})\;|\;\mathtt{x}\in\mathtt{X}\\}$; in a
greedily resetting one, (1) $(p,\mu,t_{0})$ has _$m$ -bounded span_, in the
sense that $\mu(\mathtt{X})\subseteq(t_{0}-m,t_{0}]$, and moreover (2) any two
clocks $\mathtt{x},\mathtt{y}$ with integer difference
$\mu(\mathtt{x})-\mu(\mathtt{y})\in\mathbb{Z}$ are actually equal
$\mu(\mathtt{x})=\mu(\mathtt{y})$. Condition (2) follows from the fact that if
$\mathtt{x},\mathtt{y}$ have integer difference and $\mathtt{y}$ was reset
last, then $\mathtt{x}$ was itself an integer when this happened, and in fact
they were both reset together in a greedily resetting automaton.

##### Deterministic timed automata.

A timed automaton $A$ is _deterministic_ if it has exactly one initial
location and, for every two rules
$(p,\sigma,\varphi,\mathtt{Y},q),(p,\sigma^{\prime},\varphi^{\prime},\mathtt{Y}^{\prime},q^{\prime})\in\Delta$,
if $\sigma=\sigma^{\prime}$ and the two transition constraints are jointly
satisfiable
$\left\llbracket\varphi\land\varphi^{\prime}\right\rrbracket\neq\emptyset$,
then $\mathtt{Y}=\mathtt{Y}^{\prime}$ and $q=q^{\prime}$. Hence $A$ has at
most one run over every timed word $w$. A dta can be easily transformed to a
_total_ one, where for every location $p\in\mathtt{L}$ and $\sigma\in\Sigma$,
the sets defined by clock constraints
$\\{\left\llbracket\varphi\right\rrbracket\;|\;\exists\mathtt{Y},q\cdot(p,\sigma,\varphi,\mathtt{Y},q)\in\Delta\\}$
are a partition of ${\mathbb{R}}_{\geq 0}^{\mathtt{X}}$. Thus, a total dta has
exactly one run over every timed word $w$. We write dta for the class of
deterministic timed automata, and ${\textsf{\sc dta}_{k}}$, ${\textsf{\sc
dta}_{\textnormal{\\_},m}}$, and ${\textsf{\sc dta}_{k,m}}$ for the respective
subclasses thereof. A timed language is called nta language, dta language,
etc., if it is recognised by a timed automaton of the respective type.

This is a timed analog of Example 3. Let $\Sigma=\\{\sigma\\}$ be a unary
alphabet. As an example of a timed language $L$ recognised by a ${\textsf{\sc
nta}_{1}}$, but not by any dta, consider the set of non-negative timed words
of the form $(\sigma,t_{1})\cdots(\sigma,t_{n})$ where $t_{n}-t_{i}=1$ for
some $1\leq i<n$. The language $L$ is recognised by the ${\textsf{\sc
nta}_{1}}$
$A=(\mathtt{X},\Sigma,\mathtt{L},\mathtt{L}_{I},\mathtt{L}_{F},\Delta)$ with a
single clock $\mathtt{X}=\\{\mathtt{x}\\}$ and three locations
$\mathtt{L}=\\{p,q,r\\}$, of which $\mathtt{L}_{I}=\\{p\\}$ is initial and
$\mathtt{L}_{F}=\\{r\\}$ is final, and transition rules

$\displaystyle(p,\sigma,\mathbf{true},\emptyset,p)\qquad(p,\sigma,\mathbf{true},\\{\mathtt{x}\\},q)\qquad(q,\sigma,\mathtt{x}<1,\emptyset,q)\qquad(q,\sigma,\mathtt{x}=1,\emptyset,r).$

Intuitively, in $p$ the automaton waits until it guesses that the next input
will be $(\sigma,t_{i})$, at which point it moves to $q$ by resetting the
clock. From $q$, the automaton can accept by going to $r$ only if exactly one
time unit elapsed since $(\sigma,t_{i})$ was read. The language $L$ is not
recognised by any dta since, intuitively, any deterministic acceptor needs to
store unboundedly many timestamps $t_{i}$’s.

##### Deterministic membership problems.

The decision problems for nta we are interested in are analogous to the ones
for nra, but additionally a bound on the maximal constant appearing in a dta
may be specified as a parameter. Let $\mathcal{X}$ be a subclass of nta . We
are interested in the following decision problem.

$\mathcal{X}$ membership problem.
Input:  A timed automaton $A\in$ nta .
Output:  Does there exist a $B\in\mathcal{X}$ s.t. $L(A)=L(B)$?

In the rest of the paper, we study the decidability status of the
$\mathcal{X}$ membership problem where $\mathcal{X}$ ranges over dta,
${\textsf{\sc dta}_{k}}$ (for every fixed number of clocks $k$), ${\textsf{\sc
dta}_{\textnormal{\\_},m}}$ (for every maximal constant $m$), and
${\textsf{\sc dta}_{k,m}}$ (when both clocks $k$ and maximal constant $m$ are
fixed). Example 5 shows that there are nta languages which cannot be accepted
by any dta . Moreover, similarly as in case of nra, there is no computable
bound for the number of clocks $k$ which suffice to recognise a ${\textsf{\sc
nta}_{1}}$ language by a ${\textsf{\sc dta}_{k}}$ (when such a number exists).

##  6\. Invariance of timed automata

A fundamental tool used below is invariance properties of timed languages
recognised by nta with respect to timed automorphisms. In this section we
establish these properties, as extension of analogous properties of register
automata. We also prove a timed analog of the least support property, and
relate regions to orbits of configurations.

Recall that timed automorphisms are monotonic bijections
${\mathbb{R}}\to{\mathbb{R}}$ that preserve integer differences. A timed
automorphism $\pi$ acts on input letters in $\Sigma$ as the identity,
$\pi(a)=a$, and is extended point-wise to timed words
$\pi((\sigma_{1},t_{1})\dots(\sigma_{n},t_{n}))=(\sigma_{0},\pi(t_{1}))\dots(\sigma_{n},\pi(t_{n}))$,
configurations $\pi(p,\mu,t_{0})=(p,\pi{\circ}\mu,\pi(t_{0}))$, transitions
$\pi(c\xrightarrow{\sigma,t}c^{\prime})=\pi(c)\xrightarrow{\sigma,\pi(t)}\pi(c^{\prime})$,
and sets $X$ thereof $\pi(X)=\\{\pi(x)\;|\;x\in X\\}$.

######  Remark 14.

In considerations about timed automata we restrict to nonnegative reals, while
a timed automorphism $\pi$ can in general take a nonnegative real $t\geq 0$ to
a negative one. In the sequel whenever we write $\pi(x)$, for $x$ being any
object like a timestamp, a configuration, a timed word, etc., we always
implicitly assume that $\pi$ is well-defined on $x$, i.e., yields a timestamp,
a configuration, a timed word, etc. In other words, for invariance properties
we restrict to those timed automorphisms that preserve nonnegativeness of all
the involved timestamps.

Let $S\subseteq{\mathbb{R}}_{\geq 0}$. An _$S$ -timed automorphism_ is a timed
automorphism s.t. $\pi(t)=t$ for all $t\in S$. Let $\Pi_{S}$ denote the set of
all $S$-timed automorphisms, and let $\Pi=\Pi_{\emptyset}$. A set $X$ is _$S$
-invariant_ if $\pi(X)=X$ for every $\pi\in\Pi_{S}$; equivalently, for every
$\pi\in\Pi_{S}$, $x\in X$ if, and only if $\pi(x)\in X$. A set $X$ is
_invariant_ if it is $S$-invariant with $S=\emptyset$. The following three
facts express some basic invariance properties.

######  Fact 15.

The timed transition system $\left\llbracket A\right\rrbracket$ is invariant.

######  Proof 6.1.

Suppose
$c=(p,\mu,t_{0})\xrightarrow{\sigma,t}(p^{\prime},\mu^{\prime},t)=c^{\prime}$
due to some transition rule of $A$ whose clock constraint $\varphi$ compares
values of clocks $\mathtt{x}$, i.e., the differences $t-\mu(\mathtt{x})$, to
integers. Since a timed automorphism $\pi$ preserves integer distances, the
same clock constraint is satisfied in $\pi(c)=(p,\pi{\circ}{\mu},\pi(t_{0}))$,
and therefore the same transition rule is applicable yielding the transition
$(p,\pi{\circ}{\mu},\pi(t_{0}))\xrightarrow{\sigma,\pi(t)}(p,\pi{\circ}{\mu^{\prime}},\pi(t))=\pi(c^{\prime})$.

By unrolling the definition of invariance in the previous fact, we obtain that
the set of configurations is invariant, the set of transitions
${\xrightarrow{}}$ is invariant, and that the set of final configurations $F$
is invariant.

######  Fact 16 (Invariance of the language semantics).

The function $c\mapsto L_{A}(c)$ from $\left\llbracket A\right\rrbracket$ to
languages is invariant, i.e., for all timed automorphisms $\pi$,
$L_{A}(\pi(c))=\pi(L_{A}(c))$.

######  Proof 6.2.

Consider a timed automorphism $\pi$ and an accepting run of $A$ over a timed
word
$w=(\sigma_{1},t_{1})\dots(\sigma_{n},t_{n})\in\mathbb{T}_{\geq{t_{0}}}(\Sigma)$
starting in $c=(p,\mu,t_{0})$:

$\displaystyle(p,\mu,t_{0})\xrightarrow{\sigma_{1},t_{1}}\,\cdots\xrightarrow{\sigma_{n},t_{n}}\,(q,\nu,t_{n}),$

After $\sigma_{i}$ is read, the value of each clock is either the difference
$t_{i}-\mu(\mathtt{x})$ for some $1\leq i\leq n$ and clock
$\mathtt{x}\in\mathtt{X}$, or the difference $t_{i}-t_{j}$ for some $1\leq
j\leq i$. Likewise is the difference of values of any two clocks. Thus clock
constraints of transition rules used in the run compare these differences to
integers. As timed automorphism $\pi$ preserves integer differences, by
executing the same sequence of transition rules we obtain the run over
$\pi(w)$ starting in $\pi(c)=(p,\pi{\circ}\mu,\pi(t_{0}))$:

$(p,\pi{\circ}\mu,\pi(t_{0}))\xrightarrow{\sigma_{1},\pi(t_{1})}\,\cdots\xrightarrow{\sigma_{n},\pi(t_{n})}\,(q,\pi{\circ}\nu,\pi(t_{n})),$

also accepting as it ends in the same location $q$. As
$w\in\mathbb{T}(\Sigma)$ can be chosen arbitrarily, we have thus proved one of
inclusions, namely

$\pi(L_{A}(p,\mu,t_{0}))\ \subseteq\ L_{A}(p,\pi{\circ}\mu,\pi(t_{0})).$

The other inclusion follows from the latter one applied to $\pi^{-1}$ and
$L_{A}(p,\pi{\circ}\mu,\pi(t_{0}))$:

$\pi^{-1}(L_{A}(p,\pi{\circ}\mu,\pi(t_{0})))\ \subseteq\
L_{A}(p,\pi^{-1}{\circ}\pi{\circ}\mu,\pi^{-1}(\pi(t_{0})))\ =\
L_{A}(p,\mu,t_{0}).$

The two implications prove the equality.

######  Fact 17 (Invariance of the language of a configuration).

The language $L_{A}(p,\mu,t_{0})$ is
$(\mu(\mathtt{X})\cup\\{t_{0}\\})$-invariant. Moreover, if $A$ is always
resetting, then $L_{A}(p,\mu,t_{0})$ is $\mu(\mathtt{X})$-invariant.

######  Proof 6.3.

This is a direct consequence of the invariance of semantics. Indeed, for every
$(\mu(\mathtt{X})\cup\\{t_{0}\\})$-timed automorphism $\pi$ the configurations
$c=(p,\mu,t_{0})$ and $\pi(c)=(p,\pi{\circ}\mu,\pi(t_{0}))$ are equal, hence
their languages $L_{A}(c)$ and $L_{A}(\pi(c))$, the latter equal to
$\pi(L_{A}(c))$ by Fact 16, are equal too. Thus, $L=\pi(L)$. Finally, if $A$
is always resetting, then $t_{0}\in\mu(\mathtt{X})$, from which the second
claim follows.

Since timed automorphisms preserve integer differences, only the fractional
parts of elements of $S\subseteq{\mathbb{R}}_{\geq 0}$ matter for
$S$-invariance, and hence it makes sense to restrict to subsets of the half-
open interval $[0,1)$. Let
$\mathsf{fract}({S})=\\{\mathsf{fract}({x})\;|\;x\in S\\}\subseteq[0,1)$ stand
for the set of fractional parts of elements of $S$. The following lemma shows
that, modulo the irrelevant integer parts, there is always the least set $S$
witnessing $S$-invariance (c.f. the least support property of, e.g., equality
atoms).

######  Lemma 18.

For finite subsets $S,S^{\prime}\subseteq{\mathbb{R}}_{\geq 0}$, if a timed
language $L$ is both $S$-invariant and $S^{\prime}$-invariant, then it is also
$S^{\prime\prime}$-invariant as long as
$\mathsf{fract}({S^{\prime\prime}})=\mathsf{fract}({S})\cap\mathsf{fract}({S^{\prime}})$.

######  Proof 6.4.

Let $L$ be an $S$\- and $S^{\prime}$-invariant timed language, and let
$F=\mathsf{fract}({S})$ and $F^{\prime}=\mathsf{fract}({S^{\prime}})$. We
prove that $L$ is an $(F\cap F^{\prime})$-invariant subset of
$\mathbb{T}(\Sigma)$. Consider two timed words
$w,w^{\prime}\in\mathbb{T}(\Sigma)$ such that $w^{\prime}=\pi(w)$ for some
$(F\cap F^{\prime})$-timed automorphism $\pi$. We need to show

$\displaystyle w\in L\quad\text{iff}\quad w^{\prime}\in L,$

which follows immediately by the following claim: Every $(F\cap
F^{\prime})$-timed automorphism $\pi$ decomposes into
$\pi=\pi_{n}\circ\dots\circ\pi_{1}$, where each $\pi_{i}$ is either an $F$\-
or an $F^{\prime}$-timed automorphism. Composition of timed automorphisms
makes $\Pi$ into a group. In short terms, Claim 6.4 states that $\Pi_{F\cap
F^{\prime}}\subseteq\Pi_{F}+\Pi_{F^{\prime}}$, where
$\Pi_{F}+\Pi_{F^{\prime}}$ is the smallest subgroup of $\Pi$ including both
$\Pi_{F}$ and $\Pi_{F^{\prime}}$. We state below in Claim 6 a fact equivalent
to Claim 6.4, and which is based on the proof of Theorem 9.3 in [BKL14]. An
important ingredient of the proof of Claim 6 is the following fact where,
instead of dealing with decomposition of $\pi$, we analyse the individual
orbit of $F\setminus F^{\prime}$, in the special case when both $F\setminus
F^{\prime}$ and $F^{\prime}\setminus F$ are singleton sets: Let
$F,F^{\prime}\subseteq[0,1)$ be finite sets s.t. $F\setminus
F^{\prime}=\\{t\\}$ and $F^{\prime}\setminus F=\\{t^{\prime}\\}$. For every
$(F\cap F^{\prime})$-timed automorphism $\pi$ we have
$\pi(t)=(\pi_{n}\circ\dots\circ\pi_{1})(t)$, for some $\pi_{1},\dots,\pi_{n}$,
each of which is either an $F$\- or an $F^{\prime}$-timed automorphism (i.e.,
belongs to $\Pi_{F}+\Pi_{F^{\prime}}$).

######  Proof 6.5 (Proof of Claim 6.4).

We split the proof into two cases.

##### Case $F\cap F^{\prime}\neq\emptyset$.

Let $l$ be the greatest element of $F\cap F^{\prime}$ smaller than $t$, and
let $h$ be the smallest element of $F\cap F^{\prime}$ greater than $t$,
assuming they both exist. (If $l$ does not exist put $l:=h^{\prime}-1$, where
$h^{\prime}$ is the greatest element of $F\cap F^{\prime}$; symmetrically, if
$h$ does not exists put $h:=l^{\prime}+1$, where $l^{\prime}$ is the smallest
element of $F\cap F^{\prime}$.) Then the $(F\cap F^{\prime})$-orbit
$\\{\pi(t)\;|\;\pi\text{ is an }(F\cap F^{\prime})\text{-timed
automorphism}\\}$ is the open interval $(l,h)$. Take any $(F\cap
F^{\prime})$-timed automorphism $\pi$; without loss of generality assume that
$u=\pi(t)>t$. The only interesting case is $t<t^{\prime}\leq u$. In this case,
we show $\pi(t)=\pi_{2}(\pi_{1}(t))$,where

  * •

$\pi_{1}$ is some $F^{\prime}$-timed automorphism that acts as the identity on
$[t^{\prime},l+1]$ and s.t. $t<\pi_{1}(t)<t^{\prime}$,

  * •

$\pi_{2}$ is some $F$-timed automorphism that acts as the identity on
$[h-1,t]$ and s.t. $\pi_{2}(\pi_{1}(t))=u$.

##### Case $F\cap F^{\prime}=\emptyset$.

Thus $F=\\{t\\}$ and $F^{\prime}=\\{t^{\prime}\\}$. Take any timed
automorphism $\pi$; without loss of generality assume that $\pi(t)>t$. Let
$z\in\mathbb{Z}$ be the unique integer s.t. $t^{\prime}+z-1<t<t^{\prime}+z$.
Let $\pi_{1}$ be an arbitrary $\\{t^{\prime}\\}$-timed automorphism that maps
$t$ to some $t_{1}\in(t,t^{\prime}+z)$. Note that $t_{1}$ may be any value in
$(t,t^{\prime}+z)$. Similarly, let $\pi_{2}$ be an arbitrary $\\{t\\}$-timed
automorphism that maps $t_{1}$ to some $t_{2}\in(t^{\prime},t+1)$. Again,
$t_{2}$ may be any value in $(t^{\prime},t+1)$. By repeating this process
sufficiently many times one finally reaches $\pi(t)$ as required.

Let $F,F^{\prime}\subseteq[0,1)$ be finite sets and let $G\subseteq\Pi$ be a
subgroup of $\Pi$. If $\Pi_{F}\subseteq G$ and $\Pi_{F^{\prime}}\subseteq G$
then $\Pi_{F\cap F^{\prime}}\subseteq G$.

######  Proof 6.6 (Proof of Claim 6).

The proof is by induction on the size of the (finite) set $F\cup F^{\prime}$.
If $F\subseteq F^{\prime}$ or $F^{\prime}\subseteq F$, then the conclusion
follows trivially. Otherwise, consider any $t\in F\setminus F^{\prime}$ and
$t^{\prime}\in F^{\prime}\setminus F$; obviously $t\neq t^{\prime}$. Define
$E=(F\cup F^{\prime})\setminus\\{t,t^{\prime}\\}$. We have $F\subseteq
E\cup\\{t\\}$ and $F^{\prime}\subseteq E\cup\\{t^{\prime}\\}$ hence

$\Pi_{E\cup\\{t\\}}\subseteq\Pi_{F}\subseteq
G\qquad\Pi_{E\cup\\{t^{\prime}\\}}\subseteq\Pi_{F^{\prime}}\subseteq G.$

We shall now prove that $\Pi_{E}\subseteq G$. To this end, consider any
$\pi\in\Pi_{E}$. By Claim 6.4, there exists a permutation

$\tau=\pi_{n}\circ\dots\circ\pi_{1}\in\Pi_{E\cup\\{t\\}}+\Pi_{E\cup\\{t^{\prime}\\}}$

such that $\pi(t)=\tau(t)$. In other words, each of $\pi_{1},\dots,\pi_{n}$ is
either a $(E\cup\\{t\\})$\- or a $(E\cup\\{t^{\prime}\\})$-timed automorphism.
Since $\Pi_{E\cup\\{t\\}}\subseteq G$ and
$\Pi_{E\cup\\{t^{\prime}\\}}\subseteq G$, all $\pi_{i}\in G$, hence also
$\tau\in G$.

On the other hand, clearly $\Pi_{E\cup\\{t\\}}\subseteq\Pi_{E}$ and
$\Pi_{E\cup\\{t^{\prime}\\}}\subseteq\Pi_{E}$, so all $\pi_{i}\in\Pi_{E}$,
therefore $\tau\in\Pi_{E}$. As a result, $\pi^{-1}\circ\tau\in\Pi_{E}$. Since
$(\pi^{-1}\circ\tau)(t)=t$, we obtain
$\pi^{-1}\circ\tau\in\Pi_{E\cup\\{t\\}}$, therefore $\pi^{-1}\circ\tau\in G$.
Together with $\tau\in G$ proved above, this gives $\pi\in G$. Thus we have
proved $\Pi_{E}\subseteq G$.

It is now easy to show that $\Pi_{F\cap F^{\prime}}\subseteq G$. Indeed,
$|F\cup E|=|F\cup F^{\prime}|-1$, so by the inductive assumption for $F$ and
$E$, we have $\Pi_{F\setminus\\{t\\}}\subseteq G$ (note that
$F\setminus\\{t\\}=F\cap E$). Further, $|(F\setminus\\{t\\})\cup
F^{\prime}|=|F\cup F^{\prime}|-1$, so $\Pi_{F\cap F^{\prime}}\subseteq G$
(note that $(F\setminus\\{t\\})\cap F^{\prime}=F\cap F^{\prime}$), as
required.

Claim 6 immediately implies Claim 6.4 by taking $G=\Pi_{F}+\Pi_{F^{\prime}}$.
Lemma 18 is thus proved.

As a direct corollary of Lemma 18, we have:

######  Corollary 19.

For every timed language $L$, the set
$\\{\mathsf{fract}({S})\;|\;S\subseteq_{\text{fin}}{\mathbb{R}}_{\geq
0},L\text{ is $S$-invariant}\\}$, if nonempty, has a least (inclusion-wise)
element.

Finally, recall $S$-orbits and orbits of elements, as defined abstractly in
Section 2. Every bounded region corresponds to an orbit of configurations.
Hence, in case of greedily resetting nta where all reachable regions are
bounded, orbits of reachable configurations are in bijective correspondence
with reachable regions:

######  Fact 20.

Assume $A$ is a greedily resetting ${\textsf{\sc nta}_{k,m}}$. Two reachable
configurations $(p,\mu,t_{0})$ and $(p,\mu^{\prime},t_{0}^{\prime})$ of $A$
with the same control location $p$ have the same orbit if, and only if, the
corresponding clock valuations ${t_{0}}-{\mu}$ and
${t_{0}^{\prime}}-{\mu^{\prime}}$ belong to the same $k,m$-region.

##  7\. Decidability of ${\textsf{\sc dta}_{k}}$ and ${\textsf{\sc
dta}_{k,m}}$ membership for ${\textsf{\sc nta}_{1}}$

In this section we prove our main decidability result for timed automata,
which we now recall. See 1 Both results are shown using the following key
characterisation of those ${\textsf{\sc nta}_{1}}$ languages which are also
${\textsf{\sc dta}_{k}}$ languages.

######  Lemma 21.

Let $A$ be a ${\textsf{\sc nta}_{1,m}}$ with $n$ control locations, and let
$k\in\mathbb{N}$. The following conditions are equivalent:

  1. (1)

$L(A)=L(B)$ for some always resetting ${\textsf{\sc dta}_{k}}$ $B$.

  2. (2)

For every timed word $w$, there is $S\subseteq{\mathbb{R}}_{\geq 0}$ of size
at most $k$ s.t. the last timestamp of $w$ is in $S$ and $w^{-1}L(A)$ is
$S$-invariant.

  3. (3)

$L(A)=L(B)$ for some always resetting ${\textsf{\sc dta}_{k,m}}$ $B$ with at
most $f(k,m,n)=\textsf{Reg}(k,m)\cdot 2^{n(2km+1)}$ control locations
($\textsf{Reg}(k,m)$ stands for the number of $k,m$-regions).

As in case of register automata, this characterisation provides a bound on the
number of control locations of a ${\textsf{\sc dta}_{k}}$ equivalent to a
given ${\textsf{\sc nta}_{1}}$ (if any exists).

The proof of Theorem 1 builds on Lemma 21 and on the following fact:

######  Lemma 22.

The ${\textsf{\sc dta}_{k}}$ and ${\textsf{\sc dta}_{k,m}}$ membership
problems are both decidable for dta languages.

######  Proof 7.1.

We reduce to a deterministic separability problem. Recall that a language $S$
_separates_ two languages $L,M$ if $L\subseteq S$ and $S\cap M=\emptyset$. It
has recently been shown that the ${\textsf{\sc dta}_{k}}$ and ${\textsf{\sc
dta}_{k,m}}$ separability problems are decidable for nta [CLP20b, Theorem
1.1], and thus, in particular, for dta . To solve the membership problem,
given a dta $A$, the procedure computes a dta $A^{\prime}$ recognising the
complement of $L(A)$ and checks whether $A$ and $A^{\prime}$ are ${\textsf{\sc
dta}_{k}}$ separable (resp., ${\textsf{\sc dta}_{k,m}}$ separable) by using
the result above. It is a simple set-theoretic observation that $L(A)$ is a
${\textsf{\sc dta}_{k}}$ language if, and only if, the languages $L(A)$ and
$L(A^{\prime})$ are separated by some ${\textsf{\sc dta}_{k}}$ language, and
likewise for ${\textsf{\sc dta}_{k,m}}$ languages.

######  Proof 7.2 (Proof of Theorem 1).

We solve both problems in essentially the same way. Given a ${\textsf{\sc
nta}_{1,m}}$ $A$, the decision procedure enumerates all always resetting
${\textsf{\sc dta}_{k+1,m}}$ $B$ with at most $f(k+1,m,n)$ locations and
checks whether $L(A)=L(B)$ (which is decidable by [OW04, Theorem 17]). If no
such ${\textsf{\sc dta}_{k+1}}$ $B$ is found, the $L(A)$ is not an always
resetting ${\textsf{\sc dta}_{k+1}}$ language, due to Lemma 21, and hence
forcedly is not a ${\textsf{\sc dta}_{k}}$ language either; the procedure
therefore answers negatively. Otherwise, in case when such a ${\textsf{\sc
dta}_{k+1}}$ $B$ is found, then a ${\textsf{\sc dta}_{k}}$ membership (resp.
${\textsf{\sc dta}_{k,m}}$ membership) test is performed on $B$, which is
decidable due to Lemma 22.

######  Remark 23 (Complexity).

The decision procedure for ${\textsf{\sc nta}_{1}}$ invokes the HyperAckermann
subroutine of [OW04] to check equivalence between a ${\textsf{\sc nta}_{1}}$
and a candidate dta . This is in a sense unavoidable, since we show in Theorem
5 that ${\textsf{\sc dta}_{k}}$ and ${\textsf{\sc dta}_{k,m}}$ membership
problems are HyperAckermann-hard for ${\textsf{\sc nta}_{1}}$.

In the rest of this section we present the proof of Lemma 21. The proof is a
suitable extension and refinement of the argument used in case of register
automata in Section 4.

###  7.1. Proof of Lemma 21

Let us fix a ${\textsf{\sc nta}_{1,m}}$
$A=(\Sigma,\mathtt{L},\\{\mathtt{x}\\},\mathtt{L}_{I},\mathtt{L}_{F},\Delta)$,
where $m$ is the greatest constant used in clock constraints in $A$, and
$k\in\mathbb{N}$. We assume w.l.o.g. that $A$ is greedily resetting: This is
achieved by resetting the clock as soon as upon reading an input symbol its
value becomes greater than $m$ or is an integer $\leq m$; we can record in the
control location the actual integral value if it is $\leq m$, or a special
flag otherwise. Consequently, after every discrete transition the value of the
clock is at most $m$, and if it is an integer then it equals 0.

The implication 3$\Rightarrow$1 follows by definition. For the implication
1$\Rightarrow$2 suppose, by assumption, $L(A)=L(B)$ for a total always
resetting ${\textsf{\sc dta}_{k}}$ $B$. Every left quotient $w^{-1}L(A)$
equals $L_{B}(c)$ for some configuration $c$, hence Point 2 follows by Fact
17. Here we use the fact that $B$ is always resetting in order to apply the
second part of Fact 17; without the assumption, we would only have
$S$-invariance for sets $S$ of size at most $k+1$.

It thus remains to prove the implication 2$\Rightarrow$3, which will be the
content of the rest of the section. Assuming Point 2, we are going to define
an always resetting ${\textsf{\sc dta}_{k,m}}$ $B^{\prime}$ with clocks
$\mathtt{X}=\\{\mathtt{x}_{1},\dots,\mathtt{x}_{k}\\}$ and with at most
$f(k,m,n)$ locations such that $L(B^{\prime})=L(A)$. We start from the timed
transition system $\mathcal{X}$ obtained by the finite powerset construction
underlying the determinisation of $A$, and then transform this transition
system gradually, while preserving its language, until it finally becomes
isomorphic to the reachable part of $\left\llbracket
B^{\prime}\right\rrbracket$ for some ${\textsf{\sc dta}_{k,m}}$ $B^{\prime}$.
As the last step we extract from this deterministic timed transition system a
syntactic definition of $B^{\prime}$ and prove equality of their languages.
This is achieved thanks to the invariance properties of the transition systems
in the course of the transformation.

##### Macro-configurations.

Configurations of the ${\textsf{\sc nta}_{1}}$ $A$ are of the form
$c=(p,u,t_{0})$ where $u,t_{0}\in{\mathbb{R}}_{\geq 0}$ and $u\leq t_{0}$. A
_macro-configuration_ is a (not necessarily finite) set $X$ of configurations
$(p,u,t_{0})$ of $A$ which share the same value of the current timestamp
$t_{0}$, which we denote as $\text{\sc now}(X)=t_{0}$. We use the notation
$L_{A}(X):=\bigcup_{c\in X}L_{A}(c)$. Let $\text{\sc
succ}_{\sigma,t}(X):=\\{c^{\prime}\in\left\llbracket
A\right\rrbracket\;|\;c\xrightarrow{\sigma,t}c^{\prime}\text{ for some }c\in
X\\}$ be the set of successors of configurations in $X$. We define a
deterministic timed transition system $\mathcal{X}$ consisting of the macro-
configurations reachable in the course of determinisation of $A$. Let
$\mathcal{X}$ be the smallest set of macro-configurations and transitions such
that

  * •

$\mathcal{X}$ contains the initial macro-configuration:
$X_{0}=\\{(p,0,0)\;|\;p\in\mathtt{L}_{I}\\}\in\mathcal{X}$;

  * •

$\mathcal{X}$ is closed under successor: for every $X\in\mathcal{X}$ and
$(\sigma,t)\in\Sigma\times{\mathbb{R}}_{\geq 0}$, there is a transition
$X\xrightarrow{\sigma,t}\text{\sc succ}_{a,t}(X)$ in $\mathcal{X}$.

Due to the fact that $\left\llbracket A\right\rrbracket$ is finitely
branching, i.e. $\text{\sc succ}_{\sigma,t}(\\{c\\})$ is finite for every
fixed $(\sigma,t)$, all macro-configurations $X\in\mathcal{X}$ are finite. Let
the final configurations of $\mathcal{X}$ be
$F_{\mathcal{X}}=\\{X\in\mathcal{X}\;|\;X\cap F\neq\emptyset\\}$.
$L_{A}(X)=L_{\mathcal{X}}(X)$ for every $X\in\mathcal{X}$. In particular
$L(A)=L_{\mathcal{X}}(X_{0})$. For a macro-configuration $X$ we write
$\text{\sc Val}(X):=\\{u\;|\;(p,u,\text{\sc now}(X))\in X\\}\cup\\{\text{\sc
now}(X)\\}$ to denote the reals appearing in $X$. Since $A$ is greedily
resetting, every macro-configuration $X\in\mathcal{X}$ satisfies $\text{\sc
Val}(X)\subseteq(\text{\sc now}(X)-m,\text{\sc now}(X)]$. Whenever a macro-
configuration $X$ satisfies this condition we say that _the span of $X$ is
bounded by $m$_.

##### Pre-states.

By assumption (Point 2), $L_{A}(X)$ is $S$-invariant for some $S$ of size at
most $k$, but the macro-configuration $X$ itself needs not be $S$-invariant in
general. Indeed, a finite macro-configuration $X\in\mathcal{X}$ is
$S$-invariant if, and only if, $\mathsf{fract}({\text{\sc
Val}(X)})\subseteq\mathsf{fract}({S})$, which is impossible in general when
$X$ is arbitrarily large, its span is bounded (by $m$), and size of $S$ is
bounded (by $k$). Intuitively, in order to assure $S$-invariance we will
replace $X$ by its $S$-closure $\textrm{Cl}_{S}(X)$ (recall Fact 7).

A set $S\subseteq{\mathbb{R}}_{\geq 0}$ is _fraction-independent_ if it
contains no two reals with the same fractional part. A _pre-state_ is a pair
$Y=(X,S)$, where $X$ is an $S$-invariant macro-state, and $S$ is a finite
fraction-independent subset of $\text{\sc Val}(X)$ that contains $\text{\sc
now}(X)$. The intuitive rationale behind assuming the $S$-invariance of $X$ is
that it implies, together with the bounded span of $X$ and the bounded size of
$S$, that there are only finitely many pre-states, up to timed automorphism.
We define the deterministic timed transition system $\mathcal{Y}$ as the
smallest set of pre-states and transitions between them such that:

  * •

$\mathcal{Y}$ contains the initial pre-state:
$Y_{0}=(X_{0},\\{0\\})\in\mathcal{Y}$;

  * •

$\mathcal{Y}$ is closed under the closure of successor: for every
$(X,S)\in\mathcal{Y}$ and $(\sigma,t)\in\Sigma\times{\mathbb{R}}_{\geq 0}$,
there is a transition $(X,S)\xrightarrow{\sigma,t}(X^{\prime},S^{\prime})$,
where $S^{\prime}$ is the least, with respect to set inclusion, subset of
$S\cup\\{t\\}$ containing $t$ such that the language
$L^{\prime}=(\sigma,t)^{-1}L_{A}(X)=L_{A}(\text{\sc succ}_{\sigma,t}(X))$ is
$S^{\prime}$-invariant, and $X^{\prime}=\textrm{Cl}_{S^{\prime}}(\text{\sc
succ}_{\sigma,t}(X))$.

Observe that the least such fraction-independent subset $S^{\prime}$ exists
due to the following facts: by fraction-independence of $S$ there is a unique
fraction-independent subset $\widetilde{S}\subseteq S\cup\\{t\\}$ which
satisfies $\mathsf{fract}({\widetilde{S}})=\mathsf{fract}({S\cup\\{t\\}})$
($\widetilde{S}$ is obtained by removing from $S$ any element $u$ such that
$\mathsf{fract}({u})=\mathsf{fract}({t})$, if any); since $X$ is
$S$-invariant, due to Fact 16 so it is its language $L_{A}(X)$, and hence
$L^{\prime}$ is necessarily $\widetilde{S}$-invariant; by assumption (Point
2), $L^{\prime}$ is $R$-invariant for some set $R\subseteq{\mathbb{R}}_{\geq
0}$ of size at most $k$ containing $t$; let $T\subseteq[0,1)$ be the least set
of fractional values given by Corollary 19 applied to $L^{\prime}$, i.e.,
$T\subseteq\mathsf{fract}({\widetilde{S}})\cap\mathsf{fract}({R})$; finally
let $S^{\prime}\subseteq\widetilde{S}$ be chosen so that
$\mathsf{fract}({S^{\prime}})=T\cup\mathsf{fract}({\\{t\\}})$. Due to
fraction-independence of $\widetilde{S}$ the choice is unique and $S^{\prime}$
is fraction-independent. Furthermore, $t\in S^{\prime}$ and the size of
$S^{\prime}$ is at most $k$.

Suppose $k=3$, $m=2$, $\text{\sc
succ}_{\sigma,t}(X)=\\{(p,3.7,5),(q,3.9,5),(r,4.2,5)\\}$ and
$S^{\prime}=\\{3.7,4.2,5\\}$. Then
$X^{\prime}=\\{(p,3.7,5)\\}\cup\\{(q,t,5)\mid
t\in(3.7,4.2)\\}\cup\\{(r,4.2,5)\\}$. $\text{\sc now}(X^{\prime})=5$. A
corresponding _state_ (as defined below) is $(X^{\prime},\mu^{\prime})$, where
$\mu^{\prime}=\\{\mathtt{x}_{1}\mapsto 3.7,\mathtt{x}_{2}\mapsto
4.2,\mathtt{x}_{3}\mapsto 5\\}$.

By Fact 16, we deduce: [Invariance of $\mathcal{Y}$] For every two transitions

$(X_{1},S_{1})\xrightarrow{\sigma,t_{1}}(X^{\prime}_{1},S^{\prime}_{1})\qquad\text{and}\qquad(X_{2},S_{2})\xrightarrow{\sigma,t_{2}}(X^{\prime}_{2},S^{\prime}_{2})$

in $\mathcal{Y}$ and a timed permutation $\pi$, if $\pi(X_{1})=X_{2}$ and
$\pi(S_{1})=S_{2}$ and $\pi(t_{1})=t_{2}$, then we have
$\pi(X^{\prime}_{1})=X^{\prime}_{2}$ and $\pi(S^{\prime}_{1})=S^{\prime}_{2}$.

######  Proof 7.3.

Let $i$ range over $\\{1,2\\}$ and let $\widetilde{X}_{i}:=\text{\sc
succ}_{a,t_{i}}(X_{i})$. Thus $S^{\prime}_{i}$ is the least subset of
$S_{i}\cup\\{t_{i}\\}$ containing $t_{i}$ such that $L_{A}(\widetilde{X}_{i})$
is $S^{\prime}_{i}$-invariant, and
$X^{\prime}_{i}=\textrm{Cl}_{S^{\prime}_{i}}(\widetilde{X}_{i})$. By
invariance of $\left\llbracket A\right\rrbracket$ (Fact 15) and invariance of
semantics (Fact 16) we get

$\pi(\widetilde{X}_{1})=\widetilde{X}_{2},\qquad\text{ and
}\qquad\pi(L_{A}(\widetilde{X}_{1}))=L_{A}(\widetilde{X}_{2}),$

and therefore $\pi(S^{\prime}_{1})=S^{\prime}_{2}$, which implies
$\pi(X^{\prime}_{1})=X^{\prime}_{2}$.

Let the final configurations of $\mathcal{Y}$ be
$F_{\mathcal{Y}}=\\{(X,S)\in\mathcal{Y}\;|\;X\cap\mathtt{L}_{F}\neq\emptyset\\}$.
By induction on the length of timed words it is easy to show:
$L_{\mathcal{X}}(X_{0})=L_{\mathcal{Y}}(Y_{0})$. Due to the assumption that
$A$ is greedily resetting and due to Point 2, in every pre-state
$(X,S)\in\mathcal{Y}$ the span of $X$ is bounded by $m$ and the size of $S$ is
bounded by $k$.

##### States.

We now introduce _states_ , which are designed to be in one-to-one
correspondence with configurations of the forthcoming ${\textsf{\sc dta}_{k}}$
$B^{\prime}$. Intuitively, a state differs from a pre-state $(X,S)$ only by
allocating the values from $S$ into $k$ clocks, thus while a pre-state
contains a set $S$, the corresponding state contains a reset-point assignment
$\mu:\mathtt{X}\to{\mathbb{R}}_{\geq 0}$ with image $\mu(\mathtt{X})=S$.

Let $\mathtt{X}=\\{\mathtt{x}_{1},\dots,\mathtt{x}_{k}\\}$ be a set of $k$
clocks. A _state_ is a pair $Z=(X,\mu)$, where $X$ is a macro-configuration,
$\mu:\mathtt{X}\to\text{\sc Val}(X)$ is a reset-point assignment,
$\mu(\mathtt{X})$ is a fraction-independent set containing $\text{\sc
now}(X)$, and $X$ is $\mu(\mathtt{X})$-invariant. Thus every state $Z=(X,\mu)$
determines uniquely a corresponding pre-state $\rho(Z)=(X,S)$ with
$S=\mu(\mathtt{X})$. We define the deterministic timed transition system
$\mathcal{Z}$ consisting of those states $Z$ s.t. $\rho(Z)\in\mathcal{Y}$, and
of transitions determined as follows:
$(X,\mu)\xrightarrow{\sigma,t}(X^{\prime},\mu^{\prime})$ if the corresponding
pre-state has a transition
$(X,S)\xrightarrow{\sigma,t}(X^{\prime},S^{\prime})$ in $\mathcal{Y}$, where
$S=\mu(\mathtt{X})$, and

$\displaystyle\mu^{\prime}(\mathtt{x}_{i})\ :=\ \begin{cases}t&\text{ if
}\mu(\mathtt{x}_{i})\notin S^{\prime}\text{ or
}\mu(\mathtt{x}_{i})=\mu(\mathtt{x}_{j})\text{ for some }j>i\\\
\mu(\mathtt{x}_{i})&\text{otherwise.}\end{cases}$ (9)

Intuitively, the equation (9) defines a deterministic update of the reset-
point assignment $\mu$ that amounts to resetting
($\mu^{\prime}(\mathtt{x}_{i}):=t$) all clocks $\mathtt{x}_{i}$ whose value is
either no longer needed (because $\mu(\mathtt{x}_{i})\notin S^{\prime}$), or
is shared with some other clock $x_{j}$, for $j>i$ and is thus redundant. Due
to this disciplined elimination of redundancy, knowing that $t\in S^{\prime}$
and the size of $S^{\prime}$ is at most $k$, we ensure that at least one clock
is reset in every step. In consequence, $\mu^{\prime}(\mathtt{X})=S^{\prime}$,
and the forthcoming ${\textsf{\sc dta}_{k}}$ $B^{\prime}$ will be always
resetting. Using Claim 7.1 we derive: [Invariance of $\mathcal{Z}$] For every
two transitions

$(X_{1},\mu_{1})\xrightarrow{\sigma,t_{1}}(X^{\prime}_{1},\mu^{\prime}_{1})\qquad\text{and}\qquad(X_{2},\mu_{2})\xrightarrow{\sigma,t_{2}}(X^{\prime}_{2},\mu^{\prime}_{2})$

in $\mathcal{Z}$ and a timed permutation $\pi$, if $\pi(X_{1})=X_{2}$ and
$\pi{\circ}{\mu_{1}}=\mu_{2}$ and $\pi(t_{1})=t_{2}$, then we have
$\pi(X^{\prime}_{1})=X^{\prime}_{2}$ and
$\pi{\circ}{\mu^{\prime}_{1}}=\mu^{\prime}_{2}$.

######  Proof 7.4.

Let $i$ range over $\\{1,2\\}$. Let $S_{i}=\mu_{i}(\mathtt{X})$ and
$(X_{i},S_{i})\xrightarrow{a,t_{i}}(X^{\prime}_{i},S^{\prime}_{i})$ in
$\mathcal{Y}$. By Claim 7.1 we have

$\pi(X^{\prime}_{1})=X^{\prime}_{2}\qquad\text{ and
}\pi(S^{\prime}_{1})=S^{\prime}_{2}.$

Since $\pi{\circ}{\mu_{1}}=\mu_{2}$ and the definition (9) is invariant:

$\pi{\circ}(\mu^{\prime})=(\pi{\circ}{\mu})^{\prime},$

we derive $\pi{\circ}{\mu^{\prime}_{1}}=\mu^{\prime}_{2}$.

Let the initial state be $Z_{0}=(X_{0},\mu_{0})$, where
$\mu_{0}(\mathtt{x}_{i})=0$ for all $\mathtt{x}_{i}\in\mathtt{X}$, and let the
final states be $F_{\mathcal{Z}}=\\{(X,\mu)\in\mathcal{Z}\;|\;X\cap
F\neq\emptyset\\}$. By induction on the length of timed words one proves:
$L_{\mathcal{Y}}(Y_{0})=L_{\mathcal{Z}}(Z_{0})$. In the sequel we restrict
$\mathcal{Z}$ to states reachable from $Z_{0}$. In every state $Z=(X,\mu)$ in
$\mathcal{Z}$, we have $\text{\sc now}(X)\in\mu(\mathtt{X})$. This will ensure
the resulting ${\textsf{\sc dta}_{k}}$ $B^{\prime}$ to be always resetting.

##### Orbits of states.

While a state is designed to correspond to a configuration of the forthcoming
${\textsf{\sc dta}_{k}}$ $B^{\prime}$, its orbit is designed to play the rôle
of control location of $B^{\prime}$. We therefore need to prove that the set
of states in $\mathcal{Z}$ is orbit-finite, i.e., the set of orbits
$\\{\text{\sc orbit}(Z)\;|\;Z\in\mathcal{Z}\\}$ is finite and its size is
bounded by $f(k,m,n)$. We start by deducing an analogue of Fact 20: For two
states $Z=(X,\mu)$ and $Z^{\prime}=(X^{\prime},\mu^{\prime})$ in
$\mathcal{Z}$, their reset-point assignments are in the same orbit, i.e.,
$\pi{\circ}\mu=\mu^{\prime}$ for some $\pi\in\Pi$, if, and only if, the
corresponding clock valuations ${\text{\sc now}(X)}-{\mu}$ and ${\text{\sc
now}(X^{\prime})}-{\mu^{\prime}}$ belong to the same $k,m$-region. (In passing
note that, since in every state $(X,\mu)$ in $\mathcal{Z}$ the span of $X$ is
bounded by $m$, only bounded $k,m$-regions can appear in the last claim.
Moreover, in each $k,m$-region one of the clocks constantly equals $0$.) The
action of timed automorphisms on macro-configurations and reset-point
assignments is extended to states as $\pi(X,\mu)=(\pi(X),\pi{\circ}\mu)$.
Recall that the orbit of a state $Z$ is defined as $\text{\sc
orbit}(Z)=\\{\pi(Z)\;|\;\pi\in\Pi\\}$. The number of orbits of states in
$\mathcal{Z}$ is bounded by $f(k,m,n)$.

######  Proof 7.5.

We finitely represent a state $Z=(X,\mu)$, relying on the following general
fact.

######  Fact 24.

For every $u\in{\mathbb{R}}_{\geq 0}$ and $S\subseteq{\mathbb{R}}_{\geq 0}$,
the $S$-orbit777The orbits of states $Z$ should not be confused with
$S$-orbits of individual reals $u\in{\mathbb{R}}_{\geq 0}$. $\text{\sc
orbit}_{S}(u)$ is either the singleton $\\{u\\}$ (when $u\in S$) or an open
interval with end-points of the form $t+z$ where $t\in S$ and $z\in\mathbb{Z}$
(when $u\notin S$).

We apply the fact above to $S=\mu(\mathtt{X})$. In our case the span of $X$ is
bounded by $m$, and thus the same holds for $\mu(\mathtt{X})$. Consequently,
the integer $z$ in the fact above always belongs to $\\{-m,-m{+}1,\dots,m\\}$.
In turn, $X$ splits into disjoint $\mu(\mathtt{X})$-orbits $\text{\sc
orbit}_{\mu(\mathtt{X})}(u)$ consisting of open intervals separated by
endpoints of the form $t+z$ where $t\in\mu(\mathtt{X})$ and
$z\in\\{-m,-m{+}1,\dots,m\\}$.

Continuing Example 7.1, the endpoints are $\\{3,3.2,3.7,4,4.2,4.7,5\\}$, as
shown in the illustration:

Recall that $\mu(\mathtt{X})$ is fraction-independent. Let
$e_{1}<e_{2}<\dots<e_{l+1}$ be all the endpoints of open-interval orbits
($l\leq km$), and let $o_{1},o_{2},o_{3},\dots\ :=\
\\{e_{1}\\},(e_{1},e_{2}),\\{e_{2}\\},\dots$ be the consecutive $S$-orbits
$\text{\sc orbit}_{\mu(\mathtt{X})}(u)$ of elements $u\in\mu(\mathtt{X})$. The
number thereof is $2l+1\leq 2km+1$. The finite representation of $Z=(X,\mu)$
consists of the pair $(O,\mu)$, where

$\displaystyle O=\\{(o_{1},P_{1}),\dots,(o_{2l+1},P_{2l+1})\\}$ (10)

assigns to each orbit $o_{i}$ the set of locations
$P_{i}=\\{p\;|\;(p,u,t_{0})\in X\text{ for some }u\in
o_{i}\\}\subseteq\mathtt{L},$ (which is the same as
$P_{i}=\\{p\;|\;(p,u,t_{0})\in X\text{ for all }u\in o_{i}\\}$ since $X$ is
$\mu(\mathtt{X})$-invariant, and hence $\mu(\mathtt{X})$-closed). Thus a state
$Z=(X,\mu)$ is uniquely determined by the sequence $O$ as in (10) and the
reset-point assignment $\mu$.

We claim that the set of all the finite representations $(O,\mu)$, as defined
above, is orbit-finite. Indeed, the orbit of $(O,\mu)$ is determined by the
orbit of $\mu$ and the sequence

$\displaystyle P_{1},\ P_{2},\ \ldots,\ P_{2km+1}$ (11)

induced by the assignment $O$ as in (10). Therefore, the number of orbits is
bounded by the number of orbits of $\mu$ (which is bounded, due to Claim 7.1,
by $\textsf{Reg}(k,m)$) times the number of different sequences of the form
(11) (which is bounded by $(2^{n})^{2km+1}$). This yields the required bound
$f(k,m,n)=\textsf{Reg}(k,m)\cdot 2^{n(2km+1)}$.

##### Construction of the dta.

As the last step we define a ${\textsf{\sc dta}_{k}}$
$B^{\prime}=(\Sigma,\mathtt{L}^{\prime},\mathtt{X},\\{o_{0}\\},\mathtt{L}_{F}^{\prime},\Delta^{\prime})$
such that the reachable part of $\left\llbracket B^{\prime}\right\rrbracket$
is isomorphic to $\mathcal{Z}$. Let locations
$\mathtt{L}^{\prime}=\\{\text{\sc orbit}(Z)\;|\;Z\in\mathcal{Z}\\}$ be orbits
of states from $\mathcal{Z}$, the initial location be the orbit $o_{0}$ of
$Z_{0}$, and final locations $\mathtt{L}_{F}^{\prime}=\\{\text{\sc
orbit}(Z)\;|\;Z\in F_{\mathcal{Z}}\\}$ be orbits of final states. A transition
$Z=(X,\mu)\xrightarrow{\sigma,t}(X^{\prime},\mu^{\prime})=Z^{\prime}$ in
$\mathcal{Z}$ induces a transition rule in $B^{\prime}$

$\displaystyle(o,a,\psi,\mathtt{Y},o^{\prime})\in\Delta^{\prime}$ (12)

whenever $o=\text{\sc orbit}(Z)$, $o^{\prime}=\text{\sc orbit}(Z^{\prime})$,
$\psi$ is the unique $k,m$-region satisfying
${t}-{\mu}\in\left\llbracket\psi\right\rrbracket$, and
$\mathtt{Y}=\\{\mathtt{x}_{i}\in\mathtt{X}\;|\;\mu^{\prime}(\mathtt{x}_{i})=t\\}$.
The automaton $B^{\prime}$ is indeed a dta since $o$, $\sigma$ and $\psi$
uniquely determine $\mathtt{Y}$ and $o^{\prime}$: Suppose that two transitions
$(X_{1},\mu_{1})\xrightarrow{\sigma,t_{1}}(X^{\prime}_{1},\mu^{\prime}_{1})$
and
$(X_{2},\mu_{2})\xrightarrow{\sigma,t_{2}}(X^{\prime}_{2},\mu^{\prime}_{2})$
in $\mathcal{Z}$ induce transition rules
$(o,\sigma,\psi,\mathtt{Y}_{1},o^{\prime}_{1}),(o,\sigma,\psi,\mathtt{Y}_{2},o^{\prime}_{2})\in\Delta^{\prime}$
with the same source location $o$ and constraint $\psi$, i.e,

$\displaystyle{t_{1}}-{\mu_{1}}\in\left\llbracket\psi\right\rrbracket\qquad{t_{2}}-{\mu_{2}}\in\left\llbracket\psi\right\rrbracket.$
(13)

Then the target locations are equal $o^{\prime}_{1}=o^{\prime}_{2}$, and the
same for the reset sets $\mathtt{Y}_{1}=\mathtt{Y}_{2}$. (Notice that we only
consider two transition rules with the same constraint $\psi$, instead of two
different jointly satisfiable constraints $\psi,\psi^{\prime}$ as in the
definition of deterministic timed automata, due to the fact that each
constraint of $B^{\prime}$ is a single $k,m$-region.)

######  Proof 7.6.

We use the invariance of semantics of $A$ and Claim 7.1. Let $o=\text{\sc
orbit}(X_{1},\mu_{1})=\text{\sc orbit}(X_{2},\mu_{2})$. Thus there is a timed
automorphism $\pi$ such that

$\displaystyle X_{2}=\pi(X_{1})\qquad\mu_{2}=\pi{\circ}\mu_{1}.$ (14)

It suffices to show that there is a (possibly different) timed permutation
$\pi^{\prime}$ satisfying the following equalities:

$\displaystyle
t_{2}=\pi^{\prime}(t_{1})\quad\\{i\;|\;\mu^{\prime}_{1}(\mathtt{x}_{i})=t_{1}\\}=\\{i\;|\;\mu^{\prime}_{2}(\mathtt{x}_{i})=t_{2}\\}\quad\mu^{\prime}_{2}=\pi^{\prime}{\circ}\mu^{\prime}_{1}\quad
X^{\prime}_{2}=\pi^{\prime}(X^{\prime}_{1}).$ (15)

We now rely the fact that both ${t_{0}}_{1}=\text{\sc
now}(X_{1})\in\mu_{1}(\mathtt{X})$ and ${t_{0}}_{2}=\text{\sc
now}(X_{2})\in\mu_{2}(\mathtt{X})$ are assigned to the same clock due to the
second equality in (14): ${t_{0}}_{1}=\mu_{1}(\mathtt{x}_{i})$ and
${t_{0}}_{2}=\mu_{2}(\mathtt{x}_{i})$. We focus on the case when
$t_{1}-{t_{0}}_{1}\leq m$ (the other case is similar and easier since all
clocks are reset due to greedy resetting), which implies
$t_{2}-{t_{0}}_{2}\leq m$ due to (13). In this case we may assume w.l.o.g.,
due to (13) and the equalities (14), that $\pi$ is chosen so that
$\pi(t_{1})=t_{2}$. We thus take $\pi^{\prime}=\pi$ for proving the equalities
(15). Being done with the first equality, we observe that the last two
equalities in (15) hold due to the invariance of $\mathcal{Z}$ (c.f. Claim
7.1). The remaining second equality in (15) is a consequence of the third one.

Let $Z=(X,\mu)$ and $Z^{\prime}=(X^{\prime},\mu)$ be two states in
$\mathcal{Z}$ with the same reset-point assignment. If $\pi(X)=X^{\prime}$ and
$\pi{\circ}\mu=\mu$ for some timed automorphism $\pi$ then $X=X^{\prime}$.
$\mathcal{Z}$ is isomorphic to the reachable part of $\left\llbracket
B^{\prime}\right\rrbracket$.

######  Proof 7.7.

We essentially repeat the argument of Claim 4.1. For a state $Z=(X,\mu)$, let
$\iota(Z)=(o,\mu,t)$, where $o=\text{\sc orbit}(Z)$ and $t=\text{\sc now}(X)$.
Let $\mathcal{Z}^{\prime}$ denote the reachable part of $\left\llbracket
B^{\prime}\right\rrbracket$. By Claim 4.1, the mapping $\iota(\\_)$ is a
bijection between $\mathcal{Z}$ and its image
$\iota(\mathcal{Z})\subseteq\left\llbracket B^{\prime}\right\rrbracket$. We
aim at proving $\iota(\mathcal{Z})=\mathcal{Z}^{\prime}$.

By the very definition (6), the image $\iota(\mathcal{Z})$ is a subsystem of
$\mathcal{Z}^{\prime}$. Recall that $\mathcal{Z}$ is total: for every
$(\sigma_{1},t_{1})\dots(\sigma_{n},t_{n})\in\mathbb{T}(\Sigma)$, there is a
sequence of transitions
$(X_{0},\mu_{0})\xrightarrow{\sigma_{1},t_{1}}\cdots\xrightarrow{\sigma_{n},t_{n}}$
in $\mathcal{Z}$. Therefore $\iota(\mathcal{Z})$ is total too and, since
$\mathcal{Z}^{\prime}$ is deterministic and reachable, the subsystem
$\iota(\mathcal{Z})$ necessarily equals $\mathcal{Z}^{\prime}$.

Claims 7.1, 7.1, 7.1, and 7.1 imply $L(A)=L(B^{\prime})$, which completes the
proof of Lemma 21.

##  8\. Undecidability and hardness

In this section we complete the decidability and complexity landscape for the
deterministic membership problem by providing matching undecidability and
complexity hardness results, both for register and timed automata.

###  8.1. Lossy counter machines

Our undecidability and hardness results will be obtained by reducing from the
finiteness problem for lossy counter machines, which is known to be
undecidable. A _$k$ -counters lossy counter machine_ ($k$-LCM) is a tuple
$M=(C,Q,q_{0},\Delta)$, where $C=\\{c_{1},\dots,c_{k}\\}$ is a set of $k$
counters, $Q$ is a finite set of control locations, $q_{0}\in Q$ is the
initial control location, and $\Delta$ is a finite set of instructions of the
form $(p,\mathtt{op},q)$, where $\mathtt{op}$ is one of $c\,\texttt{++}$,
$c\,\texttt{-{}-}$, and $c\stackrel{{\scriptstyle?}}{{\texttt{=}}}0$. A
configuration of an LCM $M$ is a pair $(p,u)$, where $p\in Q$ is a control
location, and $u\in\mathbb{N}^{C}$ is a counter valuation. For two counter
valuations $u,v\in\mathbb{N}^{C}$, we write $u\leq v$ if $u(c)\leq v(c)$ for
every counter $c\in C$. The semantics of an LCM $M$ is given by a (potentially
infinite) transition system over the configurations of $M$ s.t. there is a
transition $(p,u)\xrightarrow{\delta}(q,v)$, for
$\delta=(p,\mathtt{op},q)\in\Delta$, whenever

  1. (1)

$\mathtt{op}=c\,\texttt{++}$ and $v\leq u[c\mapsto u(c)+1]$, or

  2. (2)

$\mathtt{op}=c\,\texttt{-{}-}$ and $v\leq u[c\mapsto u(c)-1]$, or

  3. (3)

$\mathtt{op}=c\stackrel{{\scriptstyle?}}{{\texttt{=}}}0$ and $u(c)=0$ and
$v\leq u$.

We omit $\delta$ in $\xrightarrow{\delta}$ when it is irrelevant, and write
$\xrightarrow{}^{*}$ for the transitive closure of $\xrightarrow{}$. The
_finiteness problem_ (a.k.a. space boundedness) for an LCM $M$ amounts to
deciding whether the reachability set
$\text{Reach}(M)=\\{(p,u)\;|\;(q_{0},u_{0})\xrightarrow{}^{*}(p,u)\\}$ is
finite, where $u_{0}$ is the constantly $0$ counter valuation. [[May03,
Theorem 13]] The $4$-LCM finiteness problem is undecidable.

###  8.2. Register automata

####  8.2.1. Undecidability of dra membership for ${\textsf{\sc nra}_{1}}$

We show that it is undecidable whether a ${\textsf{\sc nra}_{1}}$ language can
be recognised by some dra . In the following, it will be useful to be able to
refer to projection of a data word on the finite component of the alphabet. To
this end, for a data word
$w=(\sigma_{0},a_{0})\cdots(\sigma_{n},a_{n})\in(\Sigma\times\mathbb{A})^{*}$,
let $\mathsf{undata}(w)=\sigma_{0}\cdots\sigma_{n}\in\Sigma^{*}$ be the word
obtained by removing the atom component. As already announced, we reduce from
the finiteness problem for lossy counter machines. Consider a lossy counter
machine $M=(C,Q,q_{0},\Delta)$ with $4$ counters
$C=\\{c_{1},c_{2},c_{3},c_{4}\\}$. We use the following encoding of LCM runs
as data words over the alphabet $\Sigma=Q\cup\Delta\cup C$ comprising the
control locations, transitions, and counters of $M$. (A similar encoding has
been used in the proof of Theorem 5.2 in [DL09] to show that the universality
problem for ${\textsf{\sc nra}_{1}}$ is not primitive recursive.) We encode a
counter valuation $u\in\mathbb{N}^{C}$ as the word over $C\subseteq\Sigma$

$\displaystyle\mathsf{enc}(u)\;=\;\underbrace{c_{1}c_{1}\cdots
c_{1}}_{u(c_{1})\text{ letters}}\ \underbrace{c_{2}c_{2}\cdots
c_{2}}_{u(c_{2})\text{ letters}}\ \underbrace{c_{3}c_{3}\cdots
c_{3}}_{u(c_{3})\text{ letters}}\ \underbrace{c_{4}c_{4}\cdots
c_{4}}_{u(c_{4})\text{
letters}}\in\\{c_{1}\\}^{*}\\{c_{2}\\}^{*}\\{c_{3}\\}^{*}\\{c_{4}\\}^{*}.$
(16)

Consider a LCM run

$\displaystyle\pi\;=\;(p_{0},u_{0})\xrightarrow{\delta_{1}}(p_{1},u_{1})\xrightarrow{\delta_{2}}\cdots\xrightarrow{\delta_{n}}(p_{n},u_{n}).$

The set $\mathsf{Enc}(\pi)\subseteq(\Sigma\times\mathbb{A})^{*}$ of _reversal-
encodings_ of $\pi$ contains all data words $w\in(\Sigma\times\mathbb{A})^{*}$
satisfying the following conditions:

  1. (E1)

the finite part of $w$ is of the form

$\displaystyle\mathsf{undata}(w)=p_{n}\delta_{n}\mathsf{enc}(u_{n})\quad\cdots\quad
p_{1}\delta_{1}\mathsf{enc}(u_{1})\quad
p_{0}\mathsf{enc}(u_{0})\in\Sigma^{*};$ (17)

  2. (E2)

all atoms appearing in a single $\mathsf{enc}(u_{i})$ block are distinct;

  3. (E3)

for every transition $\delta_{i}=(p_{i-1},\mathtt{op}_{i},p_{i})$ and for
every counter $c_{j}\in\\{c_{1},c_{2},c_{3},c_{4}\\}$:

    1. (E3.1)

if $\mathtt{op}_{i}=c_{j}\,\texttt{++}$ increments counter $c_{j}$, then
(recalling that the lossy semantics amounts to $u_{i}(c_{j})-1\leq
u_{i-1}(c_{j})$) we require that for each occurrence of $c_{j}$ in
$\mathsf{enc}(u_{i})$ there is a matching occurrence of $c_{j}$ in
$\mathsf{enc}(u_{i-1})$ with the same atom, with the exception of the _last_
occurrence of $c_{j}$ in $\mathsf{enc}(u_{i})$;

    2. (E3.2)

if $\mathtt{op}_{i}=c_{j}\,\texttt{-{}-}$ decrements counter $c_{j}$, then
(recalling that the lossy semantics amounts to $u_{i}(c_{j})+1\leq
u_{i-1}(c_{j})$) we require that for each occurrence of $c_{j}$ in
$\mathsf{enc}(u_{i})$ there is a matching occurrence of $c_{j}$ in
$\mathsf{enc}(u_{i-1})$ with the same atom, which is _not the last_ occurrence
of $c_{j}$ in $\mathsf{enc}(u_{i-1})$.

    3. (E3.3)

if $\mathtt{op}_{i}=c_{j}\stackrel{{\scriptstyle?}}{{\texttt{=}}}0$ tests
whether counter $c_{j}$ is zero, then $u_{i-1}(c_{j})=u_{i}(c_{j})=0$, and
thus we require that neither $\mathsf{enc}(u_{i})$ nor $\mathsf{enc}(u_{i-1})$
contain any occurrence of $c_{j}$;

    4. (E3.4)

otherwise the operation $\mathtt{op}_{i}$ does not modify counter $c_{j}$,
i.e., $u_{i}(c_{j})\leq u_{i-1}(c_{j})$, and we require that for each
occurrence of $c_{j}$ in $\mathsf{enc}(u_{i})$ there is a matching occurrence
of $c_{j}$ in $\mathsf{enc}(u_{i-1})$ with the same atom.

The intuition underlying the first two items in condition (E3) is that the
effect of an increment or decrement of $c_{j}$ is encoded by creating or
removing _the last_ occurrence of $c_{j}$ in a block.

Let $L=\bigcup_{\pi\text{ a run of }M}\mathsf{Enc}(\pi)$ be the set of all
reversal-encodings of runs of $M$. Under this encoding, we can build a
${\textsf{\sc nra}_{1}}$ $A$ recognising the _complement_ of $L$. Indeed, $A$
can determine bad encodings $w\not\in L$ by guessing one of finitely many
reasons for this to occur:

  1. (F1)

the projection $\mathsf{undata}(\mathsf{enc}(\pi))$ to the finite alphabet
$\Sigma$ is not a word in the regular language
$(Q\Delta\\{c_{1}\\}^{*}\\{c_{2}\\}^{*}\\{c_{3}\\}^{*}\\{c_{4}\\}^{*})^{*}\\{q_{0}\\}$
(notice that $\mathsf{enc}(u_{0})$ is the empty string, since the initial
valuation $u_{0}$ assigns $0$ to every counter), or there is a transition
$\delta_{i}=(p,\\_,q)$ s.t. either the source is incorrect $p\neq p_{i-1}$ or
the destination is incorrect $q\neq p_{i}$. This is even a regular language of
finite words over $\Sigma$ (i.e., without atoms). Thus in the remaining cases
below we can assume that the finite part of $w$ is of the form as in (17);

  2. (F2)

there is a block $\mathsf{enc}(u_{i})$ containing the same atom twice;

  3. (F3)

there is a transition $\delta_{i}=(p_{i-1},\mathtt{op}_{i},p_{i})$ and a
counter $c_{j}\in\\{c_{1},c_{2},c_{3},c_{4}\\}$ s.t. one of the following
condition holds:

    1. (F3.1)

$\mathtt{op}=c_{j}\,\texttt{++}$ but there is a non-last occurrence of $c_{j}$
in $\mathsf{enc}(u_{i})$ without matching occurrence of $c_{j}$ in
$\mathsf{enc}(u_{i-1})$ with the same atom;

    2. (F3.2)

$\mathtt{op}=c_{j}\,\texttt{-{}-}$ but some occurrence of $c_{j}$ in
$\mathsf{enc}(u_{i})$ either has no matching occurrence of $c_{j}$ in
$\mathsf{enc}(u_{i-1})$ with the same atom, or has a matching occurrence which
is the last occurrence of $c_{j}$ in $\mathsf{enc}(u_{i-1})$.

    3. (F3.3)

$\mathtt{op}=c_{j}\stackrel{{\scriptstyle?}}{{\texttt{=}}}0$ but either
$\mathsf{enc}(u_{i})$ or $\mathsf{enc}(u_{i-1})$ contains an occurrence of
$c_{j}$;

    4. (F3.4)

the operation $\mathtt{op}$ does not modify counter $c_{j}$, but there is an
occurrence of $c_{j}$ in $\mathsf{enc}(u_{i})$ without a matching occurrence
of $c_{j}$ in $\mathsf{enc}(u_{i-1})$ with the same atom.

One register is sufficient to recognise each of the possible mistakes above.

######  Lemma 25.

The set of reachable configurations $\text{Reach}(M)$ is finite if, and only
if, $L(A)$ is a dra language.

######  Proof 8.1.

The “only if” implication follows from the fact that if $\text{Reach}(M)$ is
finite, i.e., there is a finite bound $k$ on the sum of values of all counters
of $M$ in a run, then the complement of $L(A)$ (which encodes all correct
reversal-encodings) is a ${\textsf{\sc dra}_{k}}$ language, and thus $L(A)$
itself is a dra language since dra languages are closed under complement. For
the “if” implication, assume that $\text{Reach}(M)$ is infinite, and by way of
contradiction assume that $L(A)$ is a dra language. In this case, the
complement $L$ of $L(A)$ is recognised by some ${\textsf{\sc dra}_{k}}$ $B$
with a finite number of registers $k$. Since $\text{Reach}(M)$ is infinite,
there are runs where counter (say) $c_{1}$ is unbounded. In particular, there
is a run $\pi$ reaching a counter valuation $u_{i}$ with $u_{i}(c_{1})\geq
k+2$. When $B$ reads the corresponding encoding $w\in\mathsf{Enc}(\pi)$, after
reading the first $k+1$ atoms $a_{1},\dots,a_{k+1}$ in the
$\mathsf{enc}(u_{i})$ block, it must forget at least one such atom, say
$a_{j}$. The next atom $a_{k+2}$ in the $\mathsf{enc}(u_{i})$ block can thus
be replaced by $a_{j}$ and $B$ still accepts the corresponding data word
$w^{\prime}$. However, $w^{\prime}$ is not the reversal encoding of any run of
$M$, since it violates condition (E2). This contradicts that $B$ recognises
$L$, and thus $L(A)$ is not a dra language, as required.

We thus have a reduction from the LCM finiteness problem to the dra membership
problem for ${\textsf{\sc nra}_{1}}$, which is thus undecidable thanks to
Section 8.1.

######  Corollary 26.

The dra membership problem for ${\textsf{\sc nra}_{1}}$ languages is
undecidable.

####  8.2.2. Undecidability and hardness for ${\textsf{\sc dra}_{k}}$
membership

The _nra universality problem_ asks whether a given nra $A$ recognises every
data word $L(A)=(\Sigma\times\mathbb{A})^{*}$. All the lower bounds in this
section leading to undecidability and hardness results for the ${\textsf{\sc
dra}_{k}}$ membership problem are obtained by a reduction from the
universality problem for corresponding classes of data languages.

######  Lemma 27 (c.f. [Fin06, Theorem 1]).

Let $k\in\mathbb{N}$ and let $\mathcal{Y}$ be a class of invariant data
languages that

  1. (1)

contains all the ${\textsf{\sc dra}_{0}}$ languages,

  2. (2)

is closed under union and concatenation, and

  3. (3)

contains some non-${\textsf{\sc dra}_{k}}$ language.

The universality problem for data languages in $\mathcal{Y}$ reduces in
polynomial time to the ${\textsf{\sc dra}_{k}}$ membership problem for data
languages in $\mathcal{Y}$.

######  Proof 8.2.

Let $L\in\mathcal{Y}$ be a data language over a finite alphabet $\Sigma$. We
show that universality of $L$ reduces to ${\textsf{\sc dra}_{k}}$ membership.
Thanks to the last assumption, let $M\in\mathcal{Y}$ be a data language over
some finite alphabet $\Gamma$ which is not recognised by any ${\textsf{\sc
dra}_{k}}$. Consider the following language over the extended alphabet
$\Sigma^{\prime}=\Sigma\cup\Gamma\cup\\{\$\\}$:

$\displaystyle N\ :=\
L\cdot(\\{\$\\}\times\mathbb{A})\cdot(\Gamma\times\mathbb{A})^{*}\,\cup\,(\Gamma\times\mathbb{A})^{*}\cdot(\\{\$\\}\times\mathbb{A})\cdot
M,$

where $\$\not\in\Sigma\cup\Gamma$ is a fixed fresh alphabet symbol. Since
$\mathcal{Y}$ contains the universal language, by its closure properties the
language $N$ belongs to $\mathcal{Y}$. We conclude by proving the following
equivalence:

$\displaystyle L=(\Sigma\times\mathbb{A})^{*}\quad\text{if, and only if,
}\quad\text{$N$ is recognised by a ${\textsf{\sc dra}_{k}}$.}$

For the “only if” direction, if $L$ is universal, then
$N=(\Sigma\times\mathbb{A})^{*}\cdot(\\{\$\\}\times\mathbb{A})\cdot(\Sigma\times\mathbb{A})^{*}$
is clearly recognised by a ${\textsf{\sc dra}_{k}}$. For the “if” direction
suppose, towards reaching a contradiction, that $N$ is recognised by a
${\textsf{\sc dra}_{k}}$ $A$ but $L$ is not universal. Choose an arbitrary
data word $w\not\in L$ over $\Sigma$ and consider an arbitrary extension
$u=w\cdot(\$,a)$ of $w$ by one letter. Since $\$$ does not belong to the
finite alphabet $\Sigma\cup\Gamma$, the left quotient $u^{-1}N=\\{v\;|\;uv\in
N\\}$ equals $M$. Let $(p,\mu)$ be the configuration reached by $A$ after
reading $u$, which thus recognises $L(p,\mu)=M$. Since $M$ is invariant as a
language in $\mathcal{Y}$, $M$ is a ${\textsf{\sc dra}_{k}}$ language, which
is a contradiction.

From Lemma 27 we immediately obtain the undecidability and hardness results
for the ${\textsf{\sc dra}_{k}}$ membership problem, which we now recall.

See 6

######  Proof 8.3.

For the first point, consider the class $\mathcal{Y}$ consisting of all the
${\textsf{\sc nra}_{2}}$ languages. Clearly this class contains all
${\textsf{\sc dra}_{0}}$ languages and it is closed under union and
concatenation. Thanks to Example 3 we know that there are ${\textsf{\sc
nra}_{1}}$ (and thus ${\textsf{\sc nra}_{2}}$) languages which are not dra
languages. Thus the conditions of Lemma 27 are satisfied and the universality
problem for ${\textsf{\sc nra}_{2}}$ reduces in polynomial time to the
${\textsf{\sc dra}_{k}}$ membership problem for ${\textsf{\sc nra}_{2}}$.
Since the former problem is undecidable [DL09, Theorem 5.4], undecidability of
the latter one follows. For the other two points we can proceed in an
analogous way, by using the fact that the universality problem is undecidable
for ${\textsf{\sc nra}_{1}^{\mathrm{g}}}$ (${\textsf{\sc nra}_{1}}$ with
guessing) [Boj, Exercise 9], and not primitive recursive for ${\textsf{\sc
nra}_{1}}$ [DL09, Theorem 5.2].

###  8.3. Timed automata

We now focus on timed automata. Following similar lines as in case of register
automata in Section 8.2, in Section 8.3.1 we prove undecidability of the dta
membership problem for ${\textsf{\sc nta}_{1}}$ (c.f. Theorem 3) and in
Section 8.3.2 we prove HyperAckermann-hardness of the ${\textsf{\sc dta}_{k}}$
membership problem for ${\textsf{\sc nta}_{1}}$ (c.f. Theorem 5).

####  8.3.1. Undecidability of dta and ${\textsf{\sc
dta}_{\textnormal{\\_},m}}$ membership for ${\textsf{\sc nta}_{1}}$

It has been shown in [Fin06, Theorem 1] that it is undecidable whether a
${\textsf{\sc nta}_{2}}$ timed language can be recognised by some dta . This
was obtained by a reduction from the ${\textsf{\sc nta}_{2}}$ universality
problem, which is undecidable. While the universality problem becomes
decidable for $k=1$, we show in this section that, as announced in Theorem 3,
the dta membership problem remains undecidable for ${\textsf{\sc nta}_{1}}$.

Since the universality problem for ${\textsf{\sc nta}_{1}}$ is decidable, we
need to reduce from another (undecidable) problem. As in the case of register
automata, we reduce from the finiteness problem of a LCM $M$ with 4 counters,
which is undecidable by Section 8.1. In the case of timed automata, we can use
the reversal encoding from [LW08, Definition 4.6] showing that we can build a
${\textsf{\sc nta}_{1}}$ $A$ recognising the _complement_ of the set of
reversal-encodings of the runs of $M$. Since this construction has already
been presented in full details in [CLP20c, App. C] and since it is in complete
analogy to the construction in Section 8.2.1 for register automata, we omit it
here. One can then prove the following property, which is analogous to Lemma
25 in the case of register automata.