Effective Definability of the Reachability Relation in Timed Automata

TL;DR

This paper presents a new proof demonstrating that the reachability relation in timed automata can be defined using linear arithmetic, simplifying understanding and analysis of such systems.

Contribution

The paper provides a novel proof of the definability of the reachability relation in timed automata within linear arithmetic, building on prior work.

Findings

Reachability relation is definable in linear arithmetic

New proof simplifies previous understanding

Supports automated analysis of timed automata

Abstract

We give a new proof of the result of Comon and Jurski that the binary reachability relation of a timed automaton is definable in linear arithmetic.

Equations

$$\phi ::=\text{true}\mid x<k\mid x=k\mid x>k\mid \phi \wedge \phi ,$$

$$Z[\lambda \leftarrow 0]$$

$$\overrightarrow{Z}$$

$$⟹\subseteq (L\times {\mathbb{R}}_{\ge 0}^{\mathcal{X}})\times \mathbb{R}\times (L\times {\mathbb{R}}_{\ge 0}^{\mathcal{X}})$$

$${\phi }_{{\ell }_0,\ell }^{\mathcal{A}}(\mathbf{x},\mathbf{y}):=\exists {\mathbf{x}}^{\prime }\exists z.(\mathbf{x}={\mathbf{x}}^{\prime }-z1\wedge {\psi }_{{\ell }_0^{\prime },\ell }^{\mathcal{B}}(\mathbf{y},{\mathbf{x}}^{\prime },z)).$$

$$Q=L\times {\mathbb{N}}^{\mathcal{X}}\times {\mathcal{Z}}_1(\mathcal{X})\times 2^{\mathcal{X}}.$$

$$⟨{\ell }_0,{\upsilon }^{(0)},Z_0,{\gamma }_0⟩⟶⟨{\ell }_1,{\upsilon }^{(1)},Z_1,{\gamma }_1⟩⟶\dots ⟶⟨{\ell }_k,{\upsilon }^{(k)},Z_k,{\gamma }_k⟩$$

$$⟨{\ell }_0,{\upsilon }^{(0)}+{\nu }^{(0)}⟩⟹⟨{\ell }_1,{\upsilon }^{(1)}+{\nu }^{(1)}⟩⟹\dots ⟹⟨{\ell }_k,{\upsilon }^{(k)}+{\nu }^{(k)}⟩.$$

$$⟨{\ell }_{j-1},{\upsilon }^{(j-1)},Z_{j-1},{\gamma }_{j-1}⟩⟶⟨{\ell }_j,{\upsilon }^{(j)},Z_j,{\gamma }_j⟩.$$

$$⟨{\ell }_{j-1},{\upsilon }^{(j-1)}+{\nu }^{(j-1)}⟩\stackrel{d}{⟹}⟨{\ell }_j,{\upsilon }^{(j)}+{\nu }^{(j)}⟩.$$

$$⟨{\ell }_{j-1},{\upsilon }^{(j-1)}+{\nu }^{(j-1)}⟩=⟨{\ell }_j,{\upsilon }^{(j)}+{\nu }^{(j)}⟩.$$

$$⟨{\ell }_{j-1},{\upsilon }^{(j-1)}+{\nu }^{(j-1)}⟩\stackrel{0}{⟹}⟨{\ell }_j,{\upsilon }^{(j)}+{\nu }^{(j)}⟩.$$

$$⟨{\ell }_0,{\nu }^{(0)}⟩\stackrel{d_1}{⟹}⟨{\ell }_1,{\nu }^{(1)}⟩\stackrel{d_2}{⟹}\dots \stackrel{d_k}{⟹}⟨{\ell }_k,{\nu }^{(k)}⟩$$

$$\left\{\upsilon \in {\mathbb{N}}^{\mathcal{X}}:\exists w\in {\mathcal{X}}^{\ast }\cdot ⟨{\ell }_0,0,\{0\},\gamma ⟩\stackrel{w}{⟶}⟨\ell ,\upsilon ,Z,\varnothing ⟩\right\}$$

$$L_{\mathrm{wrap}}:=\left\{w\in {\mathcal{X}}^{\ast }:\exists \upsilon \in {\mathbb{N}}^{\mathcal{X}}\cdot ⟨{\ell }_0,0,\{0\},\gamma ⟩\stackrel{w}{⟶}⟨\ell ,\upsilon ,Z,\varnothing ⟩\right\}.$$

