Relative expressiveness of calculi for reversible concurrency

Abstract

A number of formalisms have been proposed to model various approaches to reversibility and to better understand its properties and characteristics. However, the relation between these formalisms has hardly been studied. This paper examines the expressiveness of the causal-consistent reversibility in process algebras CCS and π-calculus. In particular, we show, by means of encodings, that LTSs of two reversible extensions of CCS, Reversible CCS [1] and CCS with Keys [2], are isomorphic up to some structural trans- formations of processes. To study different causal semantics for π-calculus, we devise a uniform framework for reversible π-calculi that is parametric with respect to a data structure that stores information about the extrusion of a name. Depending on the used data structure, different causal seman- tics can be obtained. We show that reversibility induced by our framework when instantiated with three different data structures is causally-consistent and prove a causal correspondence between certain causal semantics and matching instance of the framework.