Relative expressiveness of calculi for reversible concurrency

The main motivations for studying reversible computing comesfrom the promise that reversible computation (and circuits)would lead to more energy efficient computers. Besides circuits, nowadays, reversibility is studied in many other domains. This thesis studies the expressiveness of the causalconsistent reversibility (a well-known notion of reversibilityfor concurrent systems) in CCS and π-calculus.First, we show that by means of encodings, LTSs of ReversibleCCS (introduced by Danos and Krivine) and CCS with Communications Keys (introduced by Phillips and Ulidowski) areisomorphic up to some structural transformations of processes.An explanation of this result is the existence of one causalitynotion in CCS.In π-calculus, two forms of dependences between the actionsgive rise to different causal semantics. The main difference ishow the parallel extrusion of the same name is treated. Weconsider three approaches to parallel extrusion problem represented with causal semantics introduced by Boreale et al;Crafa et al; and Cristescu et al. To study them, we devise aframework for reversible π-calculi, parametric with respect tothe data structure used to keep track of information about aname extrusions. We show that reversibility induced by ourframework is causally-consistent and prove causal correspondence between the semantics given by Boreale et al, and thecorresponding instance of the framework.