uu.seUppsala University Publications
Change search
Link to record
Permanent link

Direct link
BETA
Deneux, Johann
Publications (6 of 6) Show all publications
Abdulla, P. A., Deneux, J., Ouaknine, J., Quaas, K. & Worrell, J. (2008). Universality Analysis for One-Clock Timed Automata. Fundamenta Informaticae, 89(4), 419-450
Open this publication in new window or tab >>Universality Analysis for One-Clock Timed Automata
Show others...
2008 (English)In: Fundamenta Informaticae, ISSN 0169-2968, E-ISSN 1875-8681, Vol. 89, no 4, p. 419-450Article in journal (Refereed) Published
Abstract [en]

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.

National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-149162 (URN)000262454000004 ()
Available from: 2011-03-15 Created: 2011-03-15 Last updated: 2018-01-12Bibliographically approved
Abdulla, P. A., Deneux, J., Kaati, L. & Nilsson, M. (2006). Minimization of Non-deterministic Automata with Large Alphabets. In: Implementation and Application of Automata: . Paper presented at CIAA 2005, June 27-29, Sophia Antipolis, France (pp. 31-42). Springer Berlin/Heidelberg
Open this publication in new window or tab >>Minimization of Non-deterministic Automata with Large Alphabets
2006 (English)In: Implementation and Application of Automata, Springer Berlin/Heidelberg, 2006, p. 31-42Conference paper, Published paper (Refereed)
Place, publisher, year, edition, pages
Springer Berlin/Heidelberg, 2006
Series
Lecture Notes in Computer Science ; 3845
National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-94525 (URN)10.1007/11605157_3 (DOI)3-540-31023-1 (ISBN)
Conference
CIAA 2005, June 27-29, Sophia Antipolis, France
Available from: 2006-05-12 Created: 2006-05-12 Last updated: 2018-01-13Bibliographically approved
Abdulla, P., Deneux, J. & Åkerlund, O. (2004). Designing Safe, Reliable Systems using Scade. In: Proc. ISoLA '04: International Symposium on Leveraging Applications of Formal Methods.
Open this publication in new window or tab >>Designing Safe, Reliable Systems using Scade
2004 (English)In: Proc. ISoLA '04: International Symposium on Leveraging Applications of Formal Methods, 2004Conference paper, Published paper (Refereed)
Identifiers
urn:nbn:se:uu:diva-72681 (URN)
Available from: 2005-05-27 Created: 2005-05-27
Abdulla, P., Deneux, J. & Mahata, P. (2004). Multi-Clock Timed Networks. In: LICS'2004, 18th IEEE Int. Symp. on Logic in Computer Science.
Open this publication in new window or tab >>Multi-Clock Timed Networks
2004 (English)In: LICS'2004, 18th IEEE Int. Symp. on Logic in Computer Science, 2004Conference paper, Published paper (Refereed)
National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-72673 (URN)
Available from: 2006-12-07 Created: 2006-12-07 Last updated: 2018-01-14
Abdulla, P., Deneux, J. & Mahata, P. (2004). Open, Closed and Robust Timed Networks.. In: CONCUR 2004 -- Concurrency Theory: 15th International Conference, London, UK, August 31 - September 3, 2004, Proceedings (pp. 529).
Open this publication in new window or tab >>Open, Closed and Robust Timed Networks.
2004 (English)In: CONCUR 2004 -- Concurrency Theory: 15th International Conference, London, UK, August 31 - September 3, 2004, Proceedings, 2004, p. 529-Conference paper, Published paper (Refereed)
National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-72677 (URN)3-540-22940-X (ISBN)
Available from: 2006-12-07 Created: 2006-12-07 Last updated: 2018-01-14
Abdulla, P., Ben Henda, N., Deneux, J., Jonsson, B. & Reidmar, T. (2004). Report on Dataflow Dependencies in Billing Processing Systems. In: Proc. ISoLA '04: 1st International Symposium on Leveraging Applications of Formal Methods.
Open this publication in new window or tab >>Report on Dataflow Dependencies in Billing Processing Systems
Show others...
2004 (English)In: Proc. ISoLA '04: 1st International Symposium on Leveraging Applications of Formal Methods, 2004Conference paper, Published paper (Refereed)
Identifiers
urn:nbn:se:uu:diva-72685 (URN)
Available from: 2005-05-27 Created: 2005-05-27
Organisations

Search in DiVA

Show all publications