On the Distance Between Timed Automata
| Autor: | Amnon Rosenmann |
|---|---|
| Rok vydání: | 2019 |
| Předmět: |
Physics
050101 languages & linguistics 05 social sciences Timed automaton Order (ring theory) Language inclusion 02 engineering and technology Decidability Combinatorics Closure (mathematics) Euclidean topology 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing 0501 psychology and cognitive sciences Mathematics::Representation Theory Computer Science::Formal Languages and Automata Theory |
| Zdroj: | Lecture Notes in Computer Science ISBN: 9783030296612 FORMATS |
| DOI: | 10.1007/978-3-030-29662-9_12 |
| Popis: | 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 \(\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)}\). |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|