Enabling Replications and Contexts in Reversible Concurrent Calculus

TL;DR

This paper introduces a novel reversible process algebra that addresses limitations in existing formalisms by enabling process replication, context management, and identifier generation without external consultation, enhancing the modeling of reversible concurrent systems.

Contribution

The paper presents a new reversible process algebra with mechanisms for identifier generation, process replication, and context handling, improving upon prior reversible calculi in expressiveness and flexibility.

Findings

A process algebra with internal identifier generation is designed.

The calculus allows new representations of non-determinism and concurrency.

Reversible bisimulations are analyzed and shown not to be congruences in this setting.

Abstract

Existing formalisms for the algebraic specification and representation of networks of reversible agents suffer some shortcomings. Despite multiple attempts, reversible declensions of the Calculus of Communicating Systems (CCS) do not offer satisfactory adaptation of notions that are usual in ''forward-only'' process algebras, such as replication or context. They also seem to fail to leverage possible new features stemming from reversibility, such as the capacity of distinguishing between multiple replications, based on how they replicate the memory mechanism allowing to reverse the computation. Existing formalisms disallow the ''hot-plugging'' of processes during their execution in contexts that also have a past. Finally, they assume the existence of ''eternally fresh'' keys or identifiers that, if implemented poorly, could result in unnecessary bottlenecks and look-ups involving all the threads. In this paper, we begin investigating those issues, by first designing a process algebra endowed with a mechanism to generate identifiers without the need to consult with the other threads. We use this calculus to recast the possible representations of non-determinism in CCS, and as a by-product establish a simple and straightforward definition of concurrency. Our reversible calculus is then proven to satisfy expected properties, and allows to lay out precisely different representations of the replication of a process with a memory. We also observe that none of the reversible bisimulations defined thus far are congruences under our notion of ''reversible'' contexts.