A Categorical Semantics for Bounded Petri Nets

Fabrizio Romano Genovese
(University of Pisa, Statebox)
Fosco Loregian
(Tallinn University of Technology)
Daniele Palombi
(Sapienza University of Rome)

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.

In Kohei Kishida: Proceedings of the Fourth International Conference on Applied Category Theory (ACT 2021), Cambridge, United Kingdom, 12-16th July 2021, Electronic Proceedings in Theoretical Computer Science 372, pp. 59–71.
Published: 3rd November 2022.

ArXived at: http://dx.doi.org/10.4204/EPTCS.372.5 bibtex PDF

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org