{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,13]],"date-time":"2025-05-13T21:57:22Z","timestamp":1747173442512,"version":"3.40.5"},"reference-count":31,"publisher":"Cambridge University Press (CUP)","issue":"4","license":[{"start":{"date-parts":[[2022,4,12]],"date-time":"2022-04-12T00:00:00Z","timestamp":1649721600000},"content-version":"unspecified","delay-in-days":11,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2022,4]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We investigate how various forms of bisimulation can be characterised using the technology of logical relations. The approach taken is that each form of bisimulation corresponds to an algebraic structure derived from a transition system, and the general result is that a relation <jats:italic>R<\/jats:italic> between two transition systems on state spaces <jats:italic>S<\/jats:italic> and <jats:italic>T<\/jats:italic> is a bisimulation if and only if the derived algebraic structures are in the logical relation automatically generated from <jats:italic>R<\/jats:italic>. We show that this approach works for the original Park\u2013Milner bisimulation and that it extends to weak bisimulation, and branching and semi-branching bisimulation. The paper concludes with a discussion of probabilistic bisimulation, where the situation is slightly more complex, partly owing to the need to encompass bisimulations that are not just relations.<\/jats:p>","DOI":"10.1017\/s0960129522000020","type":"journal-article","created":{"date-parts":[[2022,4,12]],"date-time":"2022-04-12T03:00:12Z","timestamp":1649732412000},"page":"442-471","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":3,"title":["Bisimulation as a logical relation"],"prefix":"10.1017","volume":"32","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8148-8057","authenticated-orcid":false,"given":"Claudio","family":"Hermida","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Uday","family":"Reddy","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3075-2217","authenticated-orcid":false,"given":"Edmund","family":"Robinson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7683-5221","authenticated-orcid":false,"given":"Alessio","family":"Santamaria","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2022,4,12]]},"reference":[{"key":"S0960129522000020_ref20","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2015.08.002"},{"first-page":"190","year":"2018","author":"Sprunger","key":"S0960129522000020_ref29"},{"key":"S0960129522000020_ref30","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1123"},{"key":"S0960129522000020_ref19","unstructured":"Katsumata, S.-y. and Sato, T. (2015). Codensity liftings of monads. In: 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015), Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik."},{"key":"S0960129522000020_ref31","doi-asserted-by":"publisher","DOI":"10.1145\/233551.233556"},{"key":"S0960129522000020_ref14","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-4049(97)00129-1"},{"key":"S0960129522000020_ref18","article-title":"Relating apartness and bisimulation","author":"Jacobs","year":"2021","journal-title":"Logical Methods in Computer Science"},{"key":"S0960129522000020_ref21","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90030-6"},{"key":"S0960129522000020_ref23","doi-asserted-by":"publisher","DOI":"10.1142\/p595"},{"key":"S0960129522000020_ref8","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00035-3"},{"key":"S0960129522000020_ref9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15205-4_27"},{"key":"S0960129522000020_ref27","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00056-6"},{"key":"S0960129522000020_ref12","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2013.09.014"},{"key":"S0960129522000020_ref13","doi-asserted-by":"crossref","unstructured":"Hermida, C. (1993). Fibrations, Logical Predicates and Related Topics. Phd thesis, University of Edinburgh, 1993. Tech. Report ECS-LFCS-93-277. Also available as Aarhus Univ. DAIMI Tech. Report PB-462.","DOI":"10.7146\/dpb.v22i462.6935"},{"key":"S0960129522000020_ref4","unstructured":"Beohar, H. and K\u00dcpper, S. (2017). On path-based coalgebras and weak notions of bisimulation. arXiv preprint arXiv:1705.08715."},{"key":"S0960129522000020_ref5","unstructured":"Bonchi, F. , K\u00d6nig, B. and Petrisan, D. (2018). Up-to techniques for behavioural metrics via fibrations. In: 29th International Conference on Concurrency Theory."},{"first-page":"68","year":"1982","author":"Giry","key":"S0960129522000020_ref10"},{"key":"S0960129522000020_ref26","doi-asserted-by":"publisher","DOI":"10.1017\/S096012950000147X"},{"key":"S0960129522000020_ref22","unstructured":"Milner, R. (1989). Communication and Concurrency, vol. 84, New York, Prentice Hall etc."},{"key":"S0960129522000020_ref3","unstructured":"Baldan, P. , Bonchi, F. , Kerstan, H. and K\u00d6nig, B. (2014). Behavioral metrics via functor lifting. In: 34th International Conference on Foundation of Software Technology and Theoretical Computer Science, 403."},{"key":"S0960129522000020_ref6","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-11(2:14)2015"},{"first-page":"167","year":"1981","author":"Park","key":"S0960129522000020_ref24"},{"key":"S0960129522000020_ref25","doi-asserted-by":"publisher","DOI":"10.1137\/0205035"},{"key":"S0960129522000020_ref1","unstructured":"Aczel, P. (1988). Non-well-founded sets, volume 14 of CSLI lecture notes series. CSLI."},{"key":"S0960129522000020_ref11","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129508007172"},{"key":"S0960129522000020_ref2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(96)00232-0"},{"key":"S0960129522000020_ref7","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2001.2962"},{"key":"S0960129522000020_ref15","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1998.2725"},{"key":"S0960129522000020_ref28","first-page":"2009","article-title":"Coalgebraic weak bisimulation for action-type systems","volume":"19","author":"Sokolova","year":"2009","journal-title":"Scientific Annals of Computer Science"},{"key":"S0960129522000020_ref16","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2014.02.008"},{"key":"S0960129522000020_ref17","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(98)00176-5"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129522000020","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,16]],"date-time":"2022-12-16T12:27:00Z","timestamp":1671193620000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129522000020\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,4]]},"references-count":31,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2022,4]]}},"alternative-id":["S0960129522000020"],"URL":"https:\/\/doi.org\/10.1017\/s0960129522000020","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"type":"print","value":"0960-1295"},{"type":"electronic","value":"1469-8072"}],"subject":[],"published":{"date-parts":[[2022,4]]},"assertion":[{"value":"\u00a9 The Author(s), 2022. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (http:\/\/creativecommons.org\/licenses\/by\/4.0\/), which permits unrestricted re-use, distribution, and reproduction, provided the original article is properly cited.","name":"license","label":"License","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}