Sökning: onr:"swepub:oai:DiVA.org:uu-149162" >
Universality Analys...
-
Abdulla, Parosh AzizUppsala universitet,Datorteknik
(författare)
Universality Analysis for One-Clock Timed Automata
- Artikel/kapitelEngelska2008
Förlag, utgivningsår, omfång ...
Nummerbeteckningar
-
LIBRIS-ID:oai:DiVA.org:uu-149162
-
https://urn.kb.se/resolve?urn=urn:nbn:se:uu:diva-149162URI
Kompletterande språkuppgifter
-
Språk:engelska
-
Sammanfattning på:engelska
Ingår i deldatabas
Klassifikation
-
Ämneskategori:ref swepub-contenttype
-
Ämneskategori:art swepub-publicationtype
Anmärkningar
-
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 och genrebeteckningar
Biuppslag (personer, institutioner, konferenser, titlar ...)
-
Deneux, JohannUppsala universitet,Datorteknik(Swepub:uu)joden179
(författare)
-
Ouaknine, Joel
(författare)
-
Quaas, Karin
(författare)
-
Worrell, James
(författare)
-
Uppsala universitetDatorteknik
(creator_code:org_t)
Sammanhörande titlar
-
Ingår i:Fundamenta Informaticae89:4, s. 419-4500169-29681875-8681
Internetlänk
Hitta via bibliotek
Till lärosätets databas