Sökning: onr:"swepub:oai:DiVA.org:uu-149162" >
Universality Analys...
Universality Analysis for One-Clock Timed Automata
-
- Abdulla, Parosh Aziz (författare)
- Uppsala universitet,Datorteknik
-
- Deneux, Johann (författare)
- Uppsala universitet,Datorteknik
-
Ouaknine, Joel (författare)
-
visa fler...
-
Quaas, Karin (författare)
-
Worrell, James (författare)
-
visa färre...
-
(creator_code:org_t)
- 2008
- 2008
- Engelska.
-
Ingår i: Fundamenta Informaticae. - 0169-2968 .- 1875-8681. ; 89:4, s. 419-450
- Relaterad länk:
-
https://urn.kb.se/re...
Abstract
Ämnesord
Stäng
- 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.
Ämnesord
- NATURVETENSKAP -- Data- och informationsvetenskap -- Datavetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences -- Computer Sciences (hsv//eng)
Nyckelord
- Computer science
- Datavetenskap
Publikations- och innehållstyp
- ref (ämneskategori)
- art (ämneskategori)
Hitta via bibliotek
Till lärosätets databas