On the Distance between Timed Automata

TL;DR

This paper introduces a method to approximate non-deterministic timed automata with deterministic ones through discretization, enabling decidable language inclusion checks and defining a measure of distance between automata's languages.

Contribution

It presents a novel discretization approach for timed automata that preserves inclusion properties and introduces a way to measure the distance between automata languages.

Findings

Discretization of timed automata preserves key language inclusion properties.

Decidability of language inclusion for discretized automata is established.

A new metric for the distance between timed automata languages is proposed.

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