On the Encodability of Reversible Process Calculi
For researchers in concurrency theory, this work clarifies the expressive power gap between reversible and irreversible process calculi through formal encoding results.
The paper proves that CCSK, a reversible process calculus, cannot be encoded into forward-only calculi like CCS or π-calculus with strong bisimilarity preservation, but provides encodings under weaker conditions. It establishes a separation theorem and identifies fundamental limitations of reversibility in concurrent models.
Reversibility, allowing one to execute a program not only forwards as usual, but also backwards, has emerged as a main 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 the 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.