2005 | OriginalPaper | Buchkapitel
Decidability and Complexity Results for Timed Automata via Channel Machines
verfasst von : Parosh Aziz Abdulla, Johann Deneux, Joël Ouaknine, James Worrell
Erschienen in: Automata, Languages and Programming
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
This paper is concerned with the language inclusion problem for timed automata: given timed automata
${\mathcal A}$
and
${\mathcal B}$
, is every word accepted by
${\mathcal B}$
also accepted by
${\mathcal A}$
? Alur and Dill [3] showed that the language inclusion problem is decidable if
${\mathcal A}$
has no clocks and undecidable if
${\mathcal A}$
has two clocks (with no restriction on
${\mathcal B}$
). However, the status of the problem when
${\mathcal A}$
has one clock is not determined by [3]. In this paper we close this gap for timed automata over infinite words by showing that the one-clock language inclusion problem is undecidable. For timed automata over finite words, building on our earlier paper [20], we show that the one-clock language inclusion problem is decidable with non-primitive recursive complexity. This reveals a surprising divergence between the theory of timed automata over finite words and over infinite words. Finally, we show that if
ε
-transitions or non-singular postconditions are allowed, then the one-clock language inclusion problem is undecidable over both finite and infinite words.