Operational semantics for Petri net components

Jan Friso Groote, Marc Voorhoeve

Research output: Contribution to journalArticleAcademicpeer-review

7 Citations (Scopus)


We propose a calculus for marked labelled nets (components), with places and transitions as atoms and merge, addition, fusion and relabelling as operators. The operators are defined using graph-based transformations; each net can be represented by a term. Next, we define both a step semantics for nets and a Plotkin-style SOS semantics for net terms and show their equivalence. In the semantics, both state-oriented and event-oriented properties of components can be expressed. We give a few rules for reducing components to smaller equivalent ones. Keywords: Semantics; Petri nets; Process algebra; Bisimulation; Modelling; Verification
Original languageEnglish
Pages (from-to)1-19
Number of pages19
JournalTheoretical Computer Science
Issue number1-2
Publication statusPublished - 2007


Dive into the research topics of 'Operational semantics for Petri net components'. Together they form a unique fingerprint.

Cite this