Pith. sign in

REVIEW 2 minor 31 references

On the Encodability of Reversible Process Calculi

T0 review · 0 major / 2 minor · reviewed 2026-07-01 · grok-4.3

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read Reversible calculi such as CCSK cannot be encoded into forward-only calculi like CCS or the pi-calculus under basic success-sensitive conditions.

desk verdict The paper establishes that CCSK cannot be encoded basically and success-sensitively into CCS or the pi-calculus under strong bisimilarity, but supplies positive encodings once parallelism is restricted or the equivalence is weakened. read the letter →

arxiv 2606.25916 v2 pith:YJDLJKUN submitted 2026-06-24 cs.LO

Ivan Lanese , Claudio Antares Mezzina , Iain Phillips , Irek Ulidowski , Shoji Yuen This is my paper · ORCID
classification cs.LO
keywords reversibleprocesscalculiencodabilityCCSKseparationtheorempi-calculusCCSstrongbisimilarityweakmutualsimulation
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

The paper tries to establish that reversibility fundamentally increases the expressive power of process calculi, preventing any basic success-sensitive encoding of CCSK into CCS or the pi-calculus. A sympathetic reader would care because this separation clarifies limits on simulating reversible behavior in standard models used for concurrent systems. The authors prove the negative result and then give positive encodings for restricted cases with top-level parallel composition into the internal pi-calculus, along with a limitation for arbitrary parallel composition under strong bisimilarity but a positive result under weak mutual simulation.

What carries the argument

The separation theorem for basic, success-sensitive encodings using strong bisimilarity as the behavioral equivalence.

What would settle it

The discovery of a basic success-sensitive encoding from CCSK to the pi-calculus that preserves the required behavioral equivalence would falsify the separation theorem.

Watch

Extended reading notes

Core claim

We establish a separation theorem showing that there is no basic, success-sensitive encoding of CCSK into CCS or the pi-calculus. We present an encoding of CCSK processes with only top-level parallel composition into the internal pi-calculus, correct up to strong bisimilarity. No parallel-preserving encoding of CCSK with arbitrary parallel composition into the pi-calculus can be correct up to strong bisimilarity, but one exists that is correct under weak mutual simulation.

Load-bearing premise

The notions of basic encoding and success-sensitive encoding, together with the choice of strong bisimilarity, must accurately capture the intended requirements for the separation to hold.

Editorial extensions

If this is right

  • Reversibility has a strong impact on the expressive power of concurrent models.
  • Encodings exist only when parallel composition is restricted to top level.
  • Parallel-preserving encodings require weaker behavioral correspondences like weak mutual simulation.
  • Reversible extensions cannot be directly simulated in classical forward-only calculi without loss of properties.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • Reversible features may require dedicated language support rather than translations to existing calculi.
  • Models for debugging or biological systems with reversibility might need to incorporate reversible primitives directly.
  • Similar separation results could apply to other reversible extensions of process calculi.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Request a human review

A listed scientist reviews the paper for a fee and the review publishes here regardless of verdict. See the reviewers or get listed.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

0 major / 2 minor

Summary. The paper claims to establish a separation theorem showing that there is no basic, success-sensitive encoding of CCSK into CCS or the π-calculus (correct w.r.t. strong bisimilarity), while also presenting a positive encoding of CCSK processes with only top-level parallel composition into the internal π-calculus (correct up to strong bisimilarity), identifying that no parallel-preserving encoding of full CCSK into the π-calculus works under strong bisimilarity, and providing a parallel-preserving encoding correct under weak mutual simulation.

Significance. If the separation and positive results hold under the stated criteria, the work meaningfully extends the encodability literature to reversible process calculi by demonstrating that reversibility imposes strict limitations on expressiveness that cannot be bridged by standard encodings into forward-only models. The explicit scoping via both negative and positive results (including the relaxation cases) provides a balanced assessment of the boundaries.

minor comments (2)
  1. [Abstract] Abstract: the phrase 'basic, success-sensitive encoding' is used without a parenthetical gloss or forward reference to the precise definition (drawn from the literature); adding one sentence would improve immediate readability for readers outside the subfield.
  2. The manuscript should ensure that all behavioral equivalences (strong bisimilarity, weak mutual simulation) and the internal π-calculus variant are uniformly notated and cross-referenced when first introduced.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the careful reading and positive assessment of our manuscript. The summary accurately reflects the separation result for basic success-sensitive encodings, the positive result for top-level parallelism, the impossibility result for parallel-preserving encodings under strong bisimilarity, and the positive result under weak mutual simulation. We are pleased that the work is viewed as a meaningful extension of the encodability literature.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: separation theorems rest on explicit external definitions

