Universality Analysis for One-Clock Timed Automata

This paper is concerned with the universality problem for timed automata: given a timed automaton A, does A accept all timed words? Alur and Dill have shown that the universality problem is undecidable if A has two clocks, but they left open the status of the problem when A has a single clock. In this paper we close this gap for timed automata over infinite words by showing that the one-clock universality problem is undecidable. For timed automata over finite words we show that the one-clock universality 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. We also show that if -transitions or non-singular postconditions are allowed, then the one-clock universality problem is undecidable over both finite and infinite words. Furthermore, we present a zone-based algorithm for solving the universality problem for single-clock timed automata. We apply the theory of b...

• Type: Journal
• Year: 2008
• Where: FUIN
• Authors: Parosh Aziz Abdulla, Johann Deneux, Joël Ouaknine, Karin Quaas, James Worrell
• Keywords: FUIN 2008, Infinite Words, One-clock Universality Problem, Universality Problem