A Categorical Semantics for Bounded Petri Nets

TL;DR

This paper develops a categorical framework for bounded Petri nets, connecting internal and external semantics through advanced category theory, including comonads and lax functors, ensuring their equivalence.

Contribution

It introduces a novel categorical semantics for bounded Petri nets, unifying internal and external approaches using advanced categorical constructions.

Findings

Internal and external semantics are proven equivalent.

External semantics encode global token properties.

Framework applies to both collective and individual-token Petri nets.

Abstract

We provide a categorical semantics for bounded Petri nets, both in the collective- and individual-token philosophy. In both cases, we describe the process of bounding a net internally, by just constructing new categories of executions of a net using comonads, and externally, using lax-monoidal-lax functors. Our external semantics is non-local, meaning that tokens are endowed with properties that say something about the global state of the net. We then prove, in both cases, that the internal and external constructions are equivalent, by using machinery built on top of the Grothendieck construction. The individual-token case is harder, as it requires a more explicit reliance on abstract methods.