Compositionality of Systems and Partially Ordered Runs

TL;DR

This work addresses the challenge of achieving true compositionality in the partial order semantics of Petri nets by introducing net modules with left and right interfaces and a precise composition operator $\bullet$. It substitutes traditional occurrence sequences with partially ordered runs and defines runs as compositions of steps, proving the Composition Theorem: $\operatorname{runs}(M \bullet N) = \operatorname{runs}(M) \bullet \operatorname{runs}(N)$. The paper provides rigorous definitions for net modules, steps, and runs, and demonstrates how modular construction and refinement can be analyzed in a unified framework, ultimately yielding a monoid-like structure for runs. This approach enables modular design and analysis of distributed systems, with potential impact on process management and formal modeling of complex, interconnected Petri-net systems. The framework emphasizes double-faced interfaces and associativity to support scalable, compositional reasoning about system behavior in a rigorous partially ordered setting.

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$.

Figures (16)

• Figure 1: Baker system and vendor system
• Figure 2: The global system composed of the baker system and the vendor system
• Figure 3: Runs of the global system
• Figure 4: Runs of the baker system and the vendor system
• Figure 5: Three system modules

Theorems & Definitions (13)

• definition 1: ordered and labeled set, degree
• definition 2: interface, matching partners, matchfree
• definition 3: net graph
• definition 4: net module, left and right interfaces, interior of module
• definition 5: composition of modules
• definition 6: step of a net module
• definition 7: runs(M)
• definition 8: basic run
• theorem 1
• proof