Affiliations: DISCo, Università degli studi di Milano–Bicocca, viale Sarca 336 U14, Milano, Italia. [email protected], [email protected]
Note: [] Address for correspondence: DISCo, Università degli studi di Milano–Bicocca, viale Sarca 336 U14, Milano, Italia
Abstract: 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.
Keywords: Non-sequential processes, partial order semantics, closure operators, orthomodularity
