Classes of Timed Automata and the Undecidability of Universality

Article type: Research Article

Authors: Moura, Arnaldo V. | Pinto, Guilherme A.

Affiliations: Institute of Computing, University of Campinas, C.P. 6176 13083-970, Campinas, SP, Brazil. E-mail: [email protected] | Dep. of Computer Science, University of Brasília, C.P. 4466 70910-900, Brasília, DF, Brazil. E-mail: [email protected]

Abstract: Universality for deterministic Timed Büchi Automata (TBA) is PSPACE-complete but becomes highly undecidable when unrestricted nondeterminism is allowed. More precisely, universality for nondeterministic TBA is Π^1_1-hard and its precise position in the analytical hierarchy is still an open question. In this paper we introduce two types of syntactical restrictions to nondeterministic TBA, which are of independent interest, and show that their universality problem is Π^1_1-complete. These restrictions define, as we prove, proper subclasses of the class of timed languages defined by nondeterministic TBA. This suggests, as we argue, that no solution to that open question will come without surprise. We also establish closure properties and the relationships between the classes of languages we describe.

Keywords: Timed Automata, Universality, Analytical Hierarchy

Journal: Fundamenta Informaticae, vol. 82, no. 1-2, pp. 171-184, 2008