$$\left\{\nu \in {\mathbb{R}}_{\ge 0}^{\mathcal{X}}:⟨{\ell }_0,0⟩{⟹}^{\ast }⟨\ell ,\nu ⟩\right\}=\bigcup _{Z\in {\mathcal{Z}}_1(\mathcal{X})}\bigcup _{\gamma \subseteq \mathcal{X}}\left\{\upsilon +Z:⟨{\ell }_0,0,\{0\},\gamma ⟩{⟶}^{\ast }⟨\ell ,\upsilon ,Z,\varnothing ⟩\right\}$$

Full text

1 Introduction

Comon and Jurski [6, 7] showed that the binary reachability relation of a given timed automaton is effectively definable by a first-order formula of linear arithmetic over the reals augmented with a unary predicate denoting the integers. The proof of this result, given in [7], is based on a syntactic transformation of arbitrary timed automata into equivalent timed automata satisfying a certain structural restriction, called flatness. The proof is relatively long and technical (running to over 40 pages) and there have been a number of subsequent attempts to both generalise the result and simplify its proof [5, 8, 9, 10]. The present note is a development of [10, Sections III and IV] and further simplifies the proof of Comon and Jurski’s result therein. In particular, we avoid many technicalities of [10] by employing a simple “clock memorisation” trick to reduce computation of the binary reachability relation of a timed automaton to computation of the set of configurations reachable from a given location starting with the all-zeros clock valuation. We show how to recover the latter set of configurations as the commutative image of a certain regular language accepted by a variant of Alur and Dill’s region automaton (cf. [1]).

2 Definitions and Main Result

Given a set $\mathcal{X}=\{x_{1},\ldots,x_{n}\}$ of clocks, the set $\Phi(\mathcal{X})$ of clock constraints is generated by the grammar

[TABLE]

where $k\in\mathbb{N}$ and $x\in\mathcal{X}$. A clock valuation is a mapping $\nu:\mathcal{X}\to\mathbb{R}_{\geq 0}$, where $\mathbb{R}_{\geq 0}$ is the set of non-negative real numbers. Denote by $\mathbb{R}_{\geq 0}^{\mathcal{X}}$ the set of all clock valuations. We write $\nu\models\varphi$ to denote that $\nu\in\mathbb{R}_{\geq 0}^{\mathcal{X}}$ satisfies the constraint $\varphi$. We denote by $\boldsymbol{0}$ the valuation such that $\boldsymbol{0}(x)=0$ for all $x\in\mathcal{X}$. Given $t\in\mathbb{R}_{\geq 0}$, we let $\nu+t$ be the clock valuation such that $(\nu+t)(x)=\nu(x)+t$ for all clocks $x\in\mathcal{X}$. Given $\lambda\subseteq\mathcal{X}$, let $\nu[\lambda\leftarrow 0]$ be the clock valuation such that $\nu[\lambda\leftarrow 0](x)=0$ if $x\in\lambda$, and $\nu[\lambda\leftarrow 0](x)=\nu(x)$ if $x\not\in\lambda$.

A 1-bounded zone $Z\subseteq[0,1]^{\mathcal{X}}$ is a set of clock valuations that is defined by a conjunction of difference constraints $x_{i}\sim c$ and $x_{i}-x_{j}\sim c$, where $c\in\{-1,0,+1\}$, ${\sim}\in\{<,=\}$, $i,j\in\{1,\ldots,n\}$. We write $\mathcal{Z}_{1}(\mathcal{X})$ for the set of 1-bounded zones. Given a 1-bounded zone $Z$ and $\lambda\subseteq\mathcal{X}$, the following are also 1-bounded zones (see, e.g., [4]):

[TABLE]

A timed automaton is a tuple $\mathcal{A}=\langle L,\mathcal{X},E\rangle$, where $L$ is a finite set of locations, $\mathcal{X}$ is a finite set of clocks, and $E\subseteq L\times\Phi(\mathcal{X})\times 2^{\mathcal{X}}\times L$ is the set of edges. A configuration of $\mathcal{A}$ is a pair $\langle\ell,\nu\rangle$ consisting of a location $\ell$ and a clock valuation $\nu$. Such a timed automaton $\mathcal{A}$ induces a ternary transition relation

[TABLE]

on the set of configurations as follows. Given configurations $\langle\ell,\nu\rangle$ and $\langle\ell^{\prime},\nu^{\prime}\rangle$, we postulate:

• •

a delay transition $\langle\ell,\nu\rangle\stackrel{{\scriptstyle d}}{{\Longrightarrow}}\langle\ell^{\prime},\nu^{\prime}\rangle$ for some $d\geq 0$, if $\nu^{\prime}=\nu+d$ and $\ell=\ell^{\prime}$;

• •

a discrete transition $\langle\ell,\nu\rangle\stackrel{{\scriptstyle 0}}{{\Longrightarrow}}\langle\ell^{\prime},\nu^{\prime}\rangle$, if there is an edge $\langle\ell,\varphi,\lambda,\ell^{\prime}\rangle$ of $\mathcal{A}$ such that $\nu\models\varphi$ and $\nu^{\prime}=\nu[\lambda\leftarrow 0]$.

A run $q_{0}\stackrel{{\scriptstyle d_{1}}}{{\Longrightarrow}}q_{1}\stackrel{{\scriptstyle d_{2}}}{{\Longrightarrow}}q_{2}\stackrel{{\scriptstyle d_{3}}}{{\Longrightarrow}}\ldots\stackrel{{\scriptstyle d_{m}}}{{\Longrightarrow}}q_{m}$ of $\mathcal{A}$ is a finite sequence of delay and discrete transitions.

Let $\mathcal{L}$ denote the set of first-order formulas over the structure $\mathcal{R}=(\mathbb{R},\mathbb{Z}(\cdot),0,1,+,\leq)$, where $\mathbb{R}$ is the universe and $\mathbb{Z}(\cdot)$ is a unary predicate denoting the set of integers. We call $\mathcal{L}$ the language of mixed linear arithmetic. This language subsumes both Presburger arithmetic (linear arithmetic over $\mathbb{Z}$) and linear arithmetic over $\mathbb{R}$. It is shown in [3, Section 3] how to rewrite a given $\mathcal{L}$-sentence in polynomial time into an equivalent Boolean formula whose atoms are either sentences of real linear arithmetic or sentences of Presburger arithmetic. From known complexity bounds for the latter two theories [2], it follows that deciding the truth of $\mathcal{L}$-sentences can be carried out by an alternating Turing machine running in time $2^{2^{O(n)}}$ with $n$ alternations (i.e., the same complexity as Presburger arithmetic).

The main contribution of the present paper is to prove the following result.

Theorem 1**.**

Given a timed automaton $\mathcal{A}$ with $n$ clock variables and locations $\ell_{0},\ell$ of $\mathcal{A}$, we can compute an $\mathcal{L}$-formula $\varphi^{\mathcal{A}}_{\ell_{0},\ell}(x_{1},\ldots,x_{n},y_{1},\ldots,y_{n})$ such that there is a run of $\mathcal{A}$ from configuration $\langle\ell_{0},\nu_{0}\rangle$ to configuration $\langle\ell,\nu\rangle$ iff $\mathcal{R}\models\varphi^{\mathcal{A}}_{\ell_{0},\ell}[\nu_{0},\nu]$.

3 Proofs

3.1 Clock Memorisation

We describe a simple trick that reduces the problem of computing the binary reachability relation on a given timed automaton $\mathcal{A}$ to that of computing the set of configurations reachable from a fixed initial configuration in a derived automaton $\mathcal{B}$. The idea is that $\mathcal{B}$ starts from the zero clock valuation, guesses an initial clock valuation $\nu_{0}$ of $\mathcal{A}$, and then simulates a computation of $\mathcal{A}$ while “remembering” $\nu_{0}$ as a set of differences between the values of some fresh clocks. Formally we derive Theorem 1 from the following result, which we prove later on.

Proposition 2**.**

Given a timed automaton $\mathcal{A}$ with $n$ clocks and locations $\ell_{0},\ell$ of $\mathcal{A}$, we can compute an $\mathcal{L}$-formula $\psi^{\mathcal{A}}_{\ell_{0},\ell}(x_{1},\ldots,x_{n})$ such that there is a run in $\mathcal{A}$ from $\langle\ell_{0},\boldsymbol{0}\rangle$ to $\langle\ell,\nu\rangle$ if and only if $\mathcal{R}\models\psi^{\mathcal{A}}_{\ell_{0},\ell}[\nu]$.

Proof of Theorem 1.

Given a timed automaton $\mathcal{A}=\langle L,\mathcal{X},E\rangle$ with a distinguished location $\ell_{0}\in L$, we define a new timed automaton $\mathcal{B}=\langle L^{\prime},\mathcal{X}^{\prime},E^{\prime}\rangle$ as follows. The set of locations is $L^{\prime}=L\cup\{\ell^{\prime}_{0}\}$, where $\ell^{\prime}_{0}\not\in L$ is a distinguished location in $\mathcal{B}$. The set of clocks is $\mathcal{X}^{\prime}=\{x,x^{\prime}:x\in\mathcal{X}\}\cup\{z\}$, where $z\not\in\mathcal{X}$, that is, $\mathcal{B}$ has two copies of each clock of $\mathcal{A}$ plus an extra “reference clock” $z$. We obtain $E^{\prime}$ by adding the following edges to $E$: for each $x\in\mathcal{X}$ we have an edge $\langle\ell^{\prime}_{0},\mathbf{true},\{x,x^{\prime}\},\ell^{\prime}_{0}\rangle$ in $E^{\prime}$ (that is, a selfloop on $\ell^{\prime}_{0}$ that resets both copies of clock $x$); we also have a single additional edge $\langle\ell^{\prime}_{0},\mathbf{true},\{z\},\ell_{0}\rangle$ in $E^{\prime}$. Notice that once $\mathcal{B}$ leaves $\ell^{\prime}_{0}$ then neither the reference clock $z$ nor any clock in the set $\{x^{\prime}\mid x\in\mathcal{X}\}$ is reset—intuitively when $\mathcal{B}$ exits $\ell^{\prime}_{0}$, the value of clock $x\in\mathcal{X}$ is stored in the difference of $x^{\prime}$ and $z$.

Observe that for all $\ell\in L$ there is a run from $\langle\ell_{0},\nu_{0}\rangle$ to $\langle\ell,\nu\rangle$ in $\mathcal{A}$ if and only if there is a run in $\mathcal{B}$ from $\langle\ell^{\prime}_{0},\boldsymbol{0}\rangle$ to $\langle\ell,\nu^{\prime}\rangle$ such that $\nu^{\prime}(x)=\nu(x)$ and $\nu^{\prime}(x^{\prime})-\nu^{\prime}(z)=\nu_{0}(x)$ for all $x\in\mathcal{X}$. In particular, a run of $\mathcal{A}$ from $\langle\ell_{0},\nu_{0}\rangle$ to $\langle\ell,\nu\rangle$ can be simulated in $\mathcal{B}$ as follows. Automaton $\mathcal{B}$ starts in configuration $\langle\ell_{0}^{\prime},\boldsymbol{0}\rangle$; by taking selfloops on $\ell_{0}^{\prime}$ and then the edge $\langle\ell^{\prime}_{0},\mathbf{true},\{z\},\ell_{0}\rangle$, $\mathcal{B}$ may reach a configuration $\langle\ell_{0},\nu^{\prime\prime}\rangle$ such that $\nu^{\prime\prime}(x)=\nu^{\prime\prime}(x^{\prime})=\nu_{0}(x)$ for all $x\in\mathcal{X}$, and $\nu^{\prime\prime}(z)=0$; then $\mathcal{B}$ directly simulates the given run of $\mathcal{A}$ (without resetting the new clocks $x^{\prime}$, $x\in\mathcal{X}$, and $z$).

Let $\psi^{\mathcal{B}}_{\ell^{\prime}_{0},\ell}(\boldsymbol{x},\boldsymbol{x}^{\prime},z)$ be the formula obtained in Proposition 2 for automaton $\mathcal{B}$. Then we define

[TABLE]

∎

3.2 A Discrete-Time Automaton

Given a timed automaton $\mathcal{A}=\langle L,\mathcal{X},E\rangle$, we define an (untimed, infinite-state) nondeterministic automaton $R(\mathcal{A})$. The set of states of $R(\mathcal{A})$ is

