Undecidability of universality for timed automata with minimal resources
Timed automata were introduced by Alur and Dill in the early 1990s and have since become the most prominent modelling formalism for real-time systems. A fundamental limit to the algorithmic analysis of timed automata, however, results from the undecidability of the universality problem: does a given...
| Main Authors: | , , |
|---|---|
| Format: | Journal article |
| Language: | English |
| Published: |
2007
|
| _version_ | 1797073281673592832 |
|---|---|
| author | Adams, S Ouaknine, J Worrell, J |
| author_facet | Adams, S Ouaknine, J Worrell, J |
| author_sort | Adams, S |
| collection | OXFORD |
| description | Timed automata were introduced by Alur and Dill in the early 1990s and have since become the most prominent modelling formalism for real-time systems. A fundamental limit to the algorithmic analysis of timed automata, however, results from the undecidability of the universality problem: does a given timed automaton accept every timed word? As a result, much research has focussed on attempting to circumvent this difficulty, often by restricting the class of automata under consideration, or by altering their semantics. In this paper, we study the decidability of universality for classes of timed automata with minimal resources. More precisely, we consider restrictions on the number of states and clock constants, as well as the size of the event alphabet. Our main result is that universality remains undecidable for timed automata with a single state, over a single-event alphabet, and using no more than three distinct clock constants. © Springer-Verlag Berlin Heidelberg 2007. |
| first_indexed | 2024-03-06T23:19:49Z |
| format | Journal article |
| id | oxford-uuid:685b8abe-009b-4aff-a41f-7abbeadf770c |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-06T23:19:49Z |
| publishDate | 2007 |
| record_format | dspace |
| spelling | oxford-uuid:685b8abe-009b-4aff-a41f-7abbeadf770c2022-03-26T18:44:18ZUndecidability of universality for timed automata with minimal resourcesJournal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:685b8abe-009b-4aff-a41f-7abbeadf770cEnglishSymplectic Elements at Oxford2007Adams, SOuaknine, JWorrell, JTimed automata were introduced by Alur and Dill in the early 1990s and have since become the most prominent modelling formalism for real-time systems. A fundamental limit to the algorithmic analysis of timed automata, however, results from the undecidability of the universality problem: does a given timed automaton accept every timed word? As a result, much research has focussed on attempting to circumvent this difficulty, often by restricting the class of automata under consideration, or by altering their semantics. In this paper, we study the decidability of universality for classes of timed automata with minimal resources. More precisely, we consider restrictions on the number of states and clock constants, as well as the size of the event alphabet. Our main result is that universality remains undecidable for timed automata with a single state, over a single-event alphabet, and using no more than three distinct clock constants. © Springer-Verlag Berlin Heidelberg 2007. |
| spellingShingle | Adams, S Ouaknine, J Worrell, J Undecidability of universality for timed automata with minimal resources |
| title | Undecidability of universality for timed automata with minimal resources |
| title_full | Undecidability of universality for timed automata with minimal resources |
| title_fullStr | Undecidability of universality for timed automata with minimal resources |
| title_full_unstemmed | Undecidability of universality for timed automata with minimal resources |
| title_short | Undecidability of universality for timed automata with minimal resources |
| title_sort | undecidability of universality for timed automata with minimal resources |
| work_keys_str_mv | AT adamss undecidabilityofuniversalityfortimedautomatawithminimalresources AT ouakninej undecidabilityofuniversalityfortimedautomatawithminimalresources AT worrellj undecidabilityofuniversalityfortimedautomatawithminimalresources |