TY - GEN
T1 - Explicit Identifiers and Contexts in Reversible Concurrent Calculus
AU - Aubert, Clément
AU - Medić, Doriana
N1 - Funding Information:
This work has been supported by French ANR project DCore ANR-18-CE25-0007.
Publisher Copyright:
© 2021, Springer Nature Switzerland AG.
PY - 2021
Y1 - 2021
N2 - 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.
AB - 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.
KW - Context for reversible calculi
KW - Formal semantics
KW - Process algebras and calculi
UR - http://www.scopus.com/inward/record.url?scp=85111993700&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85111993700&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-79837-6_9
DO - 10.1007/978-3-030-79837-6_9
M3 - Conference contribution
AN - SCOPUS:85111993700
SN - 9783030798369
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 144
EP - 162
BT - Reversible Computation 13th International - 13th International Conference, RC 2021, Proceedings
A2 - Yamashita, Shigeru
A2 - Yokoyama, Tetsuo
PB - Springer Science and Business Media Deutschland GmbH
T2 - 13th International Conference on Reversible Computation, RC 2021
Y2 - 7 July 2021 through 8 July 2021
ER -