Wyniki wyszukiwania - BazTech

1

Closed Sets in Occurrence Nets with Conflicts

Bernardinello L., Ferigato C., Haar S., Pomello L.

Fundamenta Informaticae

|

2014

|

Vol. 133, nr 4

323--344

EN

The semantics of concurrent processes can be defined in terms of partially ordered sets. Occurrence nets, which belong to the family of Petri nets, model concurrent processes as partially ordered sets of occurrences of local states and local events. On the basis of the associated concurrency relation, a closure operator can be defined, giving rise to a lattice of closed sets. Extending previous results along this line, the present paper studies occurrence nets with forward conflicts, modelling families of processes. It is shown that the lattice of closed sets is orthomodular, and the relations between closed sets and some particular substructures of an occurrence net are studied. In particular, the paper deals with runs, modelling concurrent histories, and trails, corresponding to possible histories of sequential components. A second closure operator is then defined by means of an iterative procedure. The corresponding closed sets, here called ‘dynamically closed’, are shown to form a complete lattice, which in general is not orthocomplemented. Finally, it is shown that, if an occurrence net satisfies a property called B-density, which essentially says that any antichain meets any trail, then the two notions of closed set coincide, and they form a complete, algebraic orthomodular lattice.

2

Closure Operators and Lattices Derived from Concurrency in Posets and Occurrence Nets

Bernardinello L., Pomello L., Rombola S.

Fundamenta Informaticae

|

2011

|

Vol. 105, nr 3

211-235

EN

Partially ordered sets (posets), and among them occurrence nets, are a natural formal tool for studying concurrent processes. In a poset, the concurrency relation between elements is explicit. Starting from this relation, and applying standard techniques of lattice theory, one can build a complete lattice whose elements are subsets of the given poset. We study structural properties of such closed subsets, and of the lattice they form. In particular, we show that, if a poset is Ndense, then the lattice of closed subsets is orthomodular. A characterization of K-density, valid for posets, is given on the basis of a relation between lines, or chains, and closed sets. In the case of occurrence nets, we give a characterization of the closed subsets, and define the related notion of "causally closed subset"; a constructive characterization of such subsets is given, which justifies their interpretation as causally closed subprocesses of the occurrence net. We show that, for K-dense occurrence nets, closed subsets and causally closed subsets coincide. By using causally closed subsets, we give another characterization of K-density, related to the algebraicity of the lattice of closed sets.

3

Time in State Machines

Graf S., Prinz A.

Fundamenta Informaticae

|

2007

|

Vol. 77, nr 1,2

143-174

EN

State machines are a very general means to express computations in an implementation-independent way. There are ways to extend the abstract state machine (ASM) framework with distribution aspects, but there is no unifying framework for handling time so far. We propose event structures extended with time as a natural framework for representing state machines and their true concurrency model at a semantic level and for discussing associated time models. Constraints on these timed event structures and their traces (runs) are then used for characterising different frameworks for timed computations. This characterisation of timed frameworks is independent of ASM and allows to compare time models of different modelling formalisms. Finally, we propose some specific extensions of ASM for the expressions of time constraints in accordance with the event-based semantic framework and show the applicability of the obtained framework on an example with a standard time model and a set of consistency properties for timed computations.