全谷 Petri 网与进程

Joachim Kock

doi:10.1145/3559103

全谷 Petri 网与进程

计算机科学中的逻辑 2023-01-06 v4 代数拓扑组合数学范畴论

作者: Joachim Kock

在 arXiv 上查看 ↗ PDF ↗ DOI ↗

摘要

我们提出一种基于多项式风格有限集构型与 étale 映射的 Petri 网形式化方法。该形式化同时支持 Goltz 与 Reisig 风格的几何语义（进程是从图出发的 étale 映射）以及 Meseguer 与 Montanari 风格的代数语义（就自由着色 prop 而言），并允许如下统一：对 Petri 网 P，P-进程的 Segal 空间被证明是 P 上的自由着色 groupoid 内 prop。还存在一种 à la Winskel 的展开语义，它规避了经典的对称性问题：在新形式化下，每个 Petri 网都承认一个泛展开，后者进而关联一个事件结构和一个 Scott 域。由于一切均以显式集合编码，Petri 网及其进程拥有元素。特别地，个体 token 语义是原生具备的。（集体 token 语义源于相当剧烈的 à la Best-Devillers 商构造，涉及取状态 groupoid 的 π_0。）

关键词

Petri 网进程 étale 映射几何语义代数语义展开个体 token 语义

引用

@article{arxiv.2005.05108,
  title  = {Whole-grain Petri nets and processes},
  author = {Joachim Kock},
  journal= {arXiv preprint arXiv:2005.05108},
  year   = {2023}
}

备注

This 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'

全谷 Petri 网与进程

摘要

关键词

引用

备注

相关论文