Compositional Net Semantics up to Step Net Bisimilarity

TL;DR

This paper introduces a compositional semantics for finite Petri nets based on step net bisimilarity, ensuring congruence with process algebra operators and preserving causality and branching structures.

Contribution

It proves that step net bisimilarity is a congruence for FNM operators, enabling a compositional semantics that fully respects causality and branching in finite Petri nets.

Findings

Step net bisimilarity is a congruence for FNM operators.

A compositional semantics for finite Petri nets is established.

The semantics respects causality and branching structures.

Abstract

Step net bisimilarity \cite{Gor23} is a truly concurrent behavioral equivalence for finite Petri nets, which is defined as a smooth generalization of standard step bisimilarity \cite{NT84} on Petri nets, but with the property of relating markings (of the same size only) generating the same partial orders of events. The process algebra FNM \cite{Gor17} truly represents all (and only) the finite Petri nets, up to isomorphism. We prove that step net bisimilarity is a congruence w.r.t. the FMN operators, In this way, we have defined a compositional semantics, fully respecting causality and the branching structure of systems, for the class of all the finite Petri nets.