[TABLE]

Given a state $\langle\ell,\upsilon,Z,\gamma\rangle\in Q$, intuitively $\upsilon$ and $Z$ respectively encode the integer and fractional parts of the clocks of $\mathcal{A}$, while $\gamma\subseteq\mathcal{X}$ is a “prophecy variable” denoting the set of clocks that will be reset at least once in the future. The alphabet of $R(\mathcal{A})$ is ${\mathcal{X}}$ and the set of transitions (which includes $\varepsilon$-transitions) is as follows:

For each state $\langle\ell,\upsilon,Z,\gamma\rangle\in Q$ there is a delay transition $\langle\ell,\upsilon,Z,\gamma\rangle\stackrel{{\scriptstyle\varepsilon}}{{\longrightarrow}}\langle\ell,\upsilon,\overrightarrow{Z},\gamma\rangle$. 2. 2.

For each clock $x\in\mathcal{X}$ and state $\langle\ell,\upsilon,Z,\gamma\rangle$ of $R(\mathcal{A})$ there is a wrapping transition $\langle\ell,\upsilon,Z,\gamma\rangle\stackrel{{\scriptstyle\sigma}}{{\longrightarrow}}\langle\ell,\upsilon^{\prime},Z^{\prime},\gamma\rangle$ where $Z^{\prime}:=(Z\cap[\![x=1]\!])[x\leftarrow 0]$, $\upsilon^{\prime}=\upsilon[x\leftarrow x+1]$, and $\sigma=\varepsilon$ if $x\in\gamma$ but otherwise $\sigma=x$. (Intuitively a wrapping transition for clock $x$ has label $\varepsilon$ if $x\in\gamma$ since $x$ will be reset again in the future.) 3. 3.

Each edge $\langle\ell,\varphi,\lambda,\ell^{\prime}\rangle$ of $\mathcal{A}$ yields a transition $\langle\ell,\upsilon,Z,\gamma\rangle\stackrel{{\scriptstyle\varepsilon}}{{\longrightarrow}}\langle\ell^{\prime},\upsilon^{\prime},Z^{\prime},\gamma^{\prime}\rangle$ of $R(\mathcal{A})$, where $\upsilon^{\prime}=\upsilon[\lambda\leftarrow 0]$, $Z^{\prime}:=\{\nu\in Z:\upsilon+\nu\models\varphi\}[\lambda\leftarrow 0]$, and $\gamma^{\prime}\cup\lambda=\gamma$. (Intuitively, $\gamma^{\prime}$ is obtained from $\gamma$ by guessing some clocks that will not be reset again and removing them from $\gamma$.)

Given states $q,q^{\prime}\in Q$, we write $q\stackrel{{\scriptstyle w}}{{\longrightarrow}}q^{\prime}$ if there is a run in $R(\mathcal{A})$ from $q$ to $q^{\prime}$ on word $w\in\mathcal{X}^{*}$. We furthermore write $q\longrightarrow^{*}q^{\prime}$ if there exists a run from $q$ to $q^{\prime}$.

Proposition 3**.**

Automaton $\mathcal{A}$ has a run from $\langle\ell_{0},\boldsymbol{0}\rangle$ to $\langle\ell,\nu\rangle$ along which the set of clocks that are reset is $\gamma\subseteq\mathcal{X}$ if and only if $R(\mathcal{A})$ has a run from $\langle\ell_{0},\boldsymbol{0},\{\boldsymbol{0}\},\gamma\rangle$ to $\langle\ell,\upsilon,Z,\emptyset\rangle$ for some $\upsilon\in\mathbb{N}^{\mathcal{X}}$ and $Z\in\mathcal{Z}_{1}(\mathcal{X})$ such that $\nu-\upsilon\in Z$.

Proof.

For the “if” direction, suppose that

[TABLE]

is a run of $R(\mathcal{A})$ with $\upsilon^{(0)}=\boldsymbol{0}$, $Z_{0}=\{\boldsymbol{0}\}$, and $\gamma_{0}=\gamma$. Given any valuation $\nu^{(k)}\in Z_{k}$, we construct a sequence of valuations $\nu^{(0)}\in Z_{0},\ldots,\nu^{(k-1)}\in Z_{k-1}$ such that $\mathcal{A}$ has a run

