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 th...
| Main Authors: | , , , , |
|---|---|
| Format: | Journal article |
| Language: | English |
| Published: |
2008
|
| _version_ | 1797094114547728384 |
|---|---|
| author | Abdulla, P Deneux, J Ouaknine, J Quaas, K Worrell, J |
| author_facet | Abdulla, P Deneux, J Ouaknine, J Quaas, K Worrell, J |
| author_sort | Abdulla, P |
| collection | OXFORD |
| description | 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. |
| first_indexed | 2024-03-07T04:09:39Z |
| format | Journal article |
| id | oxford-uuid:c7625d7f-726c-4dd8-b609-9e0a38e1df91 |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-07T04:09:39Z |
| publishDate | 2008 |
| record_format | dspace |
| spelling | oxford-uuid:c7625d7f-726c-4dd8-b609-9e0a38e1df912022-03-27T06:44:44ZUniversality Analysis for One-Clock Timed AutomataJournal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:c7625d7f-726c-4dd8-b609-9e0a38e1df91EnglishSymplectic Elements at Oxford2008Abdulla, PDeneux, JOuaknine, JQuaas, KWorrell, JThis 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. |
| spellingShingle | Abdulla, P Deneux, J Ouaknine, J Quaas, K Worrell, J Universality Analysis for One-Clock Timed Automata |
| title | Universality Analysis for One-Clock Timed Automata |
| title_full | Universality Analysis for One-Clock Timed Automata |
| title_fullStr | Universality Analysis for One-Clock Timed Automata |
| title_full_unstemmed | Universality Analysis for One-Clock Timed Automata |
| title_short | Universality Analysis for One-Clock Timed Automata |
| title_sort | universality analysis for one clock timed automata |
| work_keys_str_mv | AT abdullap universalityanalysisforoneclocktimedautomata AT deneuxj universalityanalysisforoneclocktimedautomata AT ouakninej universalityanalysisforoneclocktimedautomata AT quaask universalityanalysisforoneclocktimedautomata AT worrellj universalityanalysisforoneclocktimedautomata |