full rationale

The paper states separation results for basic success-sensitive encodings w.r.t. strong bisimilarity, but these notions are introduced via explicit definitions drawn from the established encodability literature (not invented or fitted inside the paper). Positive results for relaxed criteria are presented separately, confirming the negative claim is not forced by construction. No self-citation chain, ansatz smuggling, or renaming of known results is used to justify the core theorems. The derivation chain is therefore self-contained against external benchmarks.

Assumptions & free parameters 0 free parameters · 2 assumptions · 0 invented entities

The central claims rest on standard mathematical definitions of process calculi, bisimilarity, and encoding criteria from the concurrency-theory literature, with no free parameters, no invented entities, and no ad-hoc axioms introduced by the paper itself.

assumptions (2)
  • standard math Standard definitions of CCS, pi-calculus, and behavioral equivalences such as strong bisimilarity and weak mutual simulation
    Invoked throughout the statements of encodability and separation results.
  • domain assumption Definitions of basic encoding and success-sensitivity
    These domain-specific notions of encoding are required for the separation theorem to hold.

how reviews work

0 comments
Cite this review

Pith. "Pith review of On the Encodability of Reversible Process Calculi." pith.science (2026). https://pith.science/paper/YJDLJKUN

@misc{pith2026260625916,
  author       = {Pith},
  title        = {Pith review of: On the Encodability of Reversible Process Calculi},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/YJDLJKUN}},
  note         = {Machine review of arXiv:2606.25916}
}
read the original 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 {\pi}-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 {\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.

Figures

Figures reproduced from arXiv: 2606.25916 by the authors.

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 ↗
Figure 6
Figure 6. ▶ Remark 6.3. The encoding above allows for rollback messages xi to be received in any order. Picking a specific order would not change the correctness result, but will make the encoding of structural congruent processes different, making the proof more complex. This would be however better in a practical setting, since it reduces the size of the resulting process (from a factorial of the number of parallel componen… view at source ↗

Review history (2 revisions) →

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

31 extracted references · 31 canonical work pages

  1. [1]

    Bocchi, I

    Laura Bocchi, Ivan Lanese, Claudio Antares Mezzina, and Shoji Yuen. revTPL : The reversible temporal process language. Log. Methods Comput. Sci. , 20(1), 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]

    Cristescu, J

    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]

    In: Proceedings of the 15th International Conference on Con currency The- ory (CONCUR 2004)

    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]

    Giachino, I

    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. https://doi.org/10.1007/978-3-642-5480...

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

  6. [6]

    Information and Computation 208(9), pp

    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. 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

Show all 31 references
  1. [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. https://doi.org/10.1007/S00236-019-00346-6 doi:10.1007/S00236-019-00346-6

    2021 doi

  2. [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

    2016 doi

  3. [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 doi

  4. [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. https://doi.org/10.1109/MITP.2021.3117920 doi:10.1109/MITP.2021.3117920

    2022 doi

  5. [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

  6. [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. https://doi.org/10.1016/J.TCS.2022.01.013 doi:10.1016/J.TCS.2022.01.013

    2022 doi

  7. [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. https://doi.org/10.46298/LMCS-20(4:20)2024 doi:10.46298/LMCS-20(4:20)2024

    2024 doi

  8. [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

    2025 doi

  9. [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/Proc...

    1971

  10. [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

    2003 doi

  11. [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, Th...

    2019 doi

  12. [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...

    2012 doi

  13. [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, EX...

    2015 doi

  14. [23]

    Separation and encodability in mixed choice multiparty sessions

    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...

    2024 doi

  15. [24]

    CCS with priority guards

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

    2008 doi

  16. [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

    2006 doi

  17. [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

    2007 doi

  18. [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/...

    2012 doi

  19. [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

    2020 doi

  20. [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

    1996 doi

  21. [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

  22. [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

    2024 doi

  23. [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. S...

    2018 doi

Pith tools

Reviewed July 1, 2026 · model on record in the stance chip above.