A truly concurrent semantics for reversible CCS

DOI10.46298/LMCS-20(4:20)2024MaRDI QIDQ7034608zbMATH OpenFDO

Authors Hernan Melgratti, Claudio Antares Mezzina, G. Michele Pinna

Publication date 31 January 2025

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.46298/LMCS-20(4:20)2024

zbMATH Keywords

occurrence netsreversible CCStruly concurrent semanticsunravel nets

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Review text

Reversible CCS (RCCS) is a formal model for reversible communicating systems, built upon the classical Calculus of Communicating Systems (CCS). In RCCS each process is equipped with a memory that records its performed actions. This memory is then used to reverse computations, effectively incorporating a logging mechanism into the operational semantics of CCS that enables the undoing of computation steps. In the paper, CCS processes are encoded into a mild generalization of occurrence nets. It is shown that unravel nets can be made causally consistent and reversible. Finally, it is shown that these reversible unravel nets provide an interpretation of RCCS terms, and hence a truly concurrent semantics for RCCS is provided.

Cites work

• A calculus of communicating systems
• A compositional semantics for the reversible -calculus
• A distributed operational semantics of CCS based on condition/event systems
• A distributed operational view of reversible prime event structures
• A reversible perspective on Petri nets and event structures
• A verification technique for reversible process algebra
• Causal ambiguity and partial orders in event structures
• CONCUR 2004 - Concurrency Theory
• Concurrencies in reversible concurrent calculi
• Distributed semantics for the \(\pi \)-calculus based on Petri nets with inhibitor ARCS
• Event structure semantics of (controlled) reversible CCS
• Event structure semantics of (controlled) reversible CCS
• Flow models of distributed computations: Three equivalent semantics for CCS
• Fundamental properties of infinite trees
• scientific article; zbMATH DE number 4018370 (Why is no real title available?)
• scientific article; zbMATH DE number 3885321 (Why is no real title available?)
• scientific article; zbMATH DE number 4119660 (Why is no real title available?)
• scientific article; zbMATH DE number 7559463 (Why is no real title available?)
• Petri nets, event structures and domains. I
• Proved trees
• Relating reversible Petri nets and reversible event structures, categorically
• Reversibility in the higher-order \(\pi\)-calculus
• Reversible occurrence nets and causal reversible prime event structures
• Reversing algebraic process calculi
• Reversing place transition nets
• Rigid families for the reversible -calculus
• Semantics of systems of concurrent processes. LITP Spring School on theoretical computer science, La Roche Posay, France, 23-27 April 1990. Proceedings
• Static versus dynamic reversibility in CCS
• The correctness of concurrencies in (reversible) concurrent calculi
• Towards a Truly Concurrent Semantics for Reversible CCS
• Types and programing languages

Cited in

(2)

• Relating reversible Petri nets and reversible event structures, categorically
• Reversible computations are computations

This page was built for publication: A truly concurrent semantics for reversible CCS

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q7034608)