some restriction whether the distance between two timed automata is finite or infinite.
address: 'Graz University of Technology, Steyrergasse 30, A-8010 Graz, Austria'
author:
- Amnon Rosenmann
bibliography:
- 'ta.bib'
title: On the Distance between Timed Automata
---

Introduction {#sec:intro}
============

Timed automaton (TA) was introduced by Alur and Dill [@ta] as an abstract model for real-time systems by extending finite automaton with continuous clocks. When the ${\mathrm{TA}}$s are non-deterministic then a fundamental problem of language inclusion is, in general, undecidable, for example, whether the set of timed traces of the ${\mathrm{TA}}$ representing the implementation is included in that of the specification. This lead to imposing restrictions on and modifications to non-deterministic TAs in order to achieve decidability (see [@bbbb; @ta-eps; @era; @updatable-ta; @Ouak_one_clk; @Ouak_time_bound; @bounded-time; @Dec_TA_Survey; @bound-det] for a partial list). Another approach was to allow robustness in the language [@GHJ97] or perturbations in the clocks [@purturbed-ta] (see also [@BMS15]). The problem is that by allowing a fixed imprecision, undecidability problems due to working over continuous time do not vanish.

Digitization of timed systems, where basic decision problems like language inclusion are decidable, was considered, for example, in [@HMP92; @O02; @OW03]. But, as stated in [@OW03], the implementation should 