In: Fundamenta Informaticae 43, pages 105-127. 2000.
Abstract: The 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, branches, trails, choices, and alternatives are introduced and studied. All finite systems are shown to satisfy certain density properties, i.e. non-empty intersections of substructures. On the semantic level, partial order logics are 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, Occurence (Petri) nets, Semantics, Partial Order Logics.
Back to the Petri Nets Bibliography