*timed transition system* $[[A]] = (S, s_0, {\mathbb{R}_{\geq 0}}, {\Sigma}, T)$, where:

1.  $S = \{(q,v) \in {\mathcal{Q}}\times {\mathcal{V}}\}$ is the set of states, with $s_0 = (q_0, {\textbf{0}})$ the initial state;

2.  $T \subseteq S \times ({\Sigma}\cup {\mathbb{R}_{\geq 0}}) \times S$ is the transition relation. The set $T$ consists of

    1.  *Timed transitions (delays):* $(q,v) \xrightarrow{d} (q, v+d)$, where $d \in {\mathbb{R}_{\geq 0}}$;

    2.  *Discrete transitions (jumps):* $(q,v) \xrightarrow{a} (q',v')$, where $a \in {\Sigma}$ and there exists a transition $(q, a, g, {\mathcal{C}_{rst}}, q')$ in ${\mathcal{T}}$, such that the valuation $v$ satisfies the guard $g$ and $v' = v[{\mathcal{C}_{rst}}]$.

A (finite) *run* $\varrho$ on $A \in {\mathrm{eNTA}}$ is a sequence of alternating timed and discrete transitions of the form $$(q_{0}, {\textbf{0}}) \xrightarrow{d_{1}} (q_{0}, \textbf{d}_1) \xrightarrow{a_{1}} (q_{1}, v_{1}) \xrightarrow{d_{2}} \cdots 
\xrightarrow{d_{k}} (q_{k-1}, v_{k-1} + d_{k}) \xrightarrow{a_{k}} (q_{k}, v_{k}).$$ The run $\varrho$ on $A$ induces the *timed trace* (*timed word*) $$\tau = (t_{1}, a_{1}), (t_{2}, a_{2}), \ldots, (t_{k}, a_{k}),$$ with $a_i \in {\Sigma}$ and $t_{i} = \Sigma_{j=1}^{i} d_i$. The language ${\mathfrak{L}}(A)$ consists of the set of timed traces that are obtained from the runs that end in accepting locations. We remark that for simplification of presentation we did not include the 