Wyniki wyszukiwania - Biblioteka Nauki

Nowa wersja platformy, zawierająca wyłącznie zasoby pełnotekstowe, jest już dostępna.
Przejdź na https://bibliotekanauki.pl

Ograniczanie wyników

3 Fundamenta Informaticae

Znaleziono wyników: 3

Liczba wyników na stronie

Wyniki wyszukiwania

Sortuj według:

Ogranicz wyniki do:

Relating Reachability Problems in Timed and Counter Automata

100%

Haase C. , Ouaknine J. , Worrell J.

tom Vol. 143, nr 3/4

317--338

We establish a relationship between reachability problems in timed automata and spacebounded counter automata. We show that reachability in timed automata with three or more clocks is logarithmic-space inter-reducible with reachability in space-bounded counter automata with two counters. We moreover show the logarithmic-space equivalence of reachability in two-clock timed automata and space-bounded one-counter automata. This last reduction has recently been employed by Fearnley and Jurdziński to settle the computational complexity of reachability in two-clock timed automata.

Nets with Tokens which Carry Data

88%

Lazić R. , Newcomb T. , Ouaknine J. , Roscoe A. W. , Worrell J.

2008

tom Vol. 88, nr 3

251-274

We study data nets, a generalisation of Petri nets in which tokens carry data from linearlyordered infinite domains and in which whole-place operations such as resets and transfers are possible. Data nets subsume several known classes of infinite-state systems, including multiset rewriting systems and polymorphic systems with arrays. We show that coverability and termination are decidable for arbitrary data nets, and that boundedness is decidable for data nets in which whole-place operations are restricted to transfers. By providing an encoding of lossy channel systems into data nets without whole-place operations, we establish that coverability, termination and boundedness for the latter class have non-primitive recursive complexity. The main result of the paper is that, even for unordered data domains (i.e., with only the equality predicate), each of the three verification problems for data nets without whole-place operations has non-elementary complexity.

Universality Analysis for One-Clock Timed Automata

88%

Abdulla P. A. , Deneux J. , Ouaknine J. , Quaas K. , Worrell J.

2008

tom Vol. 89, nr 4

419-450

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.