一句话：通过将 CCS 到 Petri 网的编码与因果一致可逆性结合，为可逆 CCS 给出真并发网语义。
可逆 CCS（RCCS）是建立在经典 CCS 之上的可逆通信系统形式模型。已有工作或用带记忆的进程项实现计算回退，或将 RCCS 进程与可逆事件结构直接关联。本文提出另一种抽象模型：从 CCS 到 Petri 网的经典编码出发，应用新近提出的将因果一致可逆性引入 Petri 网的方法，为每个 RCCS 项构造相应的可逆网对应物，从而给出 RCCS 的真并发语义。该语义以 Petri 网为基底，避免直接依赖事件结构，并为可逆计算提供因果一致的并发解释。
Reversible CCS (RCCS) is a well-established, formal model for reversible communicating systems, which has been built on top of the classical Calculus of Communicating Systems (CCS). In its original formulation, each CCS process is equipped with a memory that records its performed actions, which is then used to reverse computations. More recently, abstract models for RCCS have been proposed in the literature, basically, by directly associating RCCS processes with (reversible versions of) event structures. In this paper we propose a different abstract model: starting from one of the well-known encoding of CCS into Petri nets we apply a recently proposed approach to incorporate causally-consistent reversibility to Petri nets, obtaining as result the (reversible) net counterpart of every RCCS term.
@article{paperbot2704,
title = {A Truly Concurrent Semantics for Reversible CCS},
author = {Hernán Melgratti and Claudio Antares Mezzina and G. Michele Pinna},
journal = {Logical Methods in Computer Science},
volume = {Volume 20, Issue 4},
year = {2024},
doi = {10.46298/lmcs-20(4:20)2024}
}