Static versus dynamic reversibility in CCS
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. Notes Comput. Sci. 12805, 126--143 (2021; Zbl 1476.68097); \textit{C. Aubert} and \textit{D. Medić}, ibid. 12805, 144--162 (2021; Zbl 1476.68093)]. This may be the sign that another paper of the same caliber is needed to restore the mapping between the systems, or that, despite this sound result, the two systems are kind on diverging on their extensions.
- A calculus for local reversibility
- A calculus of communicating systems
- A compositional semantics for the reversible -calculus
- A fully abstract semantics for causality in the π-calculus
- A parametric framework for reversible \(\pi\)-calculi
- A Reversible Process Calculus and the Modelling of the ERK Signalling Pathway
- A verification technique for reversible process algebra
- Cauder: a causal-consistent reversible debugger for Erlang
- Causal-consistent reversibility
- Causal-consistent rollback in a tuple-based language
- CONCUR 2004 - Concurrency Theory
- CONCUR 2005 – Concurrency Theory
- Concurrent flexible reversibility
- Contextual equivalences in configuration structures and reversibility
- Event structure semantics of (controlled) reversible CCS
- Event structure semantics of parallel extrusion in the pi-calculus
- Flow models of distributed computations: Three equivalent semantics for CCS
- scientific article; zbMATH DE number 482761 (Why is no real title available?)
- scientific article; zbMATH DE number 4119615 (Why is no real title available?)
- Irreversibility and Heat Generation in the Computing Process
- Parallel product of event structures
- Reversibility and models for concurrency
- Reversibility in the higher-order \(\pi\)-calculus
- Reversing algebraic process calculi
- Reversing Higher-Order Pi
- Rigid families for the reversible -calculus
- Self-assembling trees
- Static VS Dynamic Reversibility in CCS
- Towards modelling of local reversibility
- Concurrencies in reversible concurrent calculi
- The reversible temporal process language
- General reversibility
- Reversibility and models for concurrency
- Static VS Dynamic Reversibility in CCS
- Towards bridging time and causal reversibility
- scientific article; zbMATH DE number 7559463 (Why is no real title available?)
- Towards a Truly Concurrent Semantics for Reversible CCS
- Forward-reverse observational equivalences in CCSK
- Explicit Identifiers and Contexts in Reversible Concurrent Calculus
- CONCUR 2004 - Concurrency Theory
- Event structure semantics of (controlled) reversible CCS
- Event structure semantics of (controlled) reversible CCS
- Event structures for the reversible early internal \(\pi\)-calculus
- Bridging Causal Reversibility and Time Reversibility: A Stochastic Process Algebraic Approach
- revTPL: The Reversible Temporal Process Language
- Relating reversible Petri nets and reversible event structures, categorically
- Causal reversibility for timed process calculi with lazy/eager durationless actions and time additivity
- Processes, systems \& tests: defining contextual equivalences
- Causal reversibility in nondeterministic process calculi extended with time or probabilities
- Alternative characterizations of hereditary history-preserving bisimilarity via backward ready multisets
- Modal logic characterizations of forward, reverse, and forward-reverse bisimilarities
- Expansion laws for forward-reverse, forward, and reverse bisimilarities via proved encodings
- CRIL: a concurrent reversible intermediate language
- Relating reversible Petri nets and reversible event structures, categorically
- Reversibility in process calculi with nondeterminism and probabilities
- A truly concurrent semantics for reversible CCS
- Reversible computations are computations
This page was built for publication: Static versus dynamic reversibility in CCS
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2022303)
