Open Petri Nets

Jade Master (UC Riverside), John Baez (UC Riverside)

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 $\open(\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 \emph{double} category $\Open(\Petri)$. Various choices of semantics for open Petri nets can be described using symmetric monoidal double functors out of $\Open(\Petri)$. Here we describe the reachability semantics, which assigns to each open Petri net the relation saying which markings of the outputs can be obtained from a given marking of the inputs via a sequence of transitions. We show this semantics gives a symmetric monoidal lax double functor from $\Open(\Petri)$ to the double category of relations. A key step in the proof is to treat Petri nets as presentations of symmetric monoidal categories; for this we use the work of Meseguer, Montanari, Sassone and others.