Note: [] Address for correspondence: Uppsala University, Dag
Hammarskjölds v. 10 B 75105 Uppsala, Sweden
Abstract: 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
better quasi-orderings, a refinement of the theory of well quasi-orderings, to
prove termination of the algorithm. We have implemented a prototype tool based
on our method, and checked universality for a number of timed automata.
Comparisons with a region-based prototype tool confirm that zones are a more
succinct representation, and hence allow a much more efficient implementation
of the universality algorithm.
