On the encodability of reversible process calculi
File(s)
Accepted version
Author(s)
Lanese, Ivan
Mezzina, Claudio Antares
Phillips, Iain
Ulidowski, Irek
Yuen, Shoji
Type
Conference Paper
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.
Date Acceptance
2026-06-15
Citation
Leibniz International Proceedings in Informatics
ISSN
1868-8969
Publisher
Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
Journal / Book Title
Leibniz International Proceedings in Informatics
Copyright Statement
Subject to copyright. This paper is embargoed until publication. Once published the Version of Record (VoR) will be available on immediate open access.
Source
37th International Conference on Concurrency Theory (CONCUR 2026)
Publication Status
Accepted
Start Date
2026-09-01
Finish Date
2026-09-05
Coverage Spatial
Liverpool, UK