paperbot · PL 论文追踪

全部论文 待读 收藏

P2 A distributed operational view of Reversible Prime Event Structures

可逆素事件结构的分布式操作视角
LICS 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)2021匹配度 1/10 · 论文属于并发语义与可逆事件结构的纯形式化理论工作,讨论可逆素事件结构与可逆因果网之间的操作对应,与用户关注的静态分析、LLM/Agent、浮点程序分析及贝叶斯程序分析均无直接交叉。虽同属形式化方法/程序语言理论大类,但不在研究方向核心范围内。引用 9 inbox
Hernan Melgratti, Claudio Antares Mezzina, G. Michele Pinna
crossref: 2026-09-12

AI 速览

一句话:给出可逆素事件结构的操作刻画,并证明其对应于一类可逆因果网。

可逆素事件结构是对素事件结构的扩展,用于抽象描述能够撤销计算步骤的过程;事件结构长期被用于连接操作模型(Petri网、进程演算)与指称模型。此前仅对满足因果尊重的子类给出了操作对应。本文为完整的可逆素事件结构给出操作刻画,证明它们对应于上下文Petri网的一个子类——可逆因果网。可逆因果网的独特之处在于,因果关系由抑制弧而非变迁后集与前集的重叠恢复,从而能够从操作层面解释违反因果顺序的可逆性。

问题
可逆素事件结构的操作对应模型是什么,尤其是如何刻画不遵守因果顺序的可逆性。
方法
为完整模型构造操作语义,并引入可逆因果网这一上下文Petri网子类,利用抑制弧恢复因果关系。
评估
通过理论构造与证明建立可逆素事件结构与可逆因果网之间的对应关系,属于形式化理论结果而非实证评估。
原文摘要(Abstract)

Reversible prime event structures extend the well-known model of prime event structures to represent reversible computational processes. Essentially, they give abstract descriptions of processes capable of undoing computation steps. Since their introduction, event structures have played a pivotal role in connecting operational models (traditionally, Petri nets and process calculi) with denotational ones (algebraic domains). For this reason, there has been a lot of interest in linking different classes of operational models with different kinds of event structures. Hence, it is natural to ask which is the operational counterpart of reversible prime event structures. Such question has been previously addressed for a subclass of reversible prime event structures in which the interplay between causality and reversibility is restricted to the so-called cause-respecting reversible structures. In this paper, we present an operational characterisation of the full-fledged model and show that reversible prime event structures correspond to a subclass of contextual Petri nets, called reversible causal nets. The distinctive feature of reversible causal nets is that causality is recovered from inhibitor arcs instead of the usual overlap between post and presets of transitions. In this way, we are able to operationally explain also out-of-causal order reversibility.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@inproceedings{paperbot6225,
  title = {A distributed operational view of Reversible Prime Event Structures},
  author = {Hernan Melgratti and Claudio Antares Mezzina and G. Michele Pinna},
  booktitle = {LICS},
  year = {2021},
  doi = {10.1109/lics52264.2021.9470623}
}