DROPS

Document

DOI: 10.4230/LIPIcs.CONCUR.2026.41

On the Encodability of Reversible Process Calculi

Authors: Ivan Lanese, Claudio Antares Mezzina, Iain Phillips, Irek Ulidowski, and Shoji Yuen

Published in: LIPIcs, Volume 391, 37th International Conference on Concurrency Theory (CONCUR 2026)

Abstract

Reversibility, allowing one to execute a program not only forwards as usual, but also backwards, has emerged as a fundamental concept in computing, with applications ranging from debugging and fault tolerance to biological and quantum systems. CCSK, a reversible extension of CCS, is a paradigmatic model of reversible concurrent computation. In this paper, we investigate the encodability of CCSK into classical forward-only concurrent models. We establish a separation theorem showing that there is no basic, success-sensitive encoding of CCSK into CCS or the π-calculus, highlighting the strong impact of reversibility on expressive power. We then present an encoding of CCSK processes with only top-level parallel composition into the internal π-calculus, correct up to strong bisimilarity. We also identify a fundamental limitation: no parallel-preserving encoding of CCSK (with arbitrary parallel composition) into the π-calculus can be correct up to strong bisimilarity. Finally, we provide a parallel-preserving encoding correct under a weaker behavioural correspondence: weak mutual simulation. Our findings extend the literature of encodability results to reversible process calculi.

Cite as

Ivan Lanese, Claudio Antares Mezzina, Iain Phillips, Irek Ulidowski, and Shoji Yuen. On the Encodability of Reversible Process Calculi. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 41:1-41:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{lanese_et_al:LIPIcs.CONCUR.2026.41,
  author =	{Lanese, Ivan and Mezzina, Claudio Antares and Phillips, Iain and Ulidowski, Irek and Yuen, Shoji},
  title =	{{On the Encodability of Reversible Process Calculi}},
  booktitle =	{37th International Conference on Concurrency Theory (CONCUR 2026)},
  pages =	{41:1--41:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-447-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{391},
  editor =	{Sokolova, Ana and Totzke, Patrick},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.41},
  URN =		{urn:nbn:de:0030-drops-273715},
  doi =		{10.4230/LIPIcs.CONCUR.2026.41},
  annote =	{Keywords: Reversible computation, Process calculi, Encodings, Impossibility results}
}

Search Results

Documents authored by Mezzina, Claudio Antares

On the Encodability of Reversible Process Calculi

Abstract

Cite as

Thanks for your feedback!

Could not send message