Operational semantics for Petri net components

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.