pith. sign in

arxiv: 2606.25916 · v1 · pith:YJDLJKUNnew · submitted 2026-06-24 · 💻 cs.LO

On the Encodability of Reversible Process Calculi

Ivan Lanese , Claudio Antares Mezzina , Iain Phillips , Irek Ulidowski , Shoji Yuen This is my paper

Pith reviewed 2026-06-25 18:58 UTC · model grok-4.3

classification 💻 cs.LO
keywords reversible calculiencodabilityCCSKCCSpi-calculusbisimilarityseparation results
0
0 comments X

The pith

Reversibility prevents basic encoding of CCSK into CCS or the π-calculus.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper shows that CCSK, a reversible extension of CCS, cannot be encoded into non-reversible models like CCS or the π-calculus under standard encodability criteria. Specifically, there is no basic, success-sensitive encoding, and no parallel-preserving encoding correct up to strong bisimilarity. This demonstrates that reversibility introduces new expressive capabilities related to history and compensation that forward calculi cannot simulate. Positive encodings exist for restricted cases and under weaker equivalences.

Core claim

There is no basic, success-sensitive encoding of CCSK into CCS or the π-calculus, and no parallel-preserving encoding of CCSK into the π-calculus is correct up to strong bisimilarity, although encodings exist for top-level parallel composition into the internal π-calculus and under weak mutual simulation.

What carries the argument

The definitions of basic encoding, success-sensitivity, and parallel-preservation when applied to the reversible history and compensation in CCSK.

If this is right

  • Reversibility increases the expressive power of concurrent models beyond what CCS and π-calculus can express.
  • Encodings of reversible processes must account for history preservation in specific ways.
  • Weaker behavioral relations allow more encodings than strong bisimilarity.
  • Restricted forms of CCSK can be encoded into internal π-calculus.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The results may extend to other reversible calculi, suggesting dedicated support for reversibility is needed in implementations.
  • This could impact the design of reversible debuggers or fault-tolerant systems by requiring new primitives.
  • Testing by relaxing the encoding criteria could reveal boundary cases where encodings become possible.

Load-bearing premise

The specific definitions of basic, success-sensitive, and parallel-preserving encodings are what make the separation hold; changing them might allow encodings.

What would settle it

An explicit construction of a basic success-sensitive encoding from CCSK to CCS that satisfies the criteria would disprove the no-encoding result.

Figures

Figures reproduced from arXiv: 2606.25916 by Claudio Antares Mezzina, Iain Phillips, Irek Ulidowski, Ivan Lanese, Shoji Yuen.

Figure 3
Figure 3. Figure 3: π-calculus early labelled transition system. The semantics of the π-calculus is given by the labelled transition system (Procπ, Actπ, −→π ), where −→π ⊆ Procπ × Actπ × Procπ is the smallest transition relation closed under the rules of [PITH_FULL_IMAGE:figures/full_fig_p006_3.png] view at source ↗
read the original abstract

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 {\pi}-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 {\pi}-calculus, correct up to strong bisimilarity. We also identify a fundamental limitation: no parallel-preserving encoding of CCSK (with arbitrary parallel composition) into the {\pi}-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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper claims that CCSK, a reversible extension of CCS, cannot be encoded into CCS or the π-calculus under the criteria of basic success-sensitive encodings, and that no parallel-preserving encoding into the π-calculus exists that is correct up to strong bisimilarity. It provides a positive encoding of CCSK processes with only top-level parallel composition into the internal π-calculus up to strong bisimilarity, and a parallel-preserving encoding into the π-calculus that is correct up to weak mutual simulation.

Significance. If the separation and encoding results hold under the stated criteria, they extend the encodability literature by quantifying the expressive impact of reversibility (history and compensation) in concurrent models. The manuscript earns credit for stating both impossibility results and conditional positive encodings, and for explicitly noting dependence on the chosen notions of encoding.

major comments (2)
  1. [Definitions of encoding criteria (likely §2–3)] The separation theorems rest on the definitions of 'basic', 'success-sensitive', and 'parallel-preserving' encodings and how they interact with CCSK's reversible history and compensation. The abstract states that the results depend on these notions, but without an explicit check that the standard criteria (lifted from forward-only calculi) correctly observe backward transitions, the negative claims risk being sensitive to minor reformulations of observability.
  2. [Theorem on basic success-sensitive encoding] The claim of no basic success-sensitive encoding into CCS or π-calculus is load-bearing for the main separation result. The manuscript should verify in the relevant theorem statement whether the success predicate is defined uniformly for reversible and non-reversible processes, as any post-hoc adjustment to success observability would invalidate the impossibility.
