On the Distance Between Timed Automata.

Publikation: Beitrag in Buch/Bericht/KonferenzbandBeitrag in einem KonferenzbandForschungBegutachtung

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.
Originalspracheenglisch
TitelFORMATS 2019
Redakteure/-innenÉ André, M. Stoelinga
Herausgeber (Verlag)Springer, Cham
Seiten199-215
Seitenumfang17
Band11750
ISBN (elektronisch)978-3-030-29662-9
ISBN (Print)978-3-030-29661-2
DOIs
PublikationsstatusVeröffentlicht - 13 Aug 2019
Veranstaltung17th International Conference on Formal Modeling and Analysis of Timed Systems - Amsterdam, Niederlande
Dauer: 27 Aug 201929 Aug 2019

Publikationsreihe

NameLecture Notes in Computer Science
Band11750

Konferenz

Konferenz17th International Conference on Formal Modeling and Analysis of Timed Systems
KurztitelFORMATS 2019
LandNiederlande
OrtAmsterdam
Zeitraum27/08/1929/08/19

Fingerprint

Timed Automata
Inclusion
Trace
Digitization
Automata
Euclidean
Closure
Discretization
Specification
Restriction
Topology
Unit
Language

Dies zitieren

Rosenmann, A. (2019). On the Distance Between Timed Automata. in É. André, & M. Stoelinga (Hrsg.), FORMATS 2019 (Band 11750, S. 199-215). (Lecture Notes in Computer Science; Band 11750). Springer, Cham. https://doi.org/10.1007/978-3-030-29662-9_12

On the Distance Between Timed Automata. / Rosenmann, Amnon.

FORMATS 2019. Hrsg. / É André; M. Stoelinga. Band 11750 Springer, Cham, 2019. S. 199-215 (Lecture Notes in Computer Science; Band 11750).

Publikation: Beitrag in Buch/Bericht/KonferenzbandBeitrag in einem KonferenzbandForschungBegutachtung

Rosenmann, A 2019, On the Distance Between Timed Automata. in É André & M Stoelinga (Hrsg.), FORMATS 2019. Bd. 11750, Lecture Notes in Computer Science, Bd. 11750, Springer, Cham, S. 199-215, Amsterdam, Niederlande, 27/08/19. https://doi.org/10.1007/978-3-030-29662-9_12
Rosenmann A. On the Distance Between Timed Automata. in André É, Stoelinga M, Hrsg., FORMATS 2019. Band 11750. Springer, Cham. 2019. S. 199-215. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-030-29662-9_12
Rosenmann, Amnon. / On the Distance Between Timed Automata. FORMATS 2019. Hrsg. / É André ; M. Stoelinga. Band 11750 Springer, Cham, 2019. S. 199-215 (Lecture Notes in Computer Science).
@inproceedings{df771e79b8764c0eaf47e06d78289abc,
title = "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 $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.",
author = "Amnon Rosenmann",
year = "2019",
month = "8",
day = "13",
doi = "10.1007/978-3-030-29662-9_12",
language = "English",
isbn = "978-3-030-29661-2",
volume = "11750",
series = "Lecture Notes in Computer Science",
publisher = "Springer, Cham",
pages = "199--215",
editor = "{\'E} Andr{\'e} and M. Stoelinga",
booktitle = "FORMATS 2019",

}

TY - GEN

T1 - On the Distance Between Timed Automata.

AU - Rosenmann, Amnon

PY - 2019/8/13

Y1 - 2019/8/13

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-030-29662-9_12

DO - 10.1007/978-3-030-29662-9_12

M3 - Conference contribution

SN - 978-3-030-29661-2

VL - 11750

T3 - Lecture Notes in Computer Science

SP - 199

EP - 215

BT - FORMATS 2019

A2 - André, É

A2 - Stoelinga, M.

PB - Springer, Cham

ER -