Explicit Identifiers and Contexts in Reversible Concurrent Calculus

DOI10.1007/978-3-030-79837-6_9MaRDI QIDQ5162607zbMATH OpenOpenAlexFDO

Authors Clément Aubert, Doriana Medić

Publication date 3 November 2021

Published in Reversible Computation (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2103.15623, https://zenodo.org/record/6213597

zbMATH Keywords

context for reversible calculiformal semanticsprocess algebrasprocess calculi

Mathematics Subject Classification ID

Other nonclassical models of computation (68Q09) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Abstract: Existing formalisms for the algebraic specification and representation of networks of reversible agents suffer some shortcomings. Despite multiple attempts, reversible declensions of the Calculus of Communicating Systems (CCS) do not offer satisfactory adaptation of notions that are usual in forward-only process algebras, such as replication or context. They also seem to fail to leverage possible new features stemming from reversibility, such as the capacity of distinguishing between multiple replications, based on how they replicate the memory mechanism allowing to reverse the computation. Existing formalisms disallow the hot-plugging of processes during their execution in contexts that also have a past. Finally, they assume the existence of eternally fresh keys or identifiers that, if implemented poorly, could result in unnecessary bottlenecks and look-ups involving all the threads. In this paper, we begin investigating those issues, by first designing a process algebra endowed with a mechanism to generate identifiers without the need to consult with the other threads. We use this calculus to recast the possible representations of non-determinism in CCS, and as a by-product establish a simple and straightforward definition of concurrency. Our reversible calculus is then proven to satisfy expected properties, and allows to lay out precisely different representations of the replication of a process with a memory. We also observe that none of the reversible bisimulations defined thus far are congruences under our notion of reversible contexts.

Recommendations

• Relative expressiveness of calculi for reversible concurrency
• Towards a Truly Concurrent Semantics for Reversible CCS
• Concurrencies in reversible concurrent calculi
• Towards causal-consistent reversibility of imperative concurrent programs
• Reverse exchange for concurrency and local reasoning
• Abstract interpretation of trace semantics for concurrent calculi
• Causal-consistent replay reversible semantics for message passing concurrent programs
• scientific article; zbMATH DE number 92601
• A modular formalization of reversibility for concurrent models and languages
• The \(\aleph \)-calculus. A declarative model of reversible programming

Cites work

• A calculus of communicating systems
• A compositional semantics for the reversible -calculus
• A Distributed Pi-Calculus
• A parametric framework for reversible \(\pi\)-calculi
• An axiomatic approach to reversible computation
• Axiomatising infinitary probabilistic weak bisimilarity of finite-state behaviours
• Behavioral theory for mobile ambients
• Causal Unfoldings
• CCS: it's not fair! Fair schedulers cannot be implemented in CCS-like languages even under progress and certain fairness assumptions
• Classically-controlled quantum computation
• CONCUR 2004 - Concurrency Theory
• CONCUR 2005 – Concurrency Theory
• Concurrent flexible reversibility
• Contextual equivalences in configuration structures and reversibility
• Domain equations for probabilistic processes
• EFFICIENT PAIRING FUNCTIONS — AND WHY YOU SHOULD CARE
• Event structure semantics of (controlled) reversible CCS
• Foundations of Software Science and Computation Structures
• scientific article; zbMATH DE number 5605072 (Why is no real title available?)
• scientific article; zbMATH DE number 4039251 (Why is no real title available?)
• scientific article; zbMATH DE number 4119615 (Why is no real title available?)
• Introduction to bisimulation and coinduction
• Isomorphism theorems between models of mixed choice
• On Specifying Timeouts
• Reversibility and models for concurrency
• Reversible barbed congruence on configuration structures
• Rigid families for CCS and the -calculus
• Static versus dynamic reversibility in CCS
• Static VS Dynamic Reversibility in CCS
• The -calculus: A theory of mobile processes
• The Applied Pi Calculus

Cited in

(9)

• Processes against tests: on defining contextual equivalences
• Concurrencies in reversible concurrent calculi
• Paraconsistent arithmetic with a local consistency operator and global selfreference
• scientific article; zbMATH DE number 2038705 (Why is no real title available?)
• Replications in reversible concurrent calculi
• Implementation of a reversible distributed calculus
• The correctness of concurrencies in (reversible) concurrent calculi
• An axiomatic theory for reversible computation
• Processes, systems \& tests: defining contextual equivalences

This page was built for publication: Explicit Identifiers and Contexts in Reversible Concurrent Calculus

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