On the Distance Between Timed Automata

Abstract

Some fundamental problems in the class of non-deterministic timed automata, like 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) are, in general, undecidable. In order to tackle this disturbing problem we show how to effectively construct deterministic timed automata (Formula Presented) and (Formula Presented) that are discretizations (digitizations) of the non-deterministic timed automata A and B and differ from the original automata by at most (Formula Presented) 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 (Formula Presented) we consider (Formula Presented), the closure of (Formula Presented) in the Euclidean topology: if (Formula Presented) then (Formula Presented) and if (Formula Presented) then (Formula Presented). Moreover, if(Formula Presented) we would like to know how far away is (Formula Presented) from being included in (Formula Presented). 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.