way.

1.  The directed graph structure of locations and edges of ${{A}_d}$ is the same as that of ${\mathfrak{R}^t}(A)$.

2.  The transition labels (actions) are also as in ${\mathfrak{R}^t}(A)$.

3.  There is a single clock in ${{A}_d}$, namely $t$, which is reset on each transition.

4.  The transition guards of ${{A}_d}$ are of the following form. Let $e = v_0 \to v_1$ be an edge of ${\mathfrak{R}^t}(A)$, let $w(e)$ be its weight and let $\{t_0\}, \{t_1\} \in [0,1)$ be any fractional parts of $t$ in the source and target regions. Let $$\delta = \frac{1}{2}(\lceil \{t_1\} \rceil - \lceil \{t_0\} \rceil) \in \{-\frac{1}{2},0,\frac{1}{2}\},$$ where $\lceil \{t_i\} \rceil \in \{0,1\}$ is the ceiling function applied to $t_i$. Then, we set the transition guard of the corresponding edge of ${{A}_d}$ to be $$t =  w(e) + \delta.$$ In case of a weight $w(e) = m^*$ then the transition guard is $$t \geq m+\delta.$$

A discretized timed automaton can be seen in Fig. \[fig:disc\_ta\](c).

We remark that the fact that the transition guards of ${{A}_d}$ are over $\frac{1}{2} {\mathbb{N}_0}$ and not over ${\mathbb{N}_0}$ need not bother us since the standard definition of timed automata holds also over the rational numbers. Indeed, by letting all 