A Truly Concurrent Semantics for Reversible CCS

TL;DR

This paper introduces a new abstract model for reversible CCS by translating CCS processes into Petri nets with causally-consistent reversibility, offering a novel approach to formalize reversible communicating systems.

Contribution

It presents a novel method to model reversible CCS processes as Petri nets, integrating causally-consistent reversibility directly into the net structure.

Findings

Successfully encodes RCCS processes as Petri nets with reversibility

Provides a new formal framework for reversible communicating systems

Enhances understanding of causality in reversible computations

Abstract

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.