Petri Nets Based on Lawvere Theories

Understand

We give a definition of $\mathsf{Q}$-net, a generalization of Petri nets based on a Lawvere theory $\mathsf{Q}$, for which many existing variants of Petri nets are a special case.

• This definition is functorial with respect to change in Lawvere theory, and we exploit this to explore the relationships between different kinds of $\mathsf{Q}$-nets.
• To justify our definition of $\mathsf{Q}$-net, we construct a family of adjunctions for each Lawvere theory explicating the way in which $\mathsf{Q}$-nets present free models of $\mathsf{Q}$ in $\mathsf{Cat}$.
• This gives a functorial description of the operational semantics for an arbitrary category of $\mathsf{Q}$-nets.