Universality Analysis for One-Clock Timed Automata
2008 (English)In: Fundamenta Informaticae, ISSN 0169-2968, Vol. 89, no 4, 419-450 p.Article in journal (Refereed) Published
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.
Place, publisher, year, edition, pages
2008. Vol. 89, no 4, 419-450 p.
IdentifiersURN: urn:nbn:se:uu:diva-149162ISI: 000262454000004OAI: oai:DiVA.org:uu-149162DiVA: diva2:404060