×

Closed sets in occurrence nets with conflicts. (English) Zbl 1315.68189

Summary: 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.

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
06A15 Galois correspondences, closure operators (in relation to ordered sets)
06C15 Complemented lattices, orthocomplemented lattices and posets
68Q55 Semantics in the theory of computing
Full Text: DOI