Affiliations: Département d'Informatique, École Normale Supérieure, Paris, France. Email: Stefan.Haar@ens.fr
Note: [] Supported by the European TMR project ALAPEDES, Contract Ref. ERB-FMRX-CT-96-0074 Address for correspondence: Département d'Informatique, École Normale Supérieure, Paris, France
Abstract: This paper investigates Occurrence (Petri) Nets on two levels: their structural theory and their interpretation in branching unfolding semantics of Petri Net systems. The key issue is the decomposition of occurrence nets into substructures given by the node relations associated with causal ordering, concurrency, and conflict. In addition to lines and cuts, which have long been studied in the context of causal nets ([1]), we introduce and study branches, trails, choices, and alternatives. All finite systems will be shown to satisfy certain density properties, i.e. non-empty intersections of substructures as above. On the semantic level, we introduce partial order logics to be interpreted on two different kind of frames, given by substructures of occurrence nets: on the frame of cuts, the CTL* type logics BFC and BLC, and the “non-branching” logic LLC, taylored to the frame given by the lattice of choices.
Keywords: Concurrency, Occurrence (Petri) nets, Semantics, Partial Order Logics
