On the Distance Between Timed Automata.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 $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 $L(B)$ we consider $\overline{L(B)}$, the closure of $L(B)$ in the Euclidean topology:
if $L(A_d) \nsubseteq L(B_d)$ then $L(A) \nsubseteq L(B)$ and if
$L(A_d) \subseteq L(B_d)$ then $L(A) \subseteq \overline{L(B)}$.

Moreover, if $L(A_d) \nsubseteq L(B_d)$ we would like to know how far away is $L(A_d)$ from being included in $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.
Original languageEnglish
Title of host publicationFORMATS 2019
EditorsÉ André, M. Stoelinga
PublisherSpringer, Cham
Pages199-215
Number of pages17
Volume11750
ISBN (Electronic)978-3-030-29662-9
ISBN (Print)978-3-030-29661-2
DOIs
Publication statusPublished - 13 Aug 2019
Event17th International Conference on Formal Modeling and Analysis of Timed Systems - Amsterdam, Netherlands
Duration: 27 Aug 201929 Aug 2019

Publication series

NameLecture Notes in Computer Science
Volume11750

Conference

Conference17th International Conference on Formal Modeling and Analysis of Timed Systems
Abbreviated titleFORMATS 2019
CountryNetherlands
CityAmsterdam
Period27/08/1929/08/19

Fingerprint Dive into the research topics of 'On the Distance Between Timed Automata.'. Together they form a unique fingerprint.

Cite this