[TABLE]

The construction of $\nu^{(j)}$ is by backward induction on $j$. The base step, valuation $\nu^{(k)}$, is given. The induction step divides into three cases according to the type of the transition

[TABLE]

• •

Delay transition. We have $Z_{j}=\overrightarrow{Z_{j-1}}$, $\ell_{j}=\ell_{j-1}$, and $\upsilon^{(j)}=\upsilon^{(j-1)}$. Thus we can pick $\nu^{(j-1)}\in{Z_{j-1}}$ such that $\nu^{(j)}=\nu^{(j-1)}+d$ for some $d\geq 0$. Hence there is in $\mathcal{A}$ a delay transition

[TABLE]

• •

Wrapping transition. We have $Z_{j}=(Z_{j-1}\cap[\![x=1]\!])[x\leftarrow 0]$ for some clock $x\in\mathcal{X}$. Thus we can pick $\nu^{(j-1)}\in{Z_{j-1}\cap[\![x=1]\!]}$ such that $\nu^{(j)}=\nu^{(j-1)}[x\leftarrow 0]$. In this case we have

[TABLE]

• •

Discrete transition. Let the corresponding edge of $\mathcal{A}$ be $\langle\ell_{j-1},\varphi,\lambda,\ell_{j}\rangle$. Then we have $\upsilon^{(j)}=\upsilon^{(j-1)}[\lambda\leftarrow 0]$ and $Z_{j}=\{\nu\in Z_{j-1}:\nu+\upsilon^{(j-1)}\models\varphi\}[\lambda\leftarrow 0]$. Choose $\nu^{(j-1)}\in Z_{j-1}$ such that $\nu+\upsilon^{(j)}\models\varphi$ and $\nu^{(j)}=\nu^{(j-1)}[\lambda\leftarrow 0]$. Then there is in $\mathcal{A}$ a discrete transition

[TABLE]

We now turn to the “only-if” direction of the proof. Suppose that we have a run

[TABLE]

of $\mathcal{A}$, where $\nu^{(0)}=\boldsymbol{0}$. We first transform such a run, while keeping the same initial and final configurations, by decomposing each delay step into a sequence of shorter delays, so that for all $0\leq j\leq k-1$ and all $x\in\mathcal{X}$ the open interval $(\nu^{(j)}(x),\nu^{(j+1)}(x))$ contains no integer. In other words, we break every delay step at every point at which some clock crosses an integer boundary. We thus obtain a corresponding run of $R(\mathcal{A})$ that starts from state $\langle\ell_{0},\upsilon^{(0)},Z_{0},\gamma_{0}\rangle$, where $Z_{0}=\{\boldsymbol{0}\}$, $\upsilon^{(0)}=\boldsymbol{0}$, and ends in state $\langle\ell_{k},\upsilon^{(k)},Z_{k},\emptyset\rangle$ such that $\nu^{(k)}\in\upsilon^{(k)}+Z_{k}$.

We build such a run of $R(\mathcal{A})$ by forward induction. In particular, we construct a sequence of intermediate states $\langle\ell_{i},\upsilon^{(i)},Z_{i},\gamma_{i}\rangle$, $0\leq i\leq k$, such that $\nu^{(i)}\in\upsilon^{(i)}+Z_{i}$ for each such $i$. Each discrete transition of $\mathcal{A}$ is simulated by a discrete transition of $R(\mathcal{A})$. A delay transition of $\mathcal{A}$ that ends with set of clocks $\lambda\subseteq\mathcal{X}$ being integer valued is simulated by a delay transition of $R(\mathcal{A})$, followed by wrapping transitions for all $x\in\lambda$. ∎

Proposition 4**.**

Let $\mathcal{A}=\langle L,\mathcal{X},E\rangle$ be a timed automaton with distinguished locations $\ell_{0},\ell\in L$. For every $Z\in\mathcal{Z}_{1}(\mathcal{X})$ and $\gamma\subseteq\mathcal{X}$ the set

[TABLE]

is effectively semilinear.

Proof.

Consider the following language of “wrapping transitions” in $R(\mathcal{A})$:

[TABLE]

