Enabling Replications and Contexts in Reversible Concurrent Calculus - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Pré-Publication, Document De Travail Année : 2021

Enabling Replications and Contexts in Reversible Concurrent Calculus

Résumé

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.
Fichier principal
Vignette du fichier
2021_03_26_standalone.pdf (366.46 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-03183053 , version 1 (26-03-2021)

Identifiants

Citer

Clément Aubert, Doriana Medić. Enabling Replications and Contexts in Reversible Concurrent Calculus. 2021. ⟨hal-03183053⟩
282 Consultations
47 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More