Sciweavers

ICALP
2005
Springer

Decidability and Complexity Results for Timed Automata via Channel Machines

13 years 9 months ago
Decidability and Complexity Results for Timed Automata via Channel Machines
Abstract. This paper is concerned with the language inclusion problem for timed automata: given timed automata A and B, is every word accepted by B also accepted by A? Alur and Dill [5] showed that the language inclusion problem is decidable if A has no clocks and undecidable if A has two clocks (with no restriction on B). However, the status of the problem when A has one clock is not determined by [5]. 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 [19], we show that the one-clock language inclusion problem is decidable with nonprimitive 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 ov...
Parosh Aziz Abdulla, Johann Deneux, Joël Ouak
Added 27 Jun 2010
Updated 27 Jun 2010
Type Conference
Year 2005
Where ICALP
Authors Parosh Aziz Abdulla, Johann Deneux, Joël Ouaknine, James Worrell
Comments (0)