Document Open Access Logo

On the Encodability of Reversible Process Calculi

Authors Ivan Lanese , Claudio Antares Mezzina , Iain Phillips , Irek Ulidowski , Shoji Yuen

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2026.41.pdf
  • Filesize: 0.8 MB
  • 20 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Concurrency
Keywords
  • Reversible computation
  • Process calculi
  • Encodings
  • Impossibility results

Metrics

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.

Cite As Get BibTex

Ivan Lanese, Claudio Antares Mezzina, Iain Phillips, Irek Ulidowski, and Shoji Yuen. On the Encodability of Reversible Process Calculi. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 41:1-41:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.CONCUR.2026.41

Author Details

Ivan Lanese
  • Olas Team, University of Bologna/INRIA, Italy
Claudio Antares Mezzina
  • University of Bari Aldo Moro, Italy
Iain Phillips
  • Imperial College London, UK
Irek Ulidowski
  • University of Leicester, UK
  • AGH University of Kraków, Poland
Shoji Yuen
  • Nagoya University, Japan

Funding

  • Lanese, Ivan: partial support of the French ANR project SmartCloud ANR-23-CE25-0012.
  • Mezzina, Claudio Antares: partial support of the MSCA SE project QCOMICAL (Grant Agreement ID: 101182520) and of the Japan Society for the Promotion of Science (JSPS) through the JSPS Invitation Fellowship for Research in Japan, grant no. S25016.
  • Ulidowski, Irek: partial support of the AY2024 International PI Invitation Program, IAR Nagoya University, and of the Japan Society for the Promotion of Science (JSPS) through the JSPS Invitation Fellowship for Research in Japan, grant no. S21050.

Acknowledgements

We thank the anonymous referees for their helpful comments and suggestions.

References

  1. 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.
  2. Michele Boreale. On the expressiveness of internal mobility in name-passing calculi. Theor. Comput. Sci., 195(2):205-226, 1998. URL: https://doi.org/10.1016/S0304-3975(97)00220-X.
  3. 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. URL: https://doi.org/10.1109/LICS.2013.45.
  4. 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. URL: https://doi.org/10.1007/978-3-540-28644-8_19.
  5. 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-54804-8_26.
  6. Daniele Gorla. Towards a unified approach to encodability and separation results for process calculi. Inf. Comput., 208(9):1031-1053, 2010. URL: https://doi.org/10.1016/J.IC.2010.05.002.
  7. 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 85-99. Elsevier, 2007. URL: https://doi.org/10.1016/J.ENTCS.2007.11.004.
  8. 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.
  9. Ivan Lanese, Doriana Medic, and Claudio Antares Mezzina. Static versus dynamic reversibility in CCS. Acta Informatica, 58(1-2):1-34, 2021. URL: https://doi.org/10.1007/S00236-019-00346-6.
  10. Ivan Lanese, Claudio Antares Mezzina, Iain Phillips, Irek Ulidowski, and Shoji Yuen. On the encodability of reversible process calculi. CoRR, 2606.25916, 2026. URL: https://doi.org/10.48550/arXiv.2606.25916.
  11. Ivan Lanese, Claudio Antares Mezzina, and Jean-Bernard Stefani. Reversibility in the higher-order π-calculus. Theoretical Computer Science, 625:25-84, 2016. URL: https://doi.org/10.1016/j.tcs.2016.02.019.
  12. 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. URL: https://doi.org/10.1007/978-3-030-79837-6_8.
  13. Ivan Lanese, Ulrik Pagh Schultz, and Irek Ulidowski. Reversible computing in debugging of Erlang programs. IT Prof., 24(1):74-80, 2022. URL: https://doi.org/10.1109/MITP.2021.3117920.
  14. 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.
  15. Hernán C. Melgratti, Claudio Antares Mezzina, and G. Michele Pinna. A Petri net view of covalent bonds. Theor. Comput. Sci., 908:89-119, 2022. URL: https://doi.org/10.1016/J.TCS.2022.01.013.
  16. Herná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.
  17. Claudio Antares Mezzina. On reversibility and broadcast. In Jarkko Kari and Irek Ulidowski, editors, Proceedings of RC 2018, volume 11106 of LNCS, pages 67-83. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-99498-7_5.
  18. Claudio Antares Mezzina, Francesco Tiezzi, and Nobuko Yoshida. Checkpoint-based rollback recovery in session programming. Log. Methods Comput. Sci., 21(1):2, 2025. URL: https://doi.org/10.46298/LMCS-21(1:2)2025.
  19. 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.
  20. Catuscia Palamidessi. Comparing the expressive power of the synchronous and asynchronous pi-calculi. Math. Struct. Comput. Sci., 13(5):685-719, 2003. URL: https://doi.org/10.1017/S0960129503004043.
  21. Kirstin Peters. Comparing process calculi using encodings. In Jorge A. Pé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. URL: https://doi.org/10.4204/EPTCS.300.2.
  22. 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. Proceedings, volume 7213 of Lecture Notes in Computer Science, pages 210-224. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-28729-9_14.
  23. 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-60, 2015. URL: https://doi.org/10.4204/EPTCS.190.4.
  24. 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. URL: https://doi.org/10.1145/3661814.3662085.
  25. 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.
  26. Iain C.C. Phillips and Irek Ulidowski. Reversing algebraic process calculi. In Luca Aceto and Anna Ingólfsdóttir, editors, Proceedings of FoSSaCS 2006, volume 3921 of LNCS, pages 246-260. Springer, 2006. URL: https://doi.org/10.1007/11690634_17.
  27. Iain C.C. Phillips and Irek Ulidowski. Reversing algebraic process calculi. Journal of Logic and Algebraic Programming, 73(1-2):70-96, 2007. URL: https://doi.org/10.1016/j.jlap.2006.11.002.
  28. Iain C.C. Phillips, Irek Ulidowski, and Shoji Yuen. A reversible process calculus and the modelling of the ERK signalling pathway. In Robert Glück and Tetsuo Yokoyama, editors, Proceedings of RC 2012, volume 7581 of LNCS, pages 218-232. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-36315-3_18.
  29. Rosario Pugliese and Francesco Tiezzi. Replacement freeness: A criterion for separating process calculi. J. Log. Algebraic Methods Program., 116:100579, 2020. URL: https://doi.org/10.1016/J.JLAMP.2020.100579.
  30. Davide Sangiorgi. pi-calculus, internal mobility, and agent-passing calculi. Theor. Comput. Sci., 167(1&2):235-274, 1996. URL: https://doi.org/10.1016/0304-3975(96)00075-8.
  31. Davide Sangiorgi and David Walker. The π-Calculus - a theory of mobile processes. Cambridge University Press, 2001. Google Scholar
  32. Rob van Glabbeek. Comparing the expressiveness of the π-calculus and CCS. ACM Trans. Comput. Log., 25(1):1:1-1:58, 2024. URL: https://doi.org/10.1145/3611013.
  33. 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. URL: https://doi.org/10.1007/978-3-319-99498-7_20.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact