their discretized languages.

Note that by the way the distance between languages is defined, it is clear that it refers to languages which are supposed to be (almost) identical or that one language is assumed to be (almost) included in the other, but this is normally the case in equivalence verification or when comparing the implication language with its specification. Note that even if the untimed languages of two TAs are identical, it is enough that there exists a cycle, in which the timed languages do not agree, then by repeatedly taking this cycle the distance between the timed traces of the two TAs may grow indefinitely, resulting in a distance of $\infty$, and it is of interest to be able to recognize when this phenomenon occurs. Thus, it seems that since the distance between $A$ and its discretized timed automaton ${{A}_d}$ is only $\frac{1}{2}$ time units, we may not lose much by comparing ${{A}_d}$ instead of $A$ with another TA. In fact, in order to be more precise in the computation of the distance between two languages we need to make the basic discretization interval, denoted $\Delta$, shorter than $\frac{1}{2}$ time units. By setting $\Delta = \frac{1}{n}$ we get 