a run on $A$ containing $(q, v) \xrightarrow{d} (q, v + d) \xrightarrow{a} (q', v')$, such that, the clock valuation $v$ is in the region $r$ and $v'$ is in $r'$.

4.  ${\Sigma}$ is the finite set of actions.

5.  ${\mathcal{W}}^*$ is the set of weights $m$ on the edges calculated as $m = \lfloor t_1 \rfloor - \lfloor t_0 \rfloor \in [0..M]$, where $\lfloor t_1 \rfloor$ ($\lfloor t_0 \rfloor$) is the integral part of $t$ in the target (source) location in a corresponding run on $A$. There may be more than one edge between two vertices of ${\mathfrak{R}^t}(A)$, each one with a distinguished weight. A weight $m$ may be marked as $m^*$, representing infinitely-many consecutive values $m$, $m+1$, $m+2, \ldots$ as weights between the same two vertices, for example when the regular clocks passed the maximal value $M$.

An augmented region automaton can be seen in Fig. \[fig:disc\_ta\](b) (the example is taken from [@ta]).

Discretized Timed Automaton {#sec:Approx}
===========================

After constructing the augmented region automaton ${\mathfrak{R}^t}(A)$, we turn it into a deterministic timed automaton ${{A}_d}$ which discretizes (digitizes) $A$.

\[def:appta\] A *discretized timed automaton* ${{A}_d}$ is a timed automaton constructed from the augmented region automaton ${\mathfrak{R}^t}(A)$ in the following 