Open Petri Nets

TL;DR

This paper develops a categorical framework for open Petri nets, enabling compositional analysis of their operational behaviors and reachability properties through symmetric monoidal double categories and functors.

Contribution

It introduces a novel categorical structure for open Petri nets and provides two semantics—operational and reachability—using symmetric monoidal double functors.

Findings

Operates within a symmetric monoidal double category framework.

Provides compositional semantics for open Petri nets.

Enables modular analysis of Petri net processes and reachability.

Abstract

The reachability semantics for Petri nets can be studied using open Petri nets. For us an "open" Petri net is one with certain places designated as inputs and outputs via a cospan of sets. We can compose open Petri nets by gluing the outputs of one to the inputs of another. Open Petri nets can be treated as morphisms of a category $\mathsf{Open}(\mathsf{Petri})$, which becomes symmetric monoidal under disjoint union. However, since the composite of open Petri nets is defined only up to isomorphism, it is better to treat them as morphisms of a symmetric monoidal double category $\mathbb{O}\mathbf{pen}(\mathsf{Petri})$. We describe two forms of semantics for open Petri nets using symmetric monoidal double functors out of $\mathbb{O}\mathbf{pen}(\mathsf{Petri})$. The first, an operational semantics, gives for each open Petri net a category whose morphisms are the processes that this net can carry out. This is done in a compositional way, so that these categories can be computed on smaller subnets and then glued together. The second, a reachability semantics, simply says which markings of the outputs can be reached from a given marking of the inputs.