带持久性的Petri网的事件结构
摘要：并发事件结构是一个被广泛接受的并发模型。在Nielsen、Plotkin和Winskel的划时代论文中，它们被用来建立起域论和Petri提出的并发方法之间的桥梁。其中一个基本的作用是通过将（安全的）Petri网映射到一个称为“prime event structures”的事件结构子类中来进行展开构造，其中每个事件具有一个唯一确定的因果集合。转而，可以将“prime event structures”与它的配置域进行等同处理。在范畴论的层面上，Winskel将其很好地形式化为一系列coreflections的链式关系。 与“prime event structures”相反，一般的事件结构允许存在多个因果选择，即事件可以由不同的最小事件集合激活。在本文中，我们扩展了Petri网和事件结构之间的连接，以包括多个因果选择。特别地，我们表明，在网的层面上，多个因果选择可以通过持久位置很好地解释。这些位置是一次生成多个令牌可以多次使用而不被消耗的地方，并且可以集体解释多个令牌，即它们的历史记录是无关紧要的。通过基于展开构造的一系列coreflections，将带持久性的Petri网与一种新的一般事件结构子类“locally connected”相关联。
作者：Paolo Baldan, Roberto Bruni, Andrea Corradini, Fabio Gadducci, Hernan Melgratti, and Ugo Montanari
论文ID：1802.03726
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22