{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,30]],"date-time":"2026-09-30T11:12:43Z","timestamp":1790766763647,"version":"4.1.0"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030452308","type":"print"},{"value":"9783030452315","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Undoing computations of a concurrent system is beneficial in many situations, e.g., 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, prime event structures and occurrence nets. However it has not been settled 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 these properties. In particular, we show how they 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 notions related to causal consistent reversibility, namely causal safety and causal liveness, and show that they are derivable from our axioms.<\/jats:p>","DOI":"10.1007\/978-3-030-45231-5_23","type":"book-chapter","created":{"date-parts":[[2020,4,17]],"date-time":"2020-04-17T10:02:53Z","timestamp":1587117773000},"page":"442-461","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":19,"title":["An Axiomatic Approach to Reversible Computation"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2527-9995","authenticated-orcid":false,"given":"Ivan","family":"Lanese","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5013-5876","authenticated-orcid":false,"given":"Iain","family":"Phillips","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3834-2036","authenticated-orcid":false,"given":"Irek","family":"Ulidowski","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2020,4,17]]},"reference":[{"key":"23_CR1","doi-asserted-by":"crossref","unstructured":"Barylska, K., Koutny, M., Mikulski, \u0141., Pia\u0327tkowski, M.: Reversible computation vs. reversibility in Petri nets. Science of Computer Programming 151, 48\u201360 (2018)","DOI":"10.1016\/j.scico.2017.10.008"},{"key":"23_CR2","doi-asserted-by":"crossref","unstructured":"Bennett, C.H.: Logical reversibility of computation. IBM Journal of Research and Development 17(6), 525\u2013532 (1973)","DOI":"10.1147\/rd.176.0525"},{"key":"23_CR3","doi-asserted-by":"crossref","unstructured":"Bernadet, A., Lanese, I.: A modular formalization of reversibility for concurrent models and languages. In: Bartoletti, M., Henrio, L., Knight, S., Vieira, H.T. (eds.) ICE. EPTCS, vol. 223, pp. 98\u2013112 (2016)","DOI":"10.4204\/EPTCS.223.7"},{"key":"23_CR4","doi-asserted-by":"crossref","unstructured":"Carothers, C.D., Perumalla, K.S., Fujimoto, R.: Efficient optimistic parallel simulations using reverse computation. ACM Transactions on Modeling and Computer Simulation 9(3), 224\u2013253 (1999)","DOI":"10.1145\/347823.347828"},{"key":"23_CR5","doi-asserted-by":"crossref","unstructured":"Cristescu, I., Krivine, J., Varacca, D.: A compositional semantics for the reversible pi-calculus. In: LICS. pp. 388\u2013397. IEEE Computer Society (2013)","DOI":"10.1109\/LICS.2013.45"},{"key":"23_CR6","doi-asserted-by":"crossref","unstructured":"Danos, V., Krivine, J.: Reversible communicating systems. In: Gardner, P., Yoshida, N. (eds.) CONCUR. LNCS, vol. 3170, pp. 292\u2013307. Springer (2004)","DOI":"10.1007\/978-3-540-28644-8_19"},{"key":"23_CR7","doi-asserted-by":"crossref","unstructured":"Danos, V., Krivine, J.: Transactions in RCCS. In: Abadi, M., de Alfaro, L. (eds.) CONCUR. LNCS, vol. 3653, pp. 398\u2013412. Springer (2005)","DOI":"10.1007\/11539452_31"},{"key":"23_CR8","doi-asserted-by":"crossref","unstructured":"Danos, V., Krivine, J., Soboci\u0144ski, P.: General reversibility. In: Amadio, R.M., Phillips, I. (eds.) EXPRESS. ENTCS, vol. 175(3), pp. 75\u201386. Elsevier (2006)","DOI":"10.1016\/j.entcs.2006.07.036"},{"key":"23_CR9","doi-asserted-by":"crossref","unstructured":"de Frutos Escrig, D., Koutny, M., Mikulski, \u0141.: Reversing steps in Petri nets. In: Donelli, S., Haar, S. (eds.) Petri Nets. LNCS, vol. 11522. Springer (2019)","DOI":"10.1007\/978-3-030-21571-2_11"},{"key":"23_CR10","doi-asserted-by":"crossref","unstructured":"Giachino, E., Lanese, I., Mezzina, C.A.: Causal-consistent reversible debugging. In: Gnesi, S., Rensink, A. (eds.) FASE. LNCS, vol. 8411, pp. 370\u2013384. Springer (2014)","DOI":"10.1007\/978-3-642-54804-8_26"},{"key":"23_CR11","doi-asserted-by":"crossref","unstructured":"Giachino, E., Lanese, I., Mezzina, C.A., Tiezzi, F.: Causal-consistent rollback in a tuple-based language. Journal of Logical and Algebraic Methods in Programming 88, 99\u2013120 (2017)","DOI":"10.1016\/j.jlamp.2016.09.003"},{"key":"23_CR12","doi-asserted-by":"crossref","unstructured":"van Glabbeek, R., Vaandrager, F.: The difference between splitting in $$n$$ and $$n+1$$. Information and Computation 136(2), 109\u2013142 (1997)","DOI":"10.1006\/inco.1997.2634"},{"key":"23_CR13","doi-asserted-by":"crossref","unstructured":"Kari, J.: Reversible cellular automata: From fundamental classical results to recent developments. New Generation Computing 36(3), 145\u2013172 (2018)","DOI":"10.1007\/s00354-018-0034-6"},{"key":"23_CR14","doi-asserted-by":"crossref","unstructured":"Kuhn, S., Ulidowski, I.: Local reversibility in a Calculus of Covalent Bonding. Science of Computer Programming 151, 18\u201347 (2018)","DOI":"10.1016\/j.scico.2017.09.008"},{"key":"23_CR15","doi-asserted-by":"crossref","unstructured":"Landauer, R.: Irreversibility and heat generated in the computing process. IBM Journal of Research and Development 5, 183\u2013191 (1961)","DOI":"10.1147\/rd.53.0183"},{"key":"23_CR16","doi-asserted-by":"crossref","unstructured":"Lanese, I., Phillips, I., Ulidowski, I.: An axiomatic approach to reversible computation (TR) (2020), http:\/\/www.cs.unibo.it\/~lanese\/work\/axrev-TR.pdf","DOI":"10.1007\/978-3-030-45231-5_23"},{"key":"23_CR17","doi-asserted-by":"crossref","unstructured":"Lanese, I., Mezzina, C.A., Schmitt, A., Stefani, J.: Controlling reversibility in higher-order pi. In: Katoen, J., K\u00f6nig, B. (eds.) CONCUR. LNCS, vol. 6901, pp. 297\u2013311. Springer (2011)","DOI":"10.1007\/978-3-642-23217-6_20"},{"key":"23_CR18","doi-asserted-by":"crossref","unstructured":"Lanese, I., Mezzina, C.A., Stefani, J.: Reversibility in the higher-order $$\\pi $$-calculus. Theoretical Computer Science 625, 25\u201384 (2016)","DOI":"10.1016\/j.tcs.2016.02.019"},{"key":"23_CR19","unstructured":"Lanese, I., Mezzina, C.A., Tiezzi, F.: Causal-consistent reversibility. Bulletin of the EATCS 114 (2014)"},{"key":"23_CR20","doi-asserted-by":"crossref","unstructured":"Lanese, I., Nishida, N., Palacios, A., Vidal, G.: A theory of reversibility for Erlang. Journal of Logical and Algebraic Methods in Programming 100, 71\u201397 (2018)","DOI":"10.1016\/j.jlamp.2018.06.004"},{"key":"23_CR21","doi-asserted-by":"crossref","unstructured":"Laursen, J.S., Schultz, U.P., Ellekilde, L.: Automatic error recovery in robot assembly operations using reverse execution. In: IROS. pp. 1785\u20131792. IEEE (2015)","DOI":"10.1109\/IROS.2015.7353609"},{"key":"23_CR22","doi-asserted-by":"crossref","unstructured":"Lienhardt, M., Lanese, I., Mezzina, C.A., Stefani, J.: A reversible abstract machine and its space overhead. In: Giese, H., Rosu, G. (eds.) FMOODS\/FORTE. LNCS, vol. 7273, pp. 1\u201317. Springer (2012)","DOI":"10.1007\/978-3-642-30793-5_1"},{"key":"23_CR23","unstructured":"McNellis, J., Mola, J., Sykes, K.: Time travel debugging: Root causing bugs in commercial scale software. CppCon talk, https:\/\/www.youtube.com\/watch?v=l1YJTg_A914 (2017)"},{"key":"23_CR24","doi-asserted-by":"crossref","unstructured":"Melgratti, H.C., Mezzina, C.A., Ulidowski, I.: Reversing Place Transition nets. arXiv 1910, 04266 (2019)","DOI":"10.1007\/978-3-030-22397-7_2"},{"key":"23_CR25","doi-asserted-by":"crossref","unstructured":"Melgratti, H.C., Mezzina, C.A., Ulidowski, I.: Reversing P\/T nets. In: Nielson, H.R., Tuosto, E. (eds.) COORDINATION. LNCS, vol. 11533, pp. 19\u201336. Springer (2019)","DOI":"10.1007\/978-3-030-22397-7_2"},{"key":"23_CR26","doi-asserted-by":"crossref","unstructured":"Mezzina, C.A.: On reversibility and broadcast. In: Kari, J., Ulidowski, I. (eds.) RC 2018. LNCS, vol. 11106, pp. 67\u201383. Springer (2018)","DOI":"10.1007\/978-3-319-99498-7_5"},{"key":"23_CR27","doi-asserted-by":"crossref","unstructured":"Phillips, I., Ulidowski, I.: Reversing algebraic process calculi. In: Aceto, L., Ing\u00f3lfsd\u00f3ttir, A. (eds.) FoSSaCS. LNCS, vol. 3921, pp. 246\u2013260. Springer (2006)","DOI":"10.1007\/11690634_17"},{"key":"23_CR28","doi-asserted-by":"crossref","unstructured":"Phillips, I., Ulidowski, I.: Reversibility and models for concurrency. In: Hennessy, M., van Glabbeek, R. (eds.) SOS. ENTCS, vol. 192(1), pp. 93\u2013108. Elsevier (2007)","DOI":"10.1016\/j.entcs.2007.08.018"},{"key":"23_CR29","doi-asserted-by":"crossref","unstructured":"Phillips, I., Ulidowski, I.: Reversing algebraic process calculi. Journal of Logic and Algebraic Programming 73(1-2), 70\u201396 (2007)","DOI":"10.1016\/j.jlap.2006.11.002"},{"key":"23_CR30","doi-asserted-by":"crossref","unstructured":"Phillips, I., Ulidowski, I.: Reversibility and asymmetric conflict in event structures. Journal of Logical and Algebraic Methods in Programming 84, 781\u2013805 (2015)","DOI":"10.1016\/j.jlamp.2015.07.004"},{"key":"23_CR31","doi-asserted-by":"crossref","unstructured":"Phillips, I., Ulidowski, I., Yuen, S.: A reversible process calculus and the modelling of the ERK signalling pathway. In: Gl\u00fcck, R., Yokoyama, T. (eds.) RC. LNCS, vol. 7581, pp. 218\u2013232. Springer (2012)","DOI":"10.1007\/978-3-642-36315-3_18"},{"key":"23_CR32","doi-asserted-by":"crossref","unstructured":"Pin, J.: On the language accepted by finite reversible automata. In: Ottmann, T. (ed.) ICALP. LNCS, vol. 267, pp. 237\u2013249. Springer (1987)","DOI":"10.1007\/3-540-18088-5_19"},{"key":"23_CR33","doi-asserted-by":"crossref","unstructured":"Sassone, V., Nielsen, M., Winskel, G.: Models of concurrency: Towards a classification. Theoretical Computer Science 170(1\u20132), 297\u2013348 (1996)","DOI":"10.1016\/S0304-3975(96)80710-9"},{"key":"23_CR34","doi-asserted-by":"crossref","unstructured":"Ulidowski, I., Phillips, I., Yuen, S.: Reversing event structures. New Generation Computing 36(3), 281\u2013306 (2018)","DOI":"10.1007\/s00354-018-0040-8"},{"key":"23_CR35","doi-asserted-by":"crossref","unstructured":"Yokoyama, T., Gl\u00fcck, R.: A reversible programming language and its invertible self-interpreter. In: Ramalingam, G., Visser, E. (eds.) ACM SIGPLAN PEMP. pp. 144\u2013153. ACM (2007)","DOI":"10.1145\/1244381.1244404"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-45231-5_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,1,7]],"date-time":"2021-01-07T13:46:09Z","timestamp":1610027169000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-45231-5_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030452308","9783030452315"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-45231-5_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"17 April 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FoSSaCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Foundations of Software Science and Computation Structures","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Dublin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Ireland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 April 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 April 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2020\/fossacs","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"98","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"31","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"32% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"12","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference could not take place due to the COVID-19 pandemic. There was an online event on July 2, 2020.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}