HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

On Occurrence Net Semantics of Petri Nets

Stefan Haar 1
1 TRIO - Real time and interoperability
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : This paper investigates structural properties of occurrence (Petri) nets and their interpretation as unfolding semantics of Petri net systems. Occurrence nets (ONs) exhibit three kinds of node relations associated with causal ordering, concurrency, and conflict. We show that ONs can be decomposed in a natural way into substructures in each of which one or two of these relations are empty, namely: branches, trails, choices, lines, cuts certain density properties, i.e. non-empty intersections of substructures as above.On the semantic level, two established, yet non-equival- ent, definitions of unfolding semantics are studied: branching processes (introduced by Engelfriet, Winskel et.al) and branching executions (Vogler). To both, the structural resultsapply, and both support appropriate partialorde- r logics of high expressive power.We present two such logics that can be interpreted over occurrence net semantics of either kind: the branching time logic BLC and a non-branching logic LLC whose frame is composed of choices, i.e. objects representing horizons of mutually exclusive cuts (generalized global states) compatible with the corresponding phase.
Document type :
Complete list of metadata

Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Wednesday, May 24, 2006 - 11:24:57 AM
Last modification on : Friday, February 4, 2022 - 3:30:28 AM
Long-term archiving on: : Sunday, April 4, 2010 - 11:29:07 PM


  • HAL Id : inria-00072949, version 1



Stefan Haar. On Occurrence Net Semantics of Petri Nets. [Research Report] RR-3718, INRIA. 1999. ⟨inria-00072949⟩



Record views


Files downloads