Whole-grain Petri nets and processes
arXiv:2005.05108 · doi:10.1145/3559103
Abstract
We present a formalism for Petri nets based on polynomial-style finite-set configurations and etale maps. The formalism supports both a geometric semantics in the style of Goltz and Reisig (processes are etale maps from graphs) and an algebraic semantics in the style of Meseguer and Montanari, in terms of free coloured props, and allows the following unification: for P a Petri net, the Segal space of P-processes is shown to be the free coloured prop-in-groupoids on P. There is also an unfolding semantics à la Winskel, which bypasses the classical symmetry problems: with the new formalism, every Petri net admits a universal unfolding, which in turn has associated an event structure and a Scott domain. Since everything is encoded with explicit sets, Petri nets and their processes have elements. In particular, individual-token semantics is native. (Collective-token semantics emerges from rather drastic quotient constructions à la Best-Devillers, involving taking π_0 of the groupoids of states.)
arXiv commentThis is the final 'author version', nearly identical to the version published in JACM. 58 pages. This paper previously had the title 'Elements of Petri nets and processes'
References in corpus (16)
- Polynomial functors and polynomial monads
- Configuration Structures, Event Structures and Petri Nets
- Decomposition spaces, incidence algebras and Möbius inversion I: basic theory
- Homotopy theory for algebras over polynomial monads
- A Compositional Framework for Reaction Networks
- Open Petri Nets
- Decomposition spaces, incidence algebras and Möbius inversion II: completeness, length filtration, and finiteness
- Being Van Kampen is a universal property
- Homotopy linear algebra
- Categorical Data Structures for Technical Computing
- Decomposition spaces and restriction species
- An Algebraic Framework for Structured Epidemic Modeling
- Internal algebra classifiers as codescent objects of crossed internal categories
- Computational Petri Nets: Adjunctions Considered Harmful
- Petri Nets Based on Lawvere Theories
- Cospan construction of the graph category of Borisov and Manin