  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 some restriction whether the
distance between two timed automata is finite or infinite.
