{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T16:29:15Z","timestamp":1759336155371,"version":"3.40.3"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031308284"},{"type":"electronic","value":"9783031308291"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,4,21]],"date-time":"2023-04-21T00:00:00Z","timestamp":1682035200000},"content-version":"vor","delay-in-days":110,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Reversibility is the capability of a system of undoing its own actions starting from the last performed one, in such a way that a past consistent state is reached. This is not trivial for concurrent systems, as the last performed action may not be uniquely identifiable. There are several approaches to address causality-consistent reversibility, some including a notion of forward-reverse bisimilarity. We introduce a minimal process calculus for reversible systems to investigate compositionality properties and equational characterizations of forward-reverse bisimilarity as well as of its two components, i.e., forward bisimilarity and reverse bisimilarity, so as to highlight their differences. The study is conducted not only in a nondeterministic setting, but also in a stochastic one where time reversibility and lumpability for Markov chains are exploited.<\/jats:p>","DOI":"10.1007\/978-3-031-30829-1_13","type":"book-chapter","created":{"date-parts":[[2023,4,20]],"date-time":"2023-04-20T19:56:19Z","timestamp":1682020579000},"page":"265-284","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Reverse Bisimilarity vs. Forward Bisimilarity"],"prefix":"10.1007","author":[{"given":"Marco","family":"Bernardo","sequence":"first","affiliation":[]},{"given":"Sabina","family":"Rossi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,4,21]]},"reference":[{"key":"13_CR1","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1016\/0304-3975(87)90065-X","volume":"53","author":"S Abramsky","year":"1987","unstructured":"Abramsky, S.: Observational equivalence as a testing equivalence. TheoreticalComputer Science 53, 225\u2013241 (1987)","journal-title":"Theoretical Computer Science"},{"key":"13_CR2","doi-asserted-by":"crossref","unstructured":"Baarir, S., Beccuti, M., Dutheillet, C., Franceschinis, G., Haddad, S.: Lumping partially symmetrical stochastic models. Performance Evaluation 68, 21\u201344 (2011)","DOI":"10.1016\/j.peva.2010.09.002"},{"key":"13_CR3","doi-asserted-by":"crossref","unstructured":"Bennett, C.H.: Logical reversibility of computations. IBM Journal of Research and Development 17, 525\u2013532 (1973)","DOI":"10.1147\/rd.176.0525"},{"key":"13_CR4","doi-asserted-by":"crossref","unstructured":"Bernardo, M., Mezzina, C.A.: Towards bridging time and causal reversibility. In: Proc. of the 40th Int. Conf. on Formal Techniques for Distributed Objects, Components, and Systems (FORTE\u00a02020). LNCS, vol. 12136, pp. 22\u201338. Springer (2020)","DOI":"10.1007\/978-3-030-50086-3_2"},{"key":"13_CR5","doi-asserted-by":"crossref","unstructured":"Buchholz, P.: Exact and ordinary lumpability in finite Markov chains. Journal of Applied Probability 31, 59\u201375 (1994)","DOI":"10.2307\/3215235"},{"key":"13_CR6","doi-asserted-by":"crossref","unstructured":"Buchholz, P.: Exact performance equivalence: An equivalence relation for stochastic automata. Theoretical Computer Science 215, 263\u2013287 (1999)","DOI":"10.1016\/S0304-3975(98)00169-8"},{"key":"13_CR7","doi-asserted-by":"crossref","unstructured":"Danos, V., Krivine, J.: Reversible communicating systems. In: Proc. of the 15th Int. Conf. on Concurrency Theory (CONCUR\u00a02004). LNCS, vol.\u00a03170, pp. 292\u2013307. Springer (2004)","DOI":"10.1007\/978-3-540-28644-8_19"},{"key":"13_CR8","doi-asserted-by":"crossref","unstructured":"De\u00a0Nicola, R., Montanari, U., Vaandrager, F.: Back and forth bisimulations. In: Proc. of the 1st Int. Conf. on Concurrency Theory (CONCUR\u00a01990). LNCS, vol.\u00a0458, pp. 152\u2013165. Springer (1990)","DOI":"10.1007\/BFb0039058"},{"key":"13_CR9","unstructured":"van Glabbeek, R.J.: The linear time \u2013 branching time spectrum\u00a0I. In: Handbook of Process Algebra. pp. 3\u201399. Elsevier (2001)"},{"key":"13_CR10","doi-asserted-by":"crossref","unstructured":"Harrison, P.: Turning back time in Markovian process algebra. Theoretical Computer Science 290, 1947\u20131986 (2003)","DOI":"10.1016\/S0304-3975(02)00375-4"},{"key":"13_CR11","doi-asserted-by":"crossref","unstructured":"Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. Journal of the ACM 32, 137\u2013162 (1985)","DOI":"10.1145\/2455.2460"},{"key":"13_CR12","doi-asserted-by":"crossref","unstructured":"Hillston, J.: A Compositional Approach to Performance Modelling. Cambridge University Press (1996)","DOI":"10.1017\/CBO9780511569951"},{"key":"13_CR13","unstructured":"Kelly, F.: Reversibility and Stochastic Networks. John Wiley & Sons (1979)."},{"key":"13_CR14","unstructured":"Kemeny, J.G., Snell, J.L.: Finite Markov Chains. Van Nostrand (1960)"},{"key":"13_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":"13_CR16","doi-asserted-by":"crossref","unstructured":"Lanese, I., Phillips, I.: Forward-reverse observational equivalences in CCSK. In: Proc. of the 13th Int. Conf. on Reversible Computation (RC\u00a02021). LNCS, vol. 12805, pp. 126\u2013143. Springer (2021)","DOI":"10.1007\/978-3-030-79837-6_8"},{"key":"13_CR17","doi-asserted-by":"crossref","unstructured":"Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Information and Computation 94, 1\u201328 (1991)","DOI":"10.1016\/0890-5401(91)90030-6"},{"key":"13_CR18","doi-asserted-by":"crossref","unstructured":"Marin, A., Rossi, S.: On the relations between lumpability and reversibility. In: Proc. of the 22nd IEEE Int. Symp. on Modeling, Analysis and Simulation of Computer and Telecommunication Systems (MASCOTS 2014). pp. 427\u2013432. IEEE-CS Press (2014)","DOI":"10.1109\/MASCOTS.2014.59"},{"key":"13_CR19","doi-asserted-by":"crossref","unstructured":"Marin, A., Rossi, S.: On the relations between Markov chain lumpability and reversibility. Acta Informatica 54, 447\u2013485 (2017)","DOI":"10.1007\/s00236-016-0266-1"},{"key":"13_CR20","unstructured":"Milner, R.: Communication and Concurrency. Prentice Hall (1989)"},{"key":"13_CR21","doi-asserted-by":"crossref","unstructured":"Palacios, J.L., Quiroz, D.: Birth and death chains on finite trees: Computing their stationary distribution and hitting times. Methodology and Computing in Applied Probability 18, 487\u2013498 (2016)","DOI":"10.1007\/s11009-014-9436-1"},{"key":"13_CR22","doi-asserted-by":"crossref","unstructured":"Park, D.: Concurrency and automata on infinite sequences. In: Proc. of the 5th GI Conf. on Theoretical Computer Science. LNCS, vol.\u00a0104, pp. 167\u2013183. Springer (1981)","DOI":"10.1007\/BFb0017309"},{"key":"13_CR23","doi-asserted-by":"crossref","unstructured":"Pearce, L.H.: Random walks on trees. Discrete Mathematics 30, 269\u2013276 (1980)","DOI":"10.1016\/0012-365X(80)90234-4"},{"key":"13_CR24","doi-asserted-by":"crossref","unstructured":"Phillips, I., Ulidowski, I.: Reversing algebraic process calculi. Journal of Logic and Algebraic Programming 73, 70\u201396 (2007)","DOI":"10.1016\/j.jlap.2006.11.002"},{"key":"13_CR25","unstructured":"Schweitzer, P.J.: Aggregation methods for large Markov chains. In: Proc. of the Int. Workshop on Computer Performance and Reliability. pp. 275\u2013286. North Holland (1984)"},{"key":"13_CR26","doi-asserted-by":"crossref","unstructured":"Sproston, J., Donatelli, S.: Backward bisimulation in Markov chain model checking. IEEE Trans. on Software Engineering 32, 531\u2013546 (2006)","DOI":"10.1109\/TSE.2006.74"},{"key":"13_CR27","doi-asserted-by":"crossref","unstructured":"Stewart, W.: Introduction to the Numerical Solution of Markov Chains. Princeton University Press (1994)","DOI":"10.1515\/9780691223384"},{"key":"13_CR28","doi-asserted-by":"crossref","unstructured":"Sumita, U., Rieders, M.: Lumpability and time reversibility in the aggregation-disaggregation method for large Markov chains. Communications in Statistics - Stochastic Models 5, 63\u201381 (1989)","DOI":"10.1080\/15326348908807099"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-30829-1_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,20]],"date-time":"2023-04-20T19:59:22Z","timestamp":1682020762000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-30829-1_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031308284","9783031308291"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-30829-1_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"21 April 2023","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":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 April 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 April 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2023\/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":"85","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":"26","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":"31% - 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.1","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":"10","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)"}}]}}