minor comments (2)
  1. [Preliminaries] Notation for history stacks and compensation in CCSK should be introduced with a small example before the encodability criteria are applied.
  2. [Encoding results] The distinction between strong bisimilarity and weak mutual simulation is used in the positive results; a brief comparison table would clarify the behavioural gap.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful reading and constructive comments on our manuscript. We address each major comment below.

read point-by-point responses

  1. Referee: [Definitions of encoding criteria (likely §2–3)] The separation theorems rest on the definitions of 'basic', 'success-sensitive', and 'parallel-preserving' encodings and how they interact with CCSK's reversible history and compensation. The abstract states that the results depend on these notions, but without an explicit check that the standard criteria (lifted from forward-only calculi) correctly observe backward transitions, the negative claims risk being sensitive to minor reformulations of observability.

    Authors: The criteria in Section 2 are formulated to require that encodings preserve (or reflect) both forward and backward transitions, with success-sensitivity defined solely via the observable success action. This application is symmetric by construction and does not rely on forward-only assumptions. To make the robustness explicit, we will insert a short clarifying paragraph in Section 2 of the revised manuscript. revision: yes

  2. Referee: [Theorem on basic success-sensitive encoding] The claim of no basic success-sensitive encoding into CCS or π-calculus is load-bearing for the main separation result. The manuscript should verify in the relevant theorem statement whether the success predicate is defined uniformly for reversible and non-reversible processes, as any post-hoc adjustment to success observability would invalidate the impossibility.

    Authors: The success predicate is defined uniformly in Definition 2.3 as the capability to perform the distinguished success action, without reference to reversibility. This definition is used consistently in the proofs. We will update the statement of the separation theorem to include an explicit clause confirming uniformity of the success predicate. revision: yes

Circularity Check

0 steps flagged

No circularity: separation results rest on externally defined standard encodability criteria

full rationale

The paper derives its separation theorems (no basic success-sensitive encoding of CCSK into CCS/π; no parallel-preserving strong bisimulation encoding into π) directly from the formal definitions of 'basic', 'success-sensitive', and 'parallel-preserving' encodings, which are imported from prior literature on process calculi rather than constructed or fitted within this work. No equations, self-citations, or ansatzes in the abstract or described content reduce any claim to an input by construction, and the results are explicitly conditional on these standard notions without internal redefinition or renaming of known results. The derivation is therefore self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The paper relies on standard mathematical definitions of process calculi, bisimulation, and encoding criteria from prior work; no free parameters, invented entities, or ad-hoc axioms are introduced in the abstract.

axioms (1)
  • standard math Standard definitions of strong and weak bisimilarity, success sensitivity, and basic encodings from process calculus literature.
    Invoked to state the separation and encoding theorems.

pith-pipeline@v0.9.1-grok · 5738 in / 1222 out tokens · 31610 ms · 2026-06-25T18:58:31.997023+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

