Operational semantics for Petri net components

J.F. Groote, M. Voorhoeve

Research output: Contribution to journalArticleAcademicpeer-review

7 Citations (Scopus)

Abstract

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
JournalTheoretical Computer Science
Volume379
Issue number1-2
DOIs
Publication statusPublished - 2007

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

Cite this