×

zbMATH — the first resource for mathematics

Decidability and complexity results for timed automata via channel machines. (English) Zbl 1085.68078
Caires, Luís (ed.) et al., Automata, languages and programming. 32nd international colloquium, ICALP 2005, Lisbon, Portugal, July 11–15, 2005. Proceedings. Berlin: Springer (ISBN 3-540-27580-0/pbk). Lecture Notes in Computer Science 3580, 1089-1101 (2005).
Summary: 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\)? R. Alur and D. Dill [Theor. Comput. Sci. 126, 183–235 (1994; Zbl 0803.68071)] 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 by Alur and Dill [loc. cit.]. 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 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 \(\epsilon\)-transitions or non-singular postconditions are allowed, then the one-clock language inclusion problem is undecidable over both finite and infinite words.
For the entire collection see [Zbl 1078.68001].

MSC:
68Q45 Formal languages and automata
68Q60 Specification and verification (program logics, model checking, etc.)
PDF BibTeX XML Cite
Full Text: DOI