31 extracted references · 27 canonical work pages

  1. [1]

    revtpl: The reversible temporal process language

    Laura Bocchi, Ivan Lanese, Claudio Antares Mezzina, and Shoji Yuen. revtpl: The reversible temporal process language. Log. Methods Comput. Sci. , 20(1), 2024. URL: https://doi.org/10.46298/lmcs-20(1:11)2024, https://doi.org/10.46298/LMCS-20(1:11)2024 doi:10.46298/LMCS-20(1:11)2024

    work page doi:10.46298/lmcs-20(1:11)2024 2024

  2. [2]

    On the expressiveness of internal mobility in name-passing calculi

    Michele Boreale. On the expressiveness of internal mobility in name-passing calculi. Theor. Comput. Sci. , 195(2):205--226, 1998. https://doi.org/10.1016/S0304-3975(97)00220-X doi:10.1016/S0304-3975(97)00220-X

    work page doi:10.1016/s0304-3975(97)00220-x 1998

  3. [3]

    A compositional semantics for the reversible -calculus

    Ioana Cristescu, Jean Krivine, and Daniele Varacca. A compositional semantics for the reversible -calculus. In Proceedings of LICS 2013 , pages 388--397. IEEE Computer Society, 2013. https://doi.org/10.1109/LICS.2013.45 doi:10.1109/LICS.2013.45

    work page doi:10.1109/lics.2013.45 2013

  4. [4]

    Reversible communicating systems

    Vincent Danos and Jean Krivine. Reversible communicating systems. In Philippa Gardner and Nobuko Yoshida, editors, Proceedings of CONCUR 2004 , volume 3170 of LNCS , pages 292--307. Springer, 2004. https://doi.org/10.1007/978-3-540-28644-8\_19 doi:10.1007/978-3-540-28644-8\_19

    work page doi:10.1007/978-3-540-28644-8 2004

  5. [5]

    Causal-consistent reversible debugging

    Elena Giachino, Ivan Lanese, and Claudio Antares Mezzina. Causal-consistent reversible debugging. In Stefania Gnesi and Arend Rensink, editors, Fundamental Approaches to Software Engineering - 17th International Conference, FASE 2014 , volume 8411 of Lecture Notes in Computer Science , pages 370--384. Springer, 2014. URL: https://doi.org/10.1007/978-3-642...

    work page doi:10.1007/978-3-642-54804-8 2014

  6. [6]

    Towards a unified approach to encodability and separation results for process calculi

    Daniele Gorla. Towards a unified approach to encodability and separation results for process calculi. Inf. Comput. , 208(9):1031--1053, 2010. https://doi.org/10.1016/J.IC.2010.05.002 doi:10.1016/J.IC.2010.05.002

    work page doi:10.1016/j.ic.2010.05.002 2010

  7. [7]

    Matching systems for concurrent calculi

    Bj rn Haagensen, Sergio Maffeis, and Iain Phillips. Matching systems for concurrent calculi. In Roberto M. Amadio and Thomas T. Hildebrandt, editors, Proceedings of the 14th International Workshop on Expressiveness in Concurrency, EXPRESS 2007, Lisbon, Portugal, September 3, 2007 , volume 194:2 of Electronic Notes in Theoretical Computer Science , pages 8...

    work page doi:10.1016/j.entcs.2007.11.004 2007

  8. [8]

    Modelling of DNA mismatch repair with a reversible process calculus

    Stefan Kuhn and Irek Ulidowski. Modelling of DNA mismatch repair with a reversible process calculus. Theor. Comput. Sci. , 925:68--86, 2022. URL: https://doi.org/10.1016/j.tcs.2022.06.009, https://doi.org/10.1016/J.TCS.2022.06.009 doi:10.1016/J.TCS.2022.06.009

    work page doi:10.1016/j.tcs.2022.06.009 2022

  9. [9]

    Static versus dynamic reversibility in CCS

    Ivan Lanese, Doriana Medic, and Claudio Antares Mezzina. Static versus dynamic reversibility in CCS . Acta Informatica , 58(1-2):1--34, 2021

    2021

  10. [10]

    Reversibility in the higher-order \( \) -calculus

    Ivan Lanese, Claudio Antares Mezzina, and Jean - Bernard Stefani. Reversibility in the higher-order \( \) -calculus. Theoretical Computer Science , 625:25--84, 2016. https://doi.org/10.1016/j.tcs.2016.02.019 doi:10.1016/j.tcs.2016.02.019

    work page doi:10.1016/j.tcs.2016.02.019 2016

  11. [11]

    Forward-reverse observational equivalences in CCSK

    Ivan Lanese and Iain Phillips. Forward-reverse observational equivalences in CCSK . In Shigeru Yamashita and Tetsuo Yokoyama, editors, Reversible Computation - 13th International Conference, RC 2021 , volume 12805 of Lecture Notes in Computer Science , pages 126--143. Springer, 2021. https://doi.org/10.1007/978-3-030-79837-6\_8 doi:10.1007/978-3-030-79837-6\_8

    work page doi:10.1007/978-3-030-79837-6 2021

  12. [12]

    Reversible computing in debugging of E rlang programs

    Ivan Lanese, Ulrik Pagh Schultz, and Irek Ulidowski. Reversible computing in debugging of E rlang programs. IT Prof. , 24(1):74--80, 2022. URL: https://doi.org/10.1109/MITP.2021.3117920

    work page doi:10.1109/mitp.2021.3117920 2022

  13. [13]

    Time travel debugging: root causing bugs in commercial scale software

    James McNellis, Jordi Mola, and Ken Sykes. Time travel debugging: root causing bugs in commercial scale software. CppCon talk, https://www.youtube.com/watch?v=l1YJTg_A914, 2017

    2017

  14. [14]

    Melgratti, Claudio Antares Mezzina, and G

    Hern \' a n C. Melgratti, Claudio Antares Mezzina, and G. Michele Pinna. A P etri net view of covalent bonds. Theor. Comput. Sci. , 908:89--119, 2022. URL: https://doi.org/10.1016/j.tcs.2022.01.013, https://doi.org/10.1016/J.TCS.2022.01.013 doi:10.1016/J.TCS.2022.01.013

    work page doi:10.1016/j.tcs.2022.01.013 2022

  15. [15]

    Melgratti, Claudio Antares Mezzina, and G

    Hern \' a n C. Melgratti, Claudio Antares Mezzina, and G. Michele Pinna. A truly concurrent semantics for reversible CCS . Log. Methods Comput. Sci. , 20(4), 2024. URL: https://doi.org/10.46298/lmcs-20(4:20)2024, https://doi.org/10.46298/LMCS-20(4:20)2024 doi:10.46298/LMCS-20(4:20)2024

    work page doi:10.46298/lmcs-20(4:20)2024 2024

  16. [17]

    Checkpoint-based rollback recovery in session programming

    Claudio Antares Mezzina, Francesco Tiezzi, and Nobuko Yoshida. Checkpoint-based rollback recovery in session programming. Log. Methods Comput. Sci. , 21(1):2, 2025. https://doi.org/10.46298/LMCS-21(1:2)2025 doi:10.46298/LMCS-21(1:2)2025

    work page doi:10.46298/lmcs-21(1:2)2025 2025

  17. [18]

    An algebraic definition of simulation between programs

    Robin Milner. An algebraic definition of simulation between programs. In D. C. Cooper, editor, Proceedings of the 2nd International Joint Conference on Artificial Intelligence. London, UK, September 1-3, 1971 , pages 481--489. William Kaufmann, 1971. URL: http://ijcai.org/Proceedings/71/Papers/044.pdf

    1971

  18. [19]

    Comparing the expressive power of the synchronous and asynchronous pi-calculi

    Catuscia Palamidessi. Comparing the expressive power of the synchronous and asynchronous pi-calculi. Math. Struct. Comput. Sci. , 13(5):685--719, 2003. https://doi.org/10.1017/S0960129503004043 doi:10.1017/S0960129503004043

    work page doi:10.1017/s0960129503004043 2003

  19. [20]

    Comparing process calculi using encodings

    Kirstin Peters. Comparing process calculi using encodings. In Jorge A. P \' e rez and Jurriaan Rot, editors, Proceedings Combined 26th International Workshop on Expressiveness in Concurrency and 16th Workshop on Structural Operational Semantics, EXPRESS/SOS 2019, Amsterdam, The Netherlands, 26th August 2019 , volume 300 of EPTCS , pages 19--38, 2019. http...

    work page doi:10.4204/eptcs.300.2 2019

  20. [21]

    Kirstin Peters and Uwe Nestmann. Is it a "good" encoding of mixed choice? In Lars Birkedal, editor, Foundations of Software Science and Computational Structures - 15th International Conference, FOSSACS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceeding...

    work page doi:10.1007/978-3-642-28729-9 2012

  21. [22]

    van Glabbeek

    Kirstin Peters and Rob J. van Glabbeek. Analysing and comparing encodability criteria. In Silvia Crafa and Daniel Gebler, editors, Proceedings of the Combined 22th International Workshop on Expressiveness in Concurrency and 12th Workshop on Structural Operational Semantics, EXPRESS/SOS 2015, Madrid, Spain, 31st August 2015 , volume 190 of EPTCS , pages 46...

    work page doi:10.4204/eptcs.190.4 2015

  22. [23]

    A completeness theorem for probabilistic regular expressions

    Kirstin Peters and Nobuko Yoshida. Separation and encodability in mixed choice multiparty sessions. In Pawel Sobocinski, Ugo Dal Lago, and Javier Esparza, editors, Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2024, Tallinn, Estonia, July 8-11, 2024 , pages 62:1--62:15. ACM , 2024. https://doi.org/10.1145/3661814.366...

    work page doi:10.1145/3661814.3662085 2024

  23. [24]

    CCS with priority guards

    Iain Phillips. CCS with priority guards. J. Log. Algebraic Methods Program. , 75(1):139--165, 2008. URL: https://doi.org/10.1016/j.jlap.2007.06.005, https://doi.org/10.1016/J.JLAP.2007.06.005 doi:10.1016/J.JLAP.2007.06.005

    work page doi:10.1016/j.jlap.2007.06.005 2008

  24. [25]

    Phillips and Irek Ulidowski

    Iain C.C. Phillips and Irek Ulidowski. Reversing algebraic process calculi. In Luca Aceto and Anna Ing \' o lfsd \' o ttir, editors, Proceedings of FoSSaCS 2006 , volume 3921 of LNCS , pages 246--260. Springer, 2006. https://doi.org/10.1007/11690634\_17 doi:10.1007/11690634\_17

    work page doi:10.1007/11690634 2006

  25. [26]

    Phillips and Irek Ulidowski

    Iain C.C. Phillips and Irek Ulidowski. Reversing algebraic process calculi. Journal of Logic and Algebraic Programming , 73(1-2):70--96, 2007. https://doi.org/10.1016/j.jlap.2006.11.002 doi:10.1016/j.jlap.2006.11.002

    work page doi:10.1016/j.jlap.2006.11.002 2007

  26. [27]

    Phillips, Irek Ulidowski, and Shoji Yuen

    Iain C.C. Phillips, Irek Ulidowski, and Shoji Yuen. A reversible process calculus and the modelling of the ERK signalling pathway. In Robert Gl \" u ck and Tetsuo Yokoyama, editors, Proceedings of RC 2012 , volume 7581 of LNCS , pages 218--232. Springer, 2012. https://doi.org/10.1007/978-3-642-36315-3\_18 doi:10.1007/978-3-642-36315-3\_18

    work page doi:10.1007/978-3-642-36315-3 2012

  27. [28]

    Replacement freeness: A criterion for separating process calculi

    Rosario Pugliese and Francesco Tiezzi. Replacement freeness: A criterion for separating process calculi. J. Log. Algebraic Methods Program. , 116:100579, 2020. https://doi.org/10.1016/J.JLAMP.2020.100579 doi:10.1016/J.JLAMP.2020.100579

    work page doi:10.1016/j.jlamp.2020.100579 2020

  28. [29]

    pi-calculus, internal mobility, and agent-passing calculi

    Davide Sangiorgi. pi-calculus, internal mobility, and agent-passing calculi. Theor. Comput. Sci. , 167(1 & 2):235--274, 1996. https://doi.org/10.1016/0304-3975(96)00075-8 doi:10.1016/0304-3975(96)00075-8

    work page doi:10.1016/0304-3975(96)00075-8 1996

  29. [30]

    The -Calculus - a theory of mobile processes

    Davide Sangiorgi and David Walker. The -Calculus - a theory of mobile processes . Cambridge University Press, 2001

    2001

  30. [31]

    Comparing the expressiveness of the \( \) -calculus and CCS

    Rob van Glabbeek. Comparing the expressiveness of the \( \) -calculus and CCS . ACM Trans. Comput. Log. , 25(1):1:1--1:58, 2024. https://doi.org/10.1145/3611013 doi:10.1145/3611013

    work page doi:10.1145/3611013 2024

  31. [32]

    Checkpoint/rollback vs causally-consistent reversibility

    Martin Vassor and Jean-Bernard Stefani. Checkpoint/rollback vs causally-consistent reversibility. In Jarkko Kari and Irek Ulidowski, editors, Reversible Computation - 10th International Conference, RC 2018 , volume 11106 of Lecture Notes in Computer Science , pages 286--303. Springer, 2018. https://doi.org/10.1007/978-3-319-99498-7\_20 doi:10.1007/978-3-3...

    work page doi:10.1007/978-3-319-99498-7 2018