Compositional Semantics of Finite Petri Nets

TL;DR

This paper develops a compositional semantics for finite Petri nets using structure-preserving bisimilarity, ensuring congruence with process algebra operators and capturing causality and concurrency.

Contribution

It introduces a compositional semantics for finite Petri nets based on structure-preserving bisimilarity, which is a congruence respecting causality and concurrency.

Findings

Proves bisimilarity is a congruence for FNM operators

Defines a fully compositional semantics for finite Petri nets

Provides algebraic properties foundational for axiomatization

Abstract

Structure-preserving bisimilarity is a truly concurrent behavioral equivalence for finite Petri nets, which relates markings (of the same size only) generating the same causal nets, hence also the same partial orders of events. The process algebra FNM truly represents all (and only) the finite Petri nets, up to isomorphism. We prove that structure-preserving 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. Moreover, we study some algebraic properties of structure-preserving bisimilarity, that are at the base of a sound (but incomplete) axiomatization over FNM process terms.