## Universality analysis for one-clock timed automata

*Parosh Aziz Abdulla*, *Johann Deneux*, *Joël
Ouaknine*, *Karin Quaas*, and *James Worrell*
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
epsilon-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.

*Fundamenta Informaticae* 89(4), 2008. 32 pages.

PostScript /
PDF
© 2008 IOS Press.

Imprint / Data Protection