Wyniki wyszukiwania - BazTech

1

Shelah-Stupp’s Iteration and Muchnik’s Iteration

Caucal D., Knapik T.

Fundamenta Informaticae

|

2018

|

Vol. 159, nr 4

327--359

EN

In the early seventies, Shelah proposed a model-theoretic construction, nowadays called “iteration”. This construction is an infinite replication in a tree-like manner where every vertex possesses its own copy of the original structure. Stupp proved that the decidability of the monadic second-order (MSO) theory is transferred from the original structure onto the iterated one. In its extended version discovered by Muchnik and introduced by Semenov, the iteration became popular in computer science logic thanks to a paper by Walukiewicz. Compared to the basic iteration, Muchnik’s iteration has an additional unary predicate which, in every copy, marks the vertex that is the clone of the possessor of the copy. A widely spread belief that this extension is crucial is formally confirmed in the paper. Two hierarchies of relational structures generated from finite structures by MSO interpretations and either Shelah-Stupp’s iteration or Muchnik’s iteration are compared. It turns out that the two hierarchies coincide at level 1. Every level of the latter hierarchy is closed under Shelah-Stupp’s interation. In particular, the former hierarchy collapses at level 1.

2

A Framework for the Verification of Parameterized Infinite-state Systems

Alberti F., Ghilardi S., Sharygina N.

Fundamenta Informaticae

|

2017

|

Vol. 150, nr 1

1--24

EN

We present our framework for the verification of parameterized infinite-state systems. The framework has been successfully applied in the verification of heterogeneous systems, ranging from distributed fault-tolerant protocols to programs handling unbounded data-structures. In such application domains, being able to infer quantified invariants is a mandatory requirement for successful results. Our framework differentiates itself from the state-of-the-art solutions targeting the generation of quantified safe inductive invariants: instead of monolitically exploiting a single static analysis technique, it is based on the effective integration of several analysis strategies. The paper targets the description of the engineering strategies adopted for a successful implementation of such an integrated framework, and presents the extensive experimental evaluation demonstrating its effectiveness.

3

Relating Reachability Problems in Timed and Counter Automata

Haase C., Ouaknine J., Worrell J.

Fundamenta Informaticae

|

2016

|

Vol. 143, nr 3/4

317--338

EN

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.

4

Nets with Tokens which Carry Data

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

Fundamenta Informaticae

|

2008

|

Vol. 88, nr 3

251-274

EN

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.

5

Decidability Analysis of Self-Stabilization for Infinite-State Systems

Yen H-C., Yu L-P.

Fundamenta Informaticae

|

2006

|

Vol. 70, nr 4

387-402

EN

For a variety of infinite-state systems, the problem of deciding whether a given system is self-stabilizing or not is investigated from the decidability viewpoint. We develop a unified strategy through which checking self-stabilization is shown to be decidable for lossy vector addition systems with states, one-counter machines, and conflict-free Petri nets. For lossy counter machines and lossy channel systems, in contrast, the self-stabilization problem is shown to be undecidable.