that $d({\mathfrak{L}}(A), {\mathfrak{L}}({{A}_d})) < \frac{1}{n}$, thus we can make ${\mathfrak{L}}(A)$ and ${\mathfrak{L}}({{A}_d})$ as close to one another as we like (of course, in the expense of complexity). However, it turns out that it suffices to choose $\Delta = \frac{1}{6}$ in order to get the maximal precision about $d({\mathfrak{L}}(A), {\mathfrak{L}}(B))$.

For our convenience, since we prefer not to work with small fractions we accelerate the clocks to run at triple speed. That is, from now on, given the timed automata $A$ and $B$ under test, we first multiply by $3$ all the numbers that appear in the transition guards, so they all belong to $3{\mathbb{N}_0}$. Then we proceed as before: we construct the region automata with respect to basic regions of size 1 time unit and the discretized automata with respect to $\Delta = \frac{1}{2}$. Now we have, $$\label{eq:gap_set}
c({\mathfrak{L}}(A), {\mathfrak{L}}(B)) \in \frac{3}{2}{\mathbb{N}_0}\cup \{\infty\}$$ and $$d({\mathfrak{L}}(A), {\mathfrak{L}}({{A}_d})) \leq \frac{1}{2}, \quad d({\mathfrak{L}}(B), {\mathfrak{L}}({{B}_d})) \leq \frac{1}{2}.$$

\[th:inclusion\_gap\] Let $A,B \in {\mathrm{NTA}}$ with clocks running at triple speed and let ${{A}_d}, {{B}_d}$ be their discretized timed automata with respect to $\Delta = \frac{1}{2}$. Then $$|\, c({\mathfrak{L}}(A), {\mathfrak{L}}(B)) - c({\mathfrak{L}}({{A}_d}), {\mathfrak{L}}({{B}_d})) \, | \leq \frac{1}{2}$$ and $c({\mathfrak{L}}(A), {\mathfrak{L}}(B))$ is known in case $c({\mathfrak{L}}({{A}_d}), {\mathfrak{L}}({{B}_d}))$ is 