Petri网展开的普适性质
Universal Properties of Petri Net Unfoldings
- Inria（法国国家信息与自动化研究所）
- École Normale Supérieure – PSL University（巴黎高等师范学院-PSL大学）
- CNRS（法国国家科学研究中心）
机构由 AI 辅助整理，请以论文原文为准。
AI总结：
本文通过2-范畴方法解决Petri网展开不满足普适性质的问题，提出两种解决方案并建立普适展开，证明展开函子的本质唯一性。
AI中文摘要：
在并发理论中，一个公认的观点是每个Petri网都承认一种展开语义。这是一个表示其可能执行域的外延对象。展开在实际分析和验证中扮演着重要角色。本文关注以下著名问题：虽然展开类似于Petri网范畴中的普适构造，但它通常不能满足预期的普适性质。这是因为展开构造忽略了网的内部对称性。有两种解决方案：使这些对称性显式化以获得弱普适性质（即仅“在对称性下”成立的性质）；或者通过为网的组件分配个体身份来打破对称性。我们回顾了这两种解决方案，并在每种情况下建立了从Petri网到事件结构的普适展开。本文展示了Petri网展开的2-范畴方法。我们证明每种展开语义决定了涉及Petri网和事件结构的2-范畴相对伴随。从这一视角看，上述两种构造可以通过适当的伴随态射在形式上联系起来。我们展示了事件结构的2-稠密性质，该性质蕴含展开函子本质上是唯一的。
英文摘要：
It is an established idea in concurrency theory that every Petri net admits an unfolding semantics. This is a denotational object that represents its domain of possible executions. Unfoldings play an important role in practical analysis and verification. This paper is concerned with the following well-known problem: while the unfolding resembles a universal construction in the category of Petri nets, it generally fails to satisfy the expected universal property. This is because the unfolding construction overlooks the net's internal symmetries. There are two solutions: make these symmetries explicit to obtain a weak universal property (one that holds only ''up to symmetry''); or break the symmetries by assigning individual identities to components of the net. We review these two solutions and establish, in each case, a universal unfolding of Petri nets to event structures. This paper demonstrates a 2-categorical approach to Petri net unfoldings. We show that each unfolding semantics determines a 2-categorical relative adjunction involving Petri nets and event structures. Viewed in this way, the above two constructions can be related formally via an appropriate morphism of adjunctions. We exhibit a 2-density property of event structures which implies that unfolding functors are essentially unique.
