Orthomodular Lattices Induced by the Concurrency Relation

TL;DR

This paper explores how certain properties of partially ordered sets, like N-density and K-density, influence the structure of associated orthomodular lattices, especially in models of concurrent computation such as Petri nets.

Contribution

It introduces a construction linking concurrency relations to orthomodular lattices and characterizes conditions under which these lattices are orthomodular, specifically in the context of occurrence nets.

Findings

N-density ensures the associated lattice is orthomodular.

K-density causes causally closed sets to match closure-induced sets.

The framework connects concurrency relations with orthomodular lattice theory.

Abstract

We apply to locally finite partially ordered sets a construction which associates a complete lattice to a given poset; the elements of the lattice are the closed subsets of a closure operator, defined starting from the concurrency relation. We show that, if the partially ordered set satisfies a property of local density, i.e.: N-density, then the associated lattice is also orthomodular. We then consider occurrence nets, introduced by C.A. Petri as models of concurrent computations, and define a family of subsets of the elements of an occurrence net; we call those subsets "causally closed" because they can be seen as subprocesses of the whole net which are, intuitively, closed with respect to the forward and backward local state changes. We show that, when the net is K-dense, the causally closed sets coincide with the closed sets induced by the closure operator defined starting from the concurrency relation. K-density is a property of partially ordered sets introduced by Petri, on the basis of former axiomatizations of special relativity theory.