zbMATH — the first resource for mathematics

Undecidable problems about timed automata. (English) Zbl 1141.68433
Asarin, Eugene (ed.) et al., Formal modeling and analysis of timed systems. 4th international conference, FORMATS 2006, Paris, France, September 25–27, 2006. Proceedings. Berlin: Springer (ISBN 978-3-540-45026-9/pbk). Lecture Notes in Computer Science 4202, 187-199 (2006).
Summary: We solve some decision problems for timed automata which were raised by S. Tripakis [“Folk theorems on the determinization and minimization of timed automata”, Lect. Notes Comput. Sci. 2791, 182–188 (2004; Zbl 1099.68648)] and by E. Asarin [“Challenges in timed languages: from applied theory to basic theory”, Bull. Eur. Assoc. Theor. Comput. Sci., EATCS 83, 106–120 (2004)]. In particular, we show that one cannot decide whether a given timed automaton is determinizable or whether the complement of a timed regular language is timed regular. We show that the problem of the minimization of the number of clocks of a timed automaton is undecidable. It is also undecidable whether the shuffle of two timed regular languages is timed regular. We show that in the case of timed Büchi automata accepting infinite timed words some of these problems are \(\Pi _{1}^{1}\)-hard, hence highly undecidable (located beyond the arithmetical hierarchy).
For the entire collection see [Zbl 1137.68001].

68Q45 Formal languages and automata
03D35 Undecidability and degrees of sets of sentences
Full Text: DOI