+ \frac{1}{2}$, thus, the time difference is less than $\frac{1}{2}$ time units. The fact that the clock $t$ of ${{A}_d}$ is synchronized with the clock $t$ that was added to $A$ to measures absolute time guarantees that the cumulative error does not increase over time but remains bounded by $\frac{1}{2}$. That is, ${{A}_d}$ is a $\frac{1}{2}$-time-unit approximation of $A$: there exits a surjective mapping $$\label{eq:proj}
    \pi : {\mathfrak{L}}(A) \twoheadrightarrow {\mathfrak{L}}({{A}_d}),$$ such that if $\pi(\tau) = \tilde{\tau}$ then $d(\tau, \tilde{\tau}) < \frac{1}{2}$. We showed that the following holds.

\[th:approx\_ta\] $d({\mathfrak{L}}(A), {\mathfrak{L}}({{A}_d})) \leq \frac{1}{2}$.

Since $t$ is reset only on values in $\frac{1}{2}{\mathbb{N}_0}$ then ${{A}_d}$ is determinizable (see [@irta], [@bbbb]). In fact, since $t$ is reset at each transition, we can remove it altogether to obtain an action-labeled, weighted directed graph. The determinization algorithm is then straightforward by searching the graph in a breadth-first manner, unifying edges of the same source location that agree on their labels: $(a,t)$, $a$ - action, $t$ -time, followed by unifying the target locations. The number of vertices, however, may grow exponentially.

Computing the Conformance Distance
==================================

Since ${{A}_d}$ is determinizable, we can gain information about the relation between the languages of two timed automata by comparing 