regions of ${\mathfrak{R}^t}(A)$ is clearly finite (although potentially exponentially large).

\[def:aug\_region\_automaton\] Given a non-deterministic timed automaton $A$ with clocks $x_1, \ldots, x_s$ extended with absolute-time clock $t$, a corresponding augmented region automaton ${\mathfrak{R}^t}(A)$ is a tuple $({\mathcal{V}}, v_0, {\mathcal{E}}, {\Sigma}, {\mathcal{W}}^*)$, where:

1.  ${\mathcal{V}}$ is the set of vertices. Each vertex is a triple $(q, {\bf n}, \Delta)$, where $q$ is a location of $A$ and $r=({\bf n}, \Delta)$ is a region, with ${\bf n} = (n_1, \ldots, n_s) \in \{0, 1, \ldots, M, \top \}^{s}$ consisting of the integral parts of the clocks $x_1, \ldots, x_s$ and $\Delta$ is the simplex (hyper-triangle) with vertices in the lattice ${\mathbb{N}_0}^{s+1}$ of all points that satisfy a fixed ordering of the fractional parts of the clocks $t=x_0, x_1, \ldots, x_s$: $$\label{eq:simplex}
            0 \preceq_0 {\left\{{x_{i_0}}\right\}} \preceq_1 {\left\{{x_{i_1}}\right\}} \preceq_2 \cdots \preceq_s {\left\{{x_{i_s}}\right\}} < 1,$$ where $\preceq_i \, \in \{=, < \}$.

2.  $v_0 = (q_0, {\bf 0}, {\bf 0})$ is the initial vertex, where $q_0$ is the initial location of $A$ and $({\bf 0}, {\bf 0})$ indicates that all clocks have value $0$.

3.  ${\mathcal{E}}$ is the set of edges. There is an edge $(q, r) \xrightarrow{a} (q',r')$ if and only if there is 