Concurrencies in Reversible Concurrent Calculi

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.

Original languageEnglish (US)
Title of host publicationReversible Computation - 14th International Conference, RC 2022, Proceedings
EditorsClaudio Antares Mezzina, Krzysztof Podlaski
PublisherSpringer Science and Business Media Deutschland GmbH
Number of pages18
ISBN (Print)9783031090042
StatePublished - 2022
Event14th International Conference on Reversible Computation, RC 2022 - Urbino, Italy
Duration: Jul 5 2022Jul 6 2022

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume13354 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference14th International Conference on Reversible Computation, RC 2022


  • Concurrency
  • Formal semantics
  • Process algebras

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'Concurrencies in Reversible Concurrent Calculi'. Together they form a unique fingerprint.

Cite this