{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,15]],"date-time":"2025-11-15T19:13:45Z","timestamp":1763234025908,"version":"3.41.2"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2021,8,10]],"date-time":"2021-08-10T00:00:00Z","timestamp":1628553600000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100000780","name":"European Commission","doi-asserted-by":"crossref","award":["678157"],"award-info":[{"award-number":["678157"]}],"id":[{"id":"10.13039\/501100000780","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>Open bisimilarity is defined for open process terms in which free variables\nmay appear. The insight is, in order to characterise open bisimilarity, we move\nto the setting of intuitionistic modal logics. The intuitionistic modal logic\nintroduced, called $\\mathcal{OM}$, is such that modalities are closed under\nsubstitutions, which induces a property known as intuitionistic hereditary.\nIntuitionistic hereditary reflects in logic the lazy instantiation of free\nvariables performed when checking open bisimilarity. The soundness proof for\nopen bisimilarity with respect to our intuitionistic modal logic is mechanised\nin Abella. The constructive content of the completeness proof provides an\nalgorithm for generating distinguishing formulae, which we have implemented. We\ndraw attention to the fact that there is a spectrum of bisimilarity congruences\nthat can be characterised by intuitionistic modal logics.<\/jats:p>","DOI":"10.46298\/lmcs-17(3:2)2021","type":"journal-article","created":{"date-parts":[[2021,7,27]],"date-time":"2021-07-27T09:54:51Z","timestamp":1627379691000},"source":"Crossref","is-referenced-by-count":1,"title":["A Characterisation of Open Bisimilarity using an Intuitionistic Modal Logic"],"prefix":"10.46298","volume":"Volume 17, Issue 3","author":[{"given":"Ki Yung","family":"Ahn","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ross","family":"Horne","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alwen","family":"Tiu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"25203","published-online":{"date-parts":[[2021,8,10]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/7685\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/7685\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,20]],"date-time":"2023-06-20T20:17:04Z","timestamp":1687292224000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/4666"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,8,10]]},"references-count":0,"URL":"https:\/\/doi.org\/10.46298\/lmcs-17(3:2)2021","relation":{"has-preprint":[{"id-type":"arxiv","id":"1701.05324v4","asserted-by":"subject"},{"id-type":"arxiv","id":"1701.05324v3","asserted-by":"subject"},{"id-type":"arxiv","id":"1701.05324v2","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"1701.05324","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1701.05324","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2021,8,10]]},"article-number":"4666"}}