Compositionality of Systems and Partially Ordered Runs

TL;DR

This paper presents a unified framework for composing and decomposing Petri nets and their runs, demonstrating that the runs of a composed net are the composition of the individual nets' runs.

Contribution

It introduces a formal framework that captures the compositionality of Petri nets and their runs, extending Petri's original concepts from the 1970s.

Findings

The set of runs of a composed net equals the composition of the individual nets' runs.

The framework unifies Petri nets and their behaviors under composition.

Supports modular analysis of distributed systems.

Abstract

In the late 1970s, C.A. Petri introduced partially ordered event occurrences (runs), then called \emph{processes}, as the appropriate model to describe the individual evolutions of distributed systems. Here, we present a unified framework for handling Petri nets and their runs, specifically to compose and decompose them. It is shown that, for nets $M$ and $N$, the set of runs of the composed net $M \bullet N$ equals the composition of the runs of $M$ and $N$.