2026-08-25T22:08:59Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:27371 2026-08-24T14:08:31Z ddc:004 open_access

On the Encodability of Reversible Process Calculi Lanese, Ivan Mezzina, Claudio Antares Phillips, Iain Ulidowski, Irek Yuen, Shoji Reversible computation Process calculi Encodings Impossibility results 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Ivan Lanese and Claudio Antares Mezzina and Iain Phillips and Irek Ulidowski and Shoji Yuen 2026 Is Part Of LIPIcs, Volume 391, 37th International Conference on Concurrency Theory (CONCUR 2026) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CONCUR.2026.41 urn:nbn:de:0030-drops-273715 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.41 eng https://creativecommons.org/licenses/by/4.0/legalcode