clocks run twice as fast and multiplying by 2 all values in the constraints of the transition guards, we end up in an automaton over the integers.

The Conformance Distance {#sec:inc_gap}
========================

We want to define a metric on the set of timed traces in order to define (conformance) distance between timed languages.

Given a set $T$ of timed traces over the same alphabet $\Sigma$, we define the $\infty$-metric or max-metric $d$ on $T$ in the following way. Given two timed traces $$\begin{aligned}
        \tau_1 &=(t_1^{\tau_1}, a_1^{\tau_1}), (t_2^{\tau_1}, a_{2}^{\tau_1}),\ldots,(t_m^{\tau_1}, a_m^{\tau_1}), \\
        \tau_2 &=(t_1^{\tau_2}, a_1^{\tau_2}), (t_2^{\tau_2}, a_{2}^{\tau_2}),\ldots,(t_n^{\tau_2}, a_n^{\tau_2}),
    \end{aligned}$$ the distance between $\tau_1$ and $\tau_2$ is $$d(\tau_1, \tau_2) = \begin{cases}
    \infty, &\quad \mathrm{if} \; m \neq n \; \mathrm{or} \; a_i^{\tau_1} \neq a_i^{\tau_2} \; \mathrm{for} \; \mathrm{some} \; i,\\
    \max_i{| t_i^{\tau_1}-t_i^{\tau_2} |}, &\quad \mathrm{otherwise.}
    \end{cases}$$

The above metric over the set of traces induces inclusion relation on timed languages (languages of timed automata).

Given two timed languages ${\mathfrak{L}}_1$ and ${\mathfrak{L}}_2$, ${\mathfrak{L}}_1$ is $\varepsilon$-included in ${\mathfrak{L}}_2$, denoted ${\mathfrak{L}}_1 \subseteq_{\varepsilon} {\mathfrak{L}}_2$, if for every timed trace $\tau_1 \in {\mathfrak{L}}_1$ there exists a timed trace $\tau_2 \in {\mathfrak{L}}_2$ such that $d(\tau_1, \tau_2) \leq \varepsilon$.\
The *conformance distance* $c({\mathfrak{L}}_1, {\mathfrak{L}}_2)$ between ${\mathfrak{L}}_1$ and ${\mathfrak{L}}_2$ is $$c({\mathfrak{L}}_1, 