Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Truly Concurrent Semantics for Reversible CCS

Hernán Melgratti, Claudio Antares Mezzina, G. Michele Pinna

TL;DR

The paper addresses the challenge of giving RCCS a truly concurrent semantics by encoding CCS processes into unravel nets and then enriching them to reversible unravel nets, thereby embedding RCCS history directly into the net structure. The authors develop a direct, net-based encoding that preserves causality and reversibility, prove a forward-reverse bisimulation between RCCS terms and the resulting reversible nets, and extend the approach to infinite/coinductive processes. A practical Haskell implementation demonstrates the viability of the encoding and simulation, highlighting the potential for scalable, truly concurrent reversible models. This work advances the integration of reversible process calculi with Petri-net semantics, enabling robust, concurrent reasoning about reversible computations in distributed systems.

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.

A Truly Concurrent Semantics for Reversible CCS

TL;DR

The paper addresses the challenge of giving RCCS a truly concurrent semantics by encoding CCS processes into unravel nets and then enriching them to reversible unravel nets, thereby embedding RCCS history directly into the net structure. The authors develop a direct, net-based encoding that preserves causality and reversibility, prove a forward-reverse bisimulation between RCCS terms and the resulting reversible nets, and extend the approach to infinite/coinductive processes. A practical Haskell implementation demonstrates the viability of the encoding and simulation, highlighting the potential for scalable, truly concurrent reversible models. This work advances the integration of reversible process calculi with Petri-net semantics, enabling robust, concurrent reasoning about reversible computations in distributed systems.

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.
Paper Structure (19 sections, 14 theorems, 34 equations, 16 figures)

This paper contains 19 sections, 14 theorems, 34 equations, 16 figures.

Table of Contents

  1. Introduction
  2. Organization of the paper.
  3. CCS and reversible CCS
  4. Reversible CCS
  5. Petri nets, Unravel Nets and Reversible Unravel Nets
  6. Petri nets
  7. Unravel nets.
  8. Reversible unravel nets.
  9. CCS processes as unravel nets
  10. Encoding of CCS processes
  11. Encoding of RCCS processes
  12. Correctness result
  13. Conclusions and future works
  14. Implementation
  15. Representation of infinite nets
  16. ...and 4 more sections

Key Result

Lemma 2.6

Let $R$ be a coherent process. For any forward transition $R \xrightarrow{{\hat{m}}:{\alpha}} S$ there exists a backward transition $S \mathrel{\begin{tikzpicture}[baseline= {( $ (current bounding box.south) + (0,-0.5ex) $ )}] \node[inner sep=.5ex] (6) {$ {\hat{m}}:{\alpha}$}; \path[draw,<-,decorate

Figures (16)

  • Figure 1: Encoding of $R = \langle\rangle\triangleright a.\mathsf{0}$
  • Figure 2: CCS Syntax
  • Figure 3: CCS semantics
  • Figure 4: RCCS syntax
  • Figure 5: RCCS semantics
  • ...and 11 more figures

Theorems & Definitions (50)

  • Definition 2.1: CCS Semantics
  • Definition 2.2
  • Definition 2.3
  • Definition 2.4
  • Example 2.5
  • Lemma 2.6: Loop Lemma rccs
  • Corollary 2.7
  • Definition 2.9
  • Definition 3.1
  • Definition 3.2
  • ...and 40 more