Published in

Springer Verlag, Lecture Notes in Computer Science, p. 144-162, 2021

DOI: 10.1007/978-3-030-79837-6_9



Export citation

Search in Google Scholar

Explicit Identifiers and Contexts in Reversible Concurrent Calculus

Book chapter published in 2021 by Clément Aubert ORCID, Doriana Medić ORCID
This paper is available in a repository.
This paper is available in a repository.

Full text: Download

Green circle
Preprint: archiving allowed
Green circle
Postprint: archiving allowed
Red circle
Published version: archiving forbidden
Data provided by SHERPA/RoMEO


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 usual in “forward-only” process algebras, such as replication or context. Existing formalisms disallow the “hot-plugging” of processes during their execution in contexts with their own past. They also 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. We also observe that none of the reversible bisimulations defined thus far are congruences under our notion of “reversible” contexts.