Whole-grain Petri nets and processes
Research output: Contribution to journal › Journal article › Research › peer-review
Standard
Whole-grain Petri nets and processes. / Kock, Joachim.
In: Journal of the ACM, Vol. 70, No. 1, 2022, p. 1-58.Research output: Contribution to journal › Journal article › Research › peer-review
Harvard
APA
Vancouver
Author
Bibtex
}
RIS
TY - JOUR
T1 - Whole-grain Petri nets and processes
AU - Kock, Joachim
PY - 2022
Y1 - 2022
N2 - 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.)
AB - 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.)
U2 - 10.1145/3559103
DO - 10.1145/3559103
M3 - Journal article
VL - 70
SP - 1
EP - 58
JO - Journal of the ACM
JF - Journal of the ACM
SN - 0004-5411
IS - 1
ER -
ID: 331493167