Define the function $\pi:\mathcal{X}^{*}\rightarrow\mathbb{N}^{\mathcal{X}}$ such that $\pi(w)(x)$ is the number of occurrences of letter $x$ in word $w$. Since visible transitions of $R(\mathcal{A})$ correspond to wrapping transitions of clocks that will not be reset any more, the commutative image $\pi(L_{\mathrm{wrap}})$ is precisely the set of vectors defined in (1).

We claim that $L_{\mathrm{wrap}}$ is regular, which suffices to show that the set (1) is semilinear. Indeed, denote by $c_{\max}$ the largest constant appearing in a transition constraint in $\mathcal{A}$, and consider the equivalence relation on states of $R(\mathcal{A})$ defined by $(\ell,\upsilon,Z,\gamma)\sim(\ell,\upsilon^{\prime},Z,\gamma)$ iff for all $x\in\mathcal{X}$ either $\upsilon(x)=\upsilon^{\prime}(x)$ or $\upsilon(x),\upsilon^{\prime}(x)\geq c_{\max}$. Clearly if $(\ell,\upsilon,Z,\gamma)\sim(\ell,\upsilon^{\prime},Z,\gamma)$ then for all $\nu\in Z$ and clock constraints $\varphi$ appearing in $\mathcal{A}$ we have that $\upsilon+\nu\models\varphi$ iff $\upsilon^{\prime}+\nu\models\varphi$. It follows that $\sim$ is a strong bisimulation (that moreover has finite index). Taking the quotient of $R(\mathcal{A})$ by $\sim$ it follows that $L_{\mathrm{wrap}}$ is accepted by a finite automaton and hence is regular. ∎

Proof of Proposition 2.

By Proposition 3 we have that

[TABLE]

But by Proposition 4 the right-hand expression above is definable by an $\mathcal{L}$-formula in the sense of Proposition 2. ∎

4 Computational Complexity

In this section we briefly retrace the proof of Theorem 1 in order to give a complexity bound for computing the $\mathcal{L}$-formula $\varphi_{\ell_{0},\ell}$ described therein. We sketch a proof that $\varphi_{\ell_{0},\ell}$ is an existential formula that can be computed in time polynomial in the number of locations of the timed automaton and exponential in the number of clocks and bit length of the maximum clock constant.

Working backwards, we start by considering the regular language $L_{\mathrm{wrap}}$ in the proof of Proposition 4. From the bound $|\mathcal{Z}_{1}(\mathcal{X})|\leq(2|\mathcal{X}|+1)!\leq 2^{O(|\mathcal{X}|\log|\mathcal{X}|)}$ it is straightforward that there is a finite automaton accepting language $L_{\mathrm{wrap}}$ with number of states bounded by $\mathrm{poly}(|L|,c_{\max},2^{|\mathcal{X}|\log|\mathcal{X}|})$ (where $L$ and $\mathcal{X}$ are as in the statement of Proposition 4) and moreover this automaton can be computed in time polynomial in its size.

Lin [11] shows that the Parikh image of the language of an NFA with $m$ states and alphabet size $k$ is described by a quantifier-free formula of Presburger arithmetic that can be computed in time $2^{O(k^{2}\log m)}$. We may thus refine the statement of Proposition 4 by specifying that the subset of $\mathbb{N}^{\mathcal{X}}$ in Equation (1) is described by a quantifier-free formula of Presburger arithmetic that can be computed in time bounded by $\mathrm{poly}(|L|,c_{\max},2^{|\mathcal{X}|^{2}})$.

Moving now to the proof of Proposition 2, we see that the formula $\psi_{\ell_{0},\ell}$ can likewise be computed in time bounded by $\mathrm{poly}(|L|,c_{\max},2^{|\mathcal{X}|^{2}})$. Constructing formula $\psi_{\ell_{0},\ell}$ from the Presburger-arithmetic formula referred to in Proposition 4 requires to introduce existentially quantified variables to denote the fractional parts of the clock values of the source and target configurations; but $\psi_{\ell_{0},\ell}$ is otherwise quantifier-free.

Finally, recall that the formula $\varphi_{\ell_{0},\ell}$ in Theorem 1 was obtained from the formula $\psi_{\ell_{0},\ell}$ in Proposition 2 with only a polynomial blow up that introduced extra existentially quantified variables.