{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,30]],"date-time":"2026-09-30T23:35:37Z","timestamp":1790811337475,"version":"4.1.0"},"reference-count":50,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2024,4,16]],"date-time":"2024-04-16T00:00:00Z","timestamp":1713225600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"COST Action IC1405"},{"name":"French ANR","award":["ANR-18-CE25-0007"],"award-info":[{"award-number":["ANR-18-CE25-0007"]}]},{"name":"INdAM-GNCS","award":["CUP_E55F22000270001"],"award-info":[{"award-number":["CUP_E55F22000270001"]}]},{"name":"JSPS Invitation Fellowship","award":["S21050"],"award-info":[{"award-number":["S21050"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2024,4,30]]},"abstract":"<jats:p>Undoing computations of a concurrent system is beneficial in many situations, such as in reversible debugging of multi-threaded programs and in recovery from errors due to optimistic execution in parallel discrete event simulation. A number of approaches have been proposed for how to reverse formal models of concurrent computation, including process calculi such as CCS, languages like Erlang, and abstract models such as prime event structures and occurrence nets. However, it has not been settled as to what properties a reversible system should enjoy, nor how the various properties that have been suggested, such as the parabolic lemma and the causal-consistency property, are related. We contribute to a solution to these issues by using a generic labelled transition system equipped with a relation capturing whether transitions are independent to explore the implications between various reversibility properties. In particular, we show how all properties we consider are derivable from a set of axioms. Our intention is that when establishing properties of some formalism, it will be easier to verify the axioms rather than proving properties such as the parabolic lemma directly. We also introduce two new properties related to causal-consistent reversibility, namely causal liveness and causal safety, stating, respectively, that an action can be undone if (causal liveness) and only if (causal safety) it is independent from all of the following actions. These properties come in three flavours: defined in terms of independent transitions, independent events, or via an ordering on events. Both causal liveness and causal safety are derivable from our axioms.<\/jats:p>","DOI":"10.1145\/3648474","type":"journal-article","created":{"date-parts":[[2024,2,19]],"date-time":"2024-02-19T12:22:57Z","timestamp":1708345377000},"page":"1-40","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":12,"title":["An Axiomatic Theory for Reversible Computation"],"prefix":"10.1145","volume":"25","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2527-9995","authenticated-orcid":false,"given":"Ivan","family":"Lanese","sequence":"first","affiliation":[{"name":"Olas Team, University of Bologna\/INRIA, Bologna, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5013-5876","authenticated-orcid":false,"given":"Iain","family":"Phillips","sequence":"additional","affiliation":[{"name":"Imperial College London, London, England"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3834-2036","authenticated-orcid":false,"given":"Irek","family":"Ulidowski","sequence":"additional","affiliation":[{"name":"University of Leicester, Leicester, England and AGH University of Science and Technology, Krak\u00f3w, Poland"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,4,16]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","unstructured":"Cl\u00e9ment Aubert. 2022. Concurrencies in reversible concurrent calculi. In Reversible Computation Claudio Antares Mezzina and Krzysztof Podlaski (Eds.). Lecture Notes in Computer Science Vol. 13354. Springer 146\u2013163. 10.1007\/978-3-031-09005-9_10","DOI":"10.1007\/978-3-031-09005-9_10"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","unstructured":"Cl\u00e9ment Aubert and Doriana Medic. 2021. Explicit identifiers and contexts in reversible concurrent calculus. In Reversible Computation Shigeru Yamashita and Tetsuo Yokoyama (Eds.). Lecture Notes in Computer Science Vol. 12805. Springer 144\u2013162. 10.1007\/978-3-030-79837-6_9","DOI":"10.1007\/978-3-030-79837-6_9"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2022.05.030"},{"key":"e_1_3_2_5_2","volume-title":"Hereditary History Preserving Bisimulations or What Is the Power of the Future Perfect in Program Logics","author":"Bednarczyk Marek A.","year":"1991","unstructured":"Marek A. Bednarczyk. 1991. Hereditary History Preserving Bisimulations or What Is the Power of the Future Perfect in Program Logics. Technical Report ICS PAS. Polish Academy of Sciences."},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","unstructured":"Alexis Bernadet and Ivan Lanese. 2016. A modular formalization of reversibility for concurrent models and languages. Electronic Proceedings in Theoretical Computer Science 223 (2016) 98\u2013112. 10.4204\/EPTCS.223.7","DOI":"10.4204\/EPTCS.223.7"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.46298\/LMCS-19(2:6)2023"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","unstructured":"Marco Bernardo and Sabina Rossi. 2023. Reverse bisimilarity vs. forward bisimilarity. In Foundations of Software Science and Computation Structures Orna Kupferman and Pawel Sobocinski (Eds.). Lecture Notes in Computer Science Vol. 13992. Springer 265\u2013284. 10.1007\/978-3-031-30829-1_13","DOI":"10.1007\/978-3-031-30829-1_13"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","unstructured":"Laura Bocchi Ivan Lanese Claudio Antares Mezzina and Shoji Yuen. 2022. The reversible temporal process language. In Formal Techniques for Distributed Objects Components and Systems Mohammad Reza Mousavi and Anna Philippou (Eds.). Lecture Notes in Computer Science Vol. 13273. Springer 31\u201349. 10.1007\/978-3-031-08679-3_3","DOI":"10.1007\/978-3-031-08679-3_3"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/2037509.2037529"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/347823.347828"},{"key":"e_1_3_2_12_2","volume-title":"Operational and Denotational Semantics for the Reversible  \\(\\pi\\) -Calculus","author":"Cristescu Ioana","year":"2015","unstructured":"Ioana Cristescu. 2015. Operational and Denotational Semantics for the Reversible \\(\\pi\\) -Calculus. Ph. D. Dissertation. Paris Centre Mathematical sciences Doctoral School. https:\/\/scholar.harvard.edu\/files\/cristescu\/files\/these.pdf"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2013.45"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","unstructured":"Vincent Danos and Jean Krivine. 2004. Reversible communicating systems. In CONCUR 2004\u2014Concurrency Theory Philippa Gardner and Nobuko Yoshida (Eds.). Lecture Notes in Computer Science Vol. 3170. Springer 292\u2013307. 10.1007\/978-3-540-28644-8_19","DOI":"10.1007\/978-3-540-28644-8_19"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","unstructured":"Vincent Danos and Jean Krivine. 2005. Transactions in RCCS. In CONCUR 2005\u2014Concurrency Theory Mart\u00edn Abadi and Luca de Alfaro (Eds.). Lecture Notes in Computer Science Vol. 3653. Springer 398\u2013412. 10.1007\/11539452_31","DOI":"10.1007\/11539452_31"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","unstructured":"Vincent Danos Jean Krivine and Pawe\u0142 Soboci\u0144ski. 2007. General reversibility. Electronic Notes in Theoretical Computer Science 175 3 (2007) 75\u201386. 10.1016\/j.entcs.2006.07.036","DOI":"10.1016\/j.entcs.2006.07.036"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","unstructured":"David de Frutos Escrig Maciej Koutny and \u0141ukasz Mikulski. 2019. Reversing steps in Petri nets. In Application and Theory of Petri Nets and Concurrency Susanna Donelli and Stefan Haar (Eds.). Lecture Notes in Computer Science Vol. 11522. Springer 171\u2013191. 10.1007\/978-3-030-21571-2_11","DOI":"10.1007\/978-3-030-21571-2_11"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","unstructured":"Elena Giachino Ivan Lanese and Claudio Antares Mezzina. 2014. Causal-consistent reversible debugging. In Fundamental Approaches to Software Engineering Stefania Gnesi and Arend Rensink (Eds.). Lecture Notes in Computer Science Vol. 8411. Springer 370\u2013384. 10.1007\/978-3-642-54804-8_26","DOI":"10.1007\/978-3-642-54804-8_26"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2016.09.003"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2021.100720"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2019.02.006"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2017.09.008"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","unstructured":"Pietro Lami Ivan Lanese Jean-Bernard Stefani Claudio Sacerdoti Coen and Giovanni Fabbretti. 2022. Reversibility in Erlang: Imperative constructs. In Reversible Computation Claudio Antares Mezzina and Krzysztof Podlaski (Eds.). Lecture Notes in Computer Science Vol. 13354.Springer 187\u2013203. 10.1007\/978-3-031-09005-9_13","DOI":"10.1007\/978-3-031-09005-9_13"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1147\/rd.53.0183"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","unstructured":"Ivan Lanese and Doriana Medic. 2020. A general approach to derive uncontrolled reversible semantics. In Proceedings of CONCUR 2020 Igor Konnov and Laura Kov\u00e1cs (Eds.). Liebniz International Proceedings in Informatics Vol. 171. Schloss Dagstuhl\u2013Leibniz-Zentrum f\u00fcr Informatik Article 33 24 pages. 10.4230\/LIPIcs.CONCUR.2020.33","DOI":"10.4230\/LIPIcs.CONCUR.2020.33"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","unstructured":"Ivan Lanese Claudio Antares Mezzina Alan Schmitt and Jean-Bernard Stefani. 2011. Controlling reversibility in higher-order pi. In CONCUR 2011\u2014Concurrency Theory Joost-Pieter Katoen and Barbara K\u00f6nig (Eds.). Lecture Notes in Computer Science Vol. 6901. Springer 297\u2013311. 10.1007\/978-3-642-23217-6_20","DOI":"10.1007\/978-3-642-23217-6_20"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","unstructured":"Ivan Lanese Claudio Antares Mezzina and Jean-Bernard Stefani. 2012. Controlled reversibility and compensations. In Reversible Computation Robert Gl\u00fcck and Tetsuo Yokoyama (Eds.). Lecture Notes in Computer Science Vol. 7581. Springer 233\u2013240. 10.1007\/978-3-642-36315-3_19","DOI":"10.1007\/978-3-642-36315-3_19"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2016.02.019"},{"key":"e_1_3_2_29_2","article-title":"Causal-consistent reversibility","volume":"114","author":"Lanese Ivan","year":"2014","unstructured":"Ivan Lanese, Claudio Antares Mezzina, and Francesco Tiezzi. 2014. Causal-consistent reversibility. Bulletin of the EATCS 114 (2014), 1\u201319.","journal-title":"Bulletin of the EATCS"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","unstructured":"Ivan Lanese Naoki Nishida Adri\u00e1n Palacios and Germ\u00e1n Vidal. 2018. CauDEr: A causal-consistent reversible debugger for Erlang. In Functional and Logic Programming John P. Gallagher and Martin Sulzmann (Eds.). Lecture Notes in Computer Science Vol. 10818. Springer 247\u2013263. 10.1007\/978-3-319-90686-7_16","DOI":"10.1007\/978-3-319-90686-7_16"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2018.06.004"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","unstructured":"Ivan Lanese Iain Phillips and Irek Ulidowski. 2020. An axiomatic approach to reversible computation. In Foundations of Software Science and Computation Structures Jean Goubault-Larrecq and Barbara K\u00f6nig (Eds.). Lecture Notes in Computer Science Vol. 12077. Springer 442\u2013461. 10.1007\/978-3-030-45231-5_23","DOI":"10.1007\/978-3-030-45231-5_23"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1109\/IROS.2015.7353609"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","unstructured":"Michael Lienhardt Ivan Lanese Claudio Antares Mezzina and Jean-Bernard Stefani. 2012. A reversible abstract machine and its space overhead. In Formal Techniques for Distributed Systems Holger Giese and Grigore Rosu (Eds.). Lecture Notes in Computer Science Vol. 7273. Springer 1\u201317. 10.1007\/978-3-642-30793-5_1","DOI":"10.1007\/978-3-642-30793-5_1"},{"key":"e_1_3_2_35_2","article-title":"Time Travel Debugging: Root Causing Bugs in Commercial Scale Software","author":"McNellis James","year":"2017","unstructured":"James McNellis, Jordi Mola, and Ken Sykes. 2017. Time Travel Debugging: Root Causing Bugs in Commercial Scale Software. CppCon Talk. Retrieved February 28, 2024 from https:\/\/www.youtube.com\/watch?v=l1YJTg_A914","journal-title":"CppCon Talk"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","unstructured":"Hern\u00e1n C. Melgratti Claudio Antares Mezzina Iain Phillips G. Michele Pinna and Irek Ulidowski. 2020. Reversible occurrence nets and causal reversible prime event structures. In Reversible Computation Ivan Lanese and Mariusz Rawski (Eds.). Lecture Notes in Computer Science Vol. 12227. Springer 35\u201353. 10.1007\/978-3-030-52482-1_2","DOI":"10.1007\/978-3-030-52482-1_2"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","unstructured":"Hern\u00e1n C. Melgratti Claudio Antares Mezzina and Irek Ulidowski. 2019. Reversing P\/T nets. In Coordination Models and Languages Hanne Riis Nielson and Emilio Tuosto (Eds.). Lecture Notes in Computer Science Vol. 11533. Springer 19\u201336. 10.1007\/978-3-030-22397-7_2","DOI":"10.1007\/978-3-030-22397-7_2"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-16(4:5)2020"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","unstructured":"Claudio Antares Mezzina. 2018. On reversibility and broadcast. In Reversible Computation Jarkko Kari and Irek Ulidowski (Eds.). Lecture Notes in Computer Science Vol. 11106. Springer 67\u201383. 10.1007\/978-3-319-99498-7_5","DOI":"10.1007\/978-3-319-99498-7_5"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.5555\/218623.218630"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","unstructured":"Iain Phillips and Irek Ulidowski. 2006. Reversing algebraic process calculi. In Foundations of Software Science and Computation Structures Luca Aceto and Anna Ing\u00f3lfsd\u00f3ttir (Eds.). Lecture Notes in Computer Science Vol. 3921. Springer 246\u2013260. 10.1007\/11690634_17","DOI":"10.1007\/11690634_17"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","unstructured":"Iain Phillips and Irek Ulidowski. 2007. Reversibility and models for concurrency. Electronic Notes in Theoretical Computer Science 192 (2007) 93\u2013108. 10.1016\/j.entcs.2007.08.018","DOI":"10.1016\/j.entcs.2007.08.018"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2006.11.002"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","unstructured":"Iain Phillips and Irek Ulidowski. 2013. Reversibility and asymmetric conflict in event structures. In CONCUR 2013\u2014Concurrency Theory Pedro R. D\u2019Argenio and Hern\u00e1n C. Melgratti (Eds.). Lecture Notes in Computer Science Vol. 8052. Springer 303\u2013318. 10.1007\/978-3-642-40184-8_22","DOI":"10.1007\/978-3-642-40184-8_22"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2015.07.004"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","unstructured":"Iain Phillips Irek Ulidowski and Shoji Yuen. 2012. A reversible process calculus and the modelling of the ERK signalling pathway. In Reversible Computation Robert Gl\u00fcck and Tetsuo Yokoyama (Eds.). Lecture Notes in Computer Science Vol. 7581. Springer 218\u2013232. 10.1007\/978-3-642-36315-3_18","DOI":"10.1007\/978-3-642-36315-3_18"},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","unstructured":"Jean-Eric Pin. 1987. On the language accepted by finite reversible automata. In Automata Languages and Programming Thomas Ottmann (Ed.). Lecture Notes in Computer Science Vol. 267. Springer 237\u2013249. 10.1007\/3-540-18088-5_19","DOI":"10.1007\/3-540-18088-5_19"},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(96)80710-9"},{"key":"e_1_3_2_49_2","unstructured":"Rob J. van Glabbeek. 1996. History preserving process graphs. Draft June 20 1996. Stanford University. http:\/\/boole.stanford.edu\/rvg\/pub\/history.draft.dvi"},{"key":"e_1_3_2_50_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1997.2634"},{"key":"e_1_3_2_51_2","doi-asserted-by":"publisher","DOI":"10.1145\/1244381.1244404"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3648474","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3648474","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T22:50:19Z","timestamp":1750287019000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3648474"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,4,16]]},"references-count":50,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2024,4,30]]}},"alternative-id":["10.1145\/3648474"],"URL":"https:\/\/doi.org\/10.1145\/3648474","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,4,16]]},"assertion":[{"value":"2023-07-13","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-01-22","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-04-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}