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.
翻译:可逆CCS(RCCS)是构建于经典通信系统演算(CCS)之上的、一种用于可逆通信系统的成熟形式化模型。在其原始形式中,每个CCS进程配备一个记录其已执行动作的存储器,用于后续计算逆过程。近年来,文献中提出了RCCS的抽象模型,其基本思路是将RCCS进程直接与事件结构的可逆版本相关联。本文提出了一种不同的抽象模型:从CCS到Petri网的经典编码之一出发,我们应用了一种近期提出的方法,将因果一致性可逆性纳入Petri网,从而为每个RCCS项得到对应的可逆网表示。