Static versus dynamic reversibility in CCS
type: Item
instance of: scholarly article
title: Static versus dynamic reversibility in CCS
zbMATH Open document ID: 1475.68126
author: Ivan Lanese
author: Doriana Medić
author: Claudio Antares Mezzina
published in: Acta Informatica
publication date: 2021-04-28T00:00:00Z
full work available at URL: http://hdl.handle.net/11585/739195
review text: This paper is interested in the comparison of two different systems to represent concurrent and reversible computation, RCCS and CCSK. As the authors note in the conclusion, ``while the number of concurrent reversible calculi and languages is increasing, there is very little literature on the relations between them.'' This is unfortunate, as the proliferation can sometimes hide the commonalities and hinder global progress. The two mentioned systems were born with the same goals and similar methodologies, but made different choices as to how the memory of past actions should be stored: on an independent stack for RCCS, or ``embedded'' in the term for CCSK. It has always been suspected that the two calculi were equivalent in a strong sense, and this is what this paper proves, but, as often with ``folklore results'', a lot of work and clarifications were needed to reach this point. Fortunately, the authors carry on this task with a lot of clarity and explanations, making it a pleasure to read their contribution. Among the benefits of this paper lies a certain ``standardization'' of RCCS and CSSK: both calculi have evolved over the time, and this paper takes the time to lay out the systems without ambiguity. Among other variations, RCCS's alpha-conversion and CCSK's tau prefixes are discussed and design choices are made. One of the difficulties of the result is that RCCS's structural congruence is always ``in the way'' of the reductions, and needs a particular treatment, something the authors do with clarity and care. This paper is a must-read for anyone interested in working with either system or curious about possible development for name-passing reversible operator algebra. It is interesting to note that the paper uses a notion of context (p.~11 and p.~20), with and without history: contexts were recently re-investigated in the context of (variations of) RCCS and CCSK, and, surprisingly, led to opposite results [\textit{I. Lanese} and \textit{I. Phillips}, Lect. Note…
reviewed by: Clément Aubert
Mathematics Subject Classification ID: 68Q09
Mathematics Subject Classification ID: 68Q85
zbMATH DE Number: 7340917
zbMATH Keywords: formal semantics
zbMATH Keywords: process algebras
zbMATH Keywords: process calculi
zbMATH Keywords: reversible calculi
zbMATH Keywords: concurrent computation
describes a project that uses: CauDEr
MaRDI profile type: Publication
OpenAlex ID: W2987291980
cites work: Contextual equivalences in configuration structures and reversibility
cites work: A fully abstract semantics for causality in the π-calculus
cites work: Q4733397
cites work: Flow models of distributed computations: Three equivalent semantics for CCS
cites work: Parallel product of event structures
cites work: Event Structure Semantics of Parallel Extrusion in the Pi-Calculus
cites work: A Compositional Semantics for the Reversible p-Calculus
cites work: Rigid Families for the Reversible $$\pi $$ -Calculus
cites work: CONCUR 2004 - Concurrency Theory
cites work: CONCUR 2005 – Concurrency Theory
cites work: Self-assembling trees
cites work: Causal-consistent rollback in a tuple-based language
cites work: Event structure semantics of (controlled) reversible CCS
cites work: Q4274970
cites work: A Verification Technique for Reversible Process Algebra
cites work: Towards Modelling of Local Reversibility
cites work: A Calculus for Local Reversibility
cites work: Irreversibility and Heat Generation in the Computing Process
cites work: Concurrent Flexible Reversibility
cites work: Reversing Higher-Order Pi
cites work: Reversibility in the higher-order \(\pi\)-calculus
cites work: Q4967172
cites work: Cauder: a causal-consistent reversible debugger for Erlang
cites work: Static VS Dynamic Reversibility in CCS
cites work: A parametric framework for reversible \(\pi\)-calculi
cites work: A calculus of communicating systems
cites work: Reversibility and models for concurrency
cites work: A Reversible Process Calculus and the Modelling of the ERK Signalling Pathway
cites work: Reversing algebraic process calculi
Wikidata QID: Q126830393
DOI: 10.1007/S00236-019-00346-6
description: scientific article; zbMATH DE number 7340917