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.
