from ${\mathfrak{L}}(B)$, causing $c({\mathfrak{L}}(A), {\mathfrak{L}}(B)) = \infty$. For example, it may happen that due to imprecisions or delays in a real system, a TA model is changed to allow wider time intervals around actions compared to the more idealistic previous model. It is then necessary to check whether or not this extended freedom is controlled and the distance between the two TAs stays within a reasonable bound (see [@BMS15] regarding an ideal model versus a realistic model). Moreover, an algorithm based on the approach suggested here may find the timed traces that deviate from the allowed distance between two timed languages. Further applications for computing the distance may be when safety properties include time restrictions for specific set of timed traces, given as timed automata, and we want to check these timed traces with respect to the implementation model. In general, in a design of a computerized system, e.g. a network, that contains timing changes, a relaxed equivalence verification may allow bounded perturbations in time that needed to be checked.

Computing the distance between TAs (or their languages), even between discretized TAs, may be quite complex. Here we concentrate on the problem of deciding whether the distance is infinite. It 