TY - GEN
T1 - Concurrencies in Reversible Concurrent Calculi
AU - Aubert, Clément
N1 - Publisher Copyright:
© 2022, The Author(s), under exclusive license to Springer Nature Switzerland AG.
PY - 2022
Y1 - 2022
N2 - The algebraic specification and representation of networks of agents have been greatly impacted by the study of reversible phenomena: reversible declensions of the calculus of communicating systems (CCSK and RCCS) offer new semantic models, finer congruence relations, original properties, and revisits existing theories and results in a finer light. But much remains to be done: concurrency, a central notion in establishing causal consistency–a crucial property for reversible systems–, was never given a syntactical definition in CCSK. We remedy this gap by leveraging a definition of concurrency developed for forward-only calculi using proved transition systems, and prove that CCSK still enjoys causal consistency for this elegant and syntactical notion of reversible concurrency. We also compare it to a definition of concurrency inspired by reversible π -calculus, discuss its relation with structural congruence, and prove that it can be adapted to any CCS-inspired reversible system and is equivalent—or refines—existing definitions of concurrency for those systems.
AB - The algebraic specification and representation of networks of agents have been greatly impacted by the study of reversible phenomena: reversible declensions of the calculus of communicating systems (CCSK and RCCS) offer new semantic models, finer congruence relations, original properties, and revisits existing theories and results in a finer light. But much remains to be done: concurrency, a central notion in establishing causal consistency–a crucial property for reversible systems–, was never given a syntactical definition in CCSK. We remedy this gap by leveraging a definition of concurrency developed for forward-only calculi using proved transition systems, and prove that CCSK still enjoys causal consistency for this elegant and syntactical notion of reversible concurrency. We also compare it to a definition of concurrency inspired by reversible π -calculus, discuss its relation with structural congruence, and prove that it can be adapted to any CCS-inspired reversible system and is equivalent—or refines—existing definitions of concurrency for those systems.
KW - Concurrency
KW - Formal semantics
KW - Process algebras
UR - http://www.scopus.com/inward/record.url?scp=85134298199&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85134298199&partnerID=8YFLogxK
U2 - 10.1007/978-3-031-09005-9_10
DO - 10.1007/978-3-031-09005-9_10
M3 - Conference contribution
AN - SCOPUS:85134298199
SN - 9783031090042
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 146
EP - 163
BT - Reversible Computation - 14th International Conference, RC 2022, Proceedings
A2 - Mezzina, Claudio Antares
A2 - Podlaski, Krzysztof
PB - Springer Science and Business Media Deutschland GmbH
T2 - 14th International Conference on Reversible Computation, RC 2022
Y2 - 5 July 2022 through 6 July 2022
ER -