{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,18]],"date-time":"2025-10-18T21:04:57Z","timestamp":1760821497572,"version":"3.40.4"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031908965"},{"type":"electronic","value":"9783031908972"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T00:00:00Z","timestamp":1746057600000},"content-version":"vor","delay-in-days":120,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>We provide two alternative characterizations of hereditary history-preserving bisimilarity: a denotational one, on stable configuration structures, and an operational one, on a reversible process calculus.\u00a0The characterizing equivalence is forward-reverse bisimilarity extended with a check for backward ready multiset equality. Unlike previous approaches, the focus is thus on counting identically labeled events rather\u00a0than uniquely identifying them. We also investigate the relationships between event identifier logic, characterizing the former bisimilarity, and backward ready multiset logic, characterizing the latter bisimilarity.<\/jats:p>","DOI":"10.1007\/978-3-031-90897-2_4","type":"book-chapter","created":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T08:17:18Z","timestamp":1746001038000},"page":"67-87","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Alternative Characterizations of Hereditary History-Preserving Bisimilarity via Backward Ready Multisets"],"prefix":"10.1007","author":[{"given":"Marco","family":"Bernardo","sequence":"first","affiliation":[]},{"given":"Andrea","family":"Esposito","sequence":"additional","affiliation":[]},{"given":"Claudio A.","family":"Mezzina","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,5,1]]},"reference":[{"key":"4_CR1","doi-asserted-by":"crossref","unstructured":"Aubert, C.: Concurrencies in reversible concurrent calculi. In: Proc. of the 14th Int. Conf. on Reversible Computation (RC\u00a02022). LNCS, vol. 13354, pp. 146\u2013163. Springer (2022)","DOI":"10.1007\/978-3-031-09005-9_10"},{"key":"4_CR2","doi-asserted-by":"crossref","unstructured":"Aubert, C., Cristescu, I.: Contextual equivalences in configuration structures and reversibility. Journal of Logical and Algebraic Methods in Programming 86, 77\u2013106 (2017)","DOI":"10.1016\/j.jlamp.2016.08.004"},{"key":"4_CR3","unstructured":"Aubert, C., Cristescu, I.: How reversibility can solve traditional questions: The example of hereditary history-preserving bisimulation. In: Proc. of the 31st Int. Conf. on Concurrency Theory (CONCUR\u00a02020). LIPIcs, vol.\u00a0171, pp. 7:1\u20137:23 (2020)"},{"key":"4_CR4","doi-asserted-by":"crossref","unstructured":"Baldan, P., Crafa, S.: A logic for true concurrency. Journal of the ACM 61, 24:1\u201324:36 (2014)","DOI":"10.1145\/2629638"},{"key":"4_CR5","doi-asserted-by":"crossref","unstructured":"Baldan, P., Gorla, D., Padoan, T., Salvo, I.: Behavioural logics for configuration structures. Theoretical Computer Science 913, 94\u2013112 (2022)","DOI":"10.1016\/j.tcs.2022.02.018"},{"key":"4_CR6","unstructured":"Bednarczyk, M.A.: Hereditary history preserving bisimulations or what is the power of the future perfect in program logics. Technical Report, Polish Academy of Sciences, Gdansk (1991)"},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"Bernardo, M., Esposito, A.: Modal logic characterizations of forward, reverse, and forward-reverse bisimilarities. In: Proc. of the 14th Int. Symp. on Games, Automata, Logics, and Formal Verification (GANDALF\u00a02023). EPTCS, vol.\u00a0390, pp. 67\u201381 (2023)","DOI":"10.4204\/EPTCS.390.5"},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"Bernardo, M., Esposito, A., Mezzina, C.A.: Expansion laws for forward-reverse, forward, and reverse bisimilarities via proved encodings. In: Proc. of the Combined 31st Int. Workshop on Expressiveness in Concurrency and 21st Workshop on Structural Operational Semantics (EXPRESS\/SOS\u00a02024). EPTCS, vol.\u00a0412, pp. 51\u201370 (2024)","DOI":"10.4204\/EPTCS.412.5"},{"key":"4_CR9","doi-asserted-by":"crossref","unstructured":"Bernardo, M., Rossi, S.: Reverse bisimilarity vs. forward bisimilarity. In: Proc. of the 26th Int. Conf. on Foundations of Software Science and Computation Structures (FOSSACS\u00a02023). LNCS, vol. 13992, pp. 265\u2013284. Springer (2023)","DOI":"10.1007\/978-3-031-30829-1_13"},{"key":"4_CR10","doi-asserted-by":"crossref","unstructured":"Boudol, G., Castellani, I.: A non-interleaving semantics for CCS based on proved transitions. Fundamenta Informaticae 11, 433\u2013452 (1988)","DOI":"10.3233\/FI-1988-11406"},{"key":"4_CR11","doi-asserted-by":"crossref","unstructured":"Boudol, G., Castellani, I.: Flow models of distributed computations: Three equivalent semantics for CCS. Information and Computation 114, 247\u2013314 (1994)","DOI":"10.1006\/inco.1994.1088"},{"key":"4_CR12","doi-asserted-by":"crossref","unstructured":"Brookes, S.D., Hoare, C.A.R., Roscoe, A.W.: A theory of communicating sequential processes. Journal of the ACM 31, 560\u2013599 (1984)","DOI":"10.1145\/828.833"},{"key":"4_CR13","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":"4_CR14","doi-asserted-by":"crossref","unstructured":"Danos, V., Krivine, J.: Transactions in RCCS. In: Proc. of the 16th Int. Conf. on Concurrency Theory (CONCUR\u00a02005). LNCS, vol.\u00a03653, pp. 398\u2013412. Springer (2005)","DOI":"10.1007\/11539452_31"},{"key":"4_CR15","doi-asserted-by":"crossref","unstructured":"Darondeau, P., Degano, P.: Causal trees. In: Proc. of the 16th Int. Coll. on Automata, Languages and Programming (ICALP\u00a01989). LNCS, vol.\u00a0372, pp. 234\u2013248. Springer (1989)","DOI":"10.1007\/BFb0035764"},{"key":"4_CR16","doi-asserted-by":"crossref","unstructured":"Darondeau, P., Degano, P.: Causal trees: Interleaving + causality. In: Proc. of the LITP Spring School on Theoretical Computer Science: Semantics of Systems of Concurrent Processes. LNCS, vol.\u00a0469, pp. 239\u2013255. Springer (1990)","DOI":"10.1007\/3-540-53479-2_10"},{"key":"4_CR17","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":"4_CR18","doi-asserted-by":"crossref","unstructured":"Degano, P., Priami, C.: Proved trees. In: Proc. of the 19th Int. Coll. on Automata, Languages and Programming (ICALP\u00a01992). LNCS, vol.\u00a0623, pp. 629\u2013640. Springer (1992)","DOI":"10.1007\/3-540-55719-9_110"},{"key":"4_CR19","doi-asserted-by":"crossref","unstructured":"Fecher, H.: A completed hierarchy of true concurrent equivalences. Information Processing Letters 89, 261\u2013265 (2004)","DOI":"10.1016\/j.ipl.2003.11.008"},{"key":"4_CR20","doi-asserted-by":"crossref","unstructured":"Fr\u00f6schle, S., Jan\u010dar, P., Lasota, S., Sawa, Z.: Non-interleaving bisimulation equivalences on basic parallel processes. Information and Computation 208, 42\u201362 (2010)","DOI":"10.1016\/j.ic.2009.06.001"},{"key":"4_CR21","doi-asserted-by":"crossref","unstructured":"Fr\u00f6schle, S., Lasota, S.: Decomposition and complexity of hereditary history preserving bisimulation on BPP. In: Proc. of the 16th Int. Conf. on Concurrency Theory (CONCUR\u00a02005). LNCS, vol.\u00a03653, pp. 263\u2013277. Springer (2005)","DOI":"10.1007\/11539452_22"},{"key":"4_CR22","doi-asserted-by":"crossref","unstructured":"van Glabbeek, R.J.: On the expressiveness of higher dimensional automata. Theoretical Computer Science 368, 168\u2013194 (2006)","DOI":"10.1016\/j.tcs.2006.06.024"},{"key":"4_CR23","doi-asserted-by":"crossref","unstructured":"van Glabbeek, R.J., Goltz, U.: Refinement of actions and equivalence notions for concurrent systems. Acta Informatica 37, 229\u2013327 (2001)","DOI":"10.1007\/s002360000041"},{"key":"4_CR24","doi-asserted-by":"crossref","unstructured":"van Glabbeek, R.J., Plotkin, G.D.: Configuration structures, event structures and Petri nets. Theoretical Computer Science 410, 4111\u20134159 (2009)","DOI":"10.1016\/j.tcs.2009.06.014"},{"key":"4_CR25","doi-asserted-by":"crossref","unstructured":"Joyal, A., Nielsen, M., Winskel, G.: Bisimulation from open maps. Information and Computation 127, 164\u2013185 (1996)","DOI":"10.1006\/inco.1996.0057"},{"key":"4_CR26","doi-asserted-by":"crossref","unstructured":"Jurdzinski, M., Nielsen, M., Srba, J.: Undecidability of domino games and hhp-bisimilarity. Information and Computation 184, 343\u2013368 (2003)","DOI":"10.1016\/S0890-5401(03)00064-6"},{"key":"4_CR27","doi-asserted-by":"crossref","unstructured":"Krivine, J.: A verification technique for reversible process algebra. In: Proc. of the 4th Int. Workshop on Reversible Computation (RC\u00a02012). LNCS, vol.\u00a07581, pp. 204\u2013217. Springer (2012)","DOI":"10.1007\/978-3-642-36315-3_17"},{"key":"4_CR28","doi-asserted-by":"crossref","unstructured":"Lanese, I., Medi\u0107, D., Mezzina, C.A.: Static versus dynamic reversibility in CCS. Acta Informatica 58, 1\u201334 (2021)","DOI":"10.1007\/s00236-019-00346-6"},{"key":"4_CR29","unstructured":"Milner, R.: Communication and Concurrency. Prentice Hall (1989)"},{"key":"4_CR30","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":"4_CR31","doi-asserted-by":"crossref","unstructured":"Phillips, I., Ulidowski, I.: Reversibility and models for concurrency. In: Proc. of the 4th Int. Workshop on Structural Operational Semantics (SOS\u00a02007). ENTCS, vol. 192(1), pp. 93\u2013108. Elsevier (2007)","DOI":"10.1016\/j.entcs.2007.08.018"},{"key":"4_CR32","doi-asserted-by":"crossref","unstructured":"Phillips, I., Ulidowski, I.: A hierarchy of reverse bisimulations on stable configuration structures. Mathematical Structures in Computer Science 22, 333\u2013372 (2012)","DOI":"10.1017\/S0960129511000429"},{"key":"4_CR33","doi-asserted-by":"crossref","unstructured":"Phillips, I., Ulidowski, I.: Event identifier logic. Mathematical Structures in Computer Science 24(2), 1\u201351 (2014)","DOI":"10.1017\/S0960129513000510"},{"key":"4_CR34","doi-asserted-by":"crossref","unstructured":"Rabinovich, A.M., Trakhtenbrot, B.A.: Behavior structures and nets. Fundamenta Informaticae 11, 357\u2013404 (1988)","DOI":"10.3233\/FI-1988-11404"},{"key":"4_CR35","doi-asserted-by":"crossref","unstructured":"Winskel, G.: Event structures. In: Advances in Petri Nets. LNCS, vol.\u00a0255, pp. 325\u2013392. Springer (1986)","DOI":"10.1007\/3-540-17906-2_31"}],"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-90897-2_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T08:17:44Z","timestamp":1746001064000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-90897-2_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031908965","9783031908972"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-90897-2_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"1 May 2025","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":"Hamilton, ON","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 May 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2025\/conferences\/fossacs\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}