---
abstract: |
    The problem of inclusion of the language accepted by timed automaton $A$ (e.g., the implementation) in the language accepted by $B$ (e.g., the specification) is, in general, undecidable in the class of non-deterministic timed automata. In order to tackle this disturbing problem we show how to effectively construct deterministic timed automata ${{A}_d}$ and ${{B}_d}$ that are discretizations (digitizations) of the non-deterministic timed automata $A$ and $B$ and differ from the original automata by at most $\frac{1}{6}$ time units on each occurrence of an event. Language inclusion in the discretized timed automata is decidable and it is also decidable when instead of ${\mathfrak{L}}(B)$ we consider $\overline{{\mathfrak{L}}(B)}$, the closure of ${{\mathfrak{L}}(B)}$ in the Euclidean topology: if ${\mathfrak{L}}({{A}_d}) \nsubseteq {\mathfrak{L}}({{B}_d})$ then ${\mathfrak{L}}(A) \nsubseteq {\mathfrak{L}}(B)$ and if ${\mathfrak{L}}({{A}_d}) \subseteq {\mathfrak{L}}({{B}_d})$ then ${\mathfrak{L}}(A) \subseteq \overline{{\mathfrak{L}}(B)}$.

    Moreover, if ${\mathfrak{L}}({{A}_d}) \nsubseteq {\mathfrak{L}}({{B}_d})$ we would like to know how far away is ${\mathfrak{L}}({{A}_d})$ from being included in ${\mathfrak{L}}({{B}_d})$. For that matter we define the distance between the languages of timed automata as the limit on how far away a timed trace of one timed automaton can be from the closest timed trace of the other timed automaton. We then show how one can decide under 