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