is a finite set of locations and $q_0 \in {\mathcal{Q}}$ is the initial location;

2.  ${\mathcal{F}}\subseteq {\mathcal{Q}}$ is the set of accepting locations;

3.  ${\Sigma}$ is a finite set of transition labels, called actions;

4.  ${\mathcal{C}}$ is a finite set of clock variables;

5.  ${\mathcal{T}}\subseteq {\mathcal{Q}}\times {\Sigma}\times {\mathcal{G}}\times {\mathcal P \left({{\mathcal{C}}}\right) } \times {\mathcal{Q}}$ is a finite set of transitions of the form $(q, a, g, {\mathcal{C}_{rst}}, q')$, where:

    1.  $q,q' \in {\mathcal{Q}}$ are the source and the target locations respectively;

    2.  $a \in {\Sigma}$ is the transition action;

    3.  $g \in  {\mathcal{G}}$ is the *transition guard*;

    4.  ${\mathcal{C}_{rst}}\subseteq {\mathcal{C}}$ is the subset of clocks to be reset.

A clock *valuation* $v ({c})$ is a function $v:{\mathcal{C}}\to {\mathbb{R}_{\geq 0}}$. We denote by ${\mathcal{V}}$ the set of all clock valuations and by $\textbf{d}$ the valuation which assigns the value $d$ to every clock. Given a valuation $v$ and $d \in {\mathbb{R}_{\geq 0}}$, we define $v+d$ to be the valuation $(v+d)({c}) := v({c})+d$ for every $ {c}\in {\mathcal{C}}$. The valuation $v[{\mathcal{C}_{rst}}]$, ${\mathcal{C}_{rst}}\subseteq {\mathcal{C}}$, is defined to be $v[{\mathcal{C}_{rst}}](c) = 0$ for $c \in {\mathcal{C}_{rst}}$ and $v[{\mathcal{C}_{rst}}](c) = v(c)$ for $c \notin {\mathcal{C}_{rst}}$.

The *semantics* of $A \in {\mathrm{NTA}}$ is given by the 