On Almost Deterministic Timed Automata

Abstract: Timed Automata (TAs) are a generalization of $\omega$-automata that has been largely studied both from the practical point of view of verification of real-time systems, and from the theoretical perspective of formal languages. Universality for deterministic TAs is PSPACE-complete but, surprisingly, it was shown to be $\Pi_1^1$-hard for nondeterministic TAs. The exact position of this problem in the analytical hierarchy is still open. In this paper we consider the more restricted class of almost deterministic TAs. In our main contribution we show that the restriction to almost deterministic TAs characterizes this decision problem as $\Pi_1^1$-complete and we also show that, in contrast to $\omega$-automata, almost deterministic TAs define a proper subclass of nondeterministic TAs. These results give new insights regarding the role of nondeterminism in TAs and reveal some surprising aspects of the universality problem for nondeterministic TAs.



Resumo: Autômatos Temporizados (ATs) são uma generalização de $\omega$-autômatos que tem sido bastante estudada tanto do ponto de vista prático de verificação de sistemas de tempo real, quanto da perspectiva teórica de linguagens formais. Universalidade para ATs determinísticos é PSPACE-completo mas, surpreendentemente, foi demonstrado $\Pi_1^1$-difícil para ATs não-determinísticos. A posição exata deste problema na hierarquia analítica está em aberto. Neste artigo nós consideramos a classe mais restrita de ATs quase determinísticos. Na nossa principal contribuição, mostramos que universalidade para ATs quase determinísticos é $\Pi_1^1$-completo e também mostramos que, ao contrário de $\omega$-autômatos, ATs quase determinísticos definem uma subclasse própria de ATs não-determinísticos. Estes resultados ajudam a clarificar o papel do não-determinismo em ATs e revelam alguns aspectos surpreendentes do problema de universalidade para ATs não-determinísticos.

2001