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

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 N-dense, 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.