{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,18]],"date-time":"2025-10-18T21:05:09Z","timestamp":1760821509084,"version":"3.41.2"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2019,8,7]],"date-time":"2019-08-07T00:00:00Z","timestamp":1565136000000},"content-version":"am","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2019,8,7]],"date-time":"2019-08-07T00:00:00Z","timestamp":1565136000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2019,8,7]],"date-time":"2019-08-07T00:00:00Z","timestamp":1565136000000},"content-version":"tdm","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"}]},{"DOI":"10.13039\/501100000780","name":"European Commission","doi-asserted-by":"crossref","award":["778233"],"award-info":[{"award-number":["778233"]}],"id":[{"id":"10.13039\/501100000780","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100001665","name":"French National Research Agency","doi-asserted-by":"crossref","award":["ANR-16-CE25-0011"],"award-info":[{"award-number":["ANR-16-CE25-0011"]}],"id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100001665","name":"French National Research Agency","doi-asserted-by":"crossref","award":["ANR-10-LABX-0070"],"award-info":[{"award-number":["ANR-10-LABX-0070"]}],"id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"accepted":{"date-parts":[[2025,3,31]]},"abstract":"<jats:p>We study proof techniques for bisimilarity based on unique solution of equations. We draw inspiration from a result by Roscoe in the denotational setting of CSP and for failure semantics, essentially stating that an equation (or a system of equations) whose infinite unfolding never produces a divergence has the unique-solution property. We transport this result onto the operational setting of CCS and for bisimilarity. We then exploit the operational approach to: refine the theorem, distinguishing between different forms of divergence; derive an abstract formulation of the theorems, on generic LTSs; adapt the theorems to other equivalences such as trace equivalence, and to preorders such as trace inclusion. We compare the resulting techniques to enhancements of the bisimulation proof method (the `up-to techniques'). Finally, we study the theorems in name-passing calculi such as the asynchronous $\\pi$-calculus, and use them to revisit the completeness part of the proof of full abstraction of Milner's encoding of the $\\lambda$-calculus into the $\\pi$-calculus for L\\'evy-Longo Trees.<\/jats:p><jats:p>Comment: This is an extended version of the paper with the same title   published in the proceedings of CONCUR'17<\/jats:p>","DOI":"10.23638\/lmcs-15(3:12)2019","type":"journal-article","created":{"date-parts":[[2025,4,3]],"date-time":"2025-04-03T17:38:03Z","timestamp":1743701883000},"source":"Crossref","is-referenced-by-count":1,"title":["Divergence and unique solution of equations"],"prefix":"10.23638","volume":"Volume 15, Issue 3","author":[{"given":"Adrien","family":"Durier","sequence":"first","affiliation":[]},{"given":"Daniel","family":"Hirschkoff","sequence":"additional","affiliation":[]},{"given":"Davide","family":"Sangiorgi","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2019,8,7]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/arxiv.org\/pdf\/1806.11354v3","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/arxiv.org\/pdf\/1806.11354v3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,3]],"date-time":"2025-04-03T17:38:04Z","timestamp":1743701884000},"score":1,"resource":{"primary":{"URL":"http:\/\/lmcs.episciences.org\/4653"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,8,7]]},"references-count":0,"URL":"https:\/\/doi.org\/10.23638\/lmcs-15(3:12)2019","relation":{"has-preprint":[{"id-type":"arxiv","id":"1806.11354v2","asserted-by":"subject"},{"id-type":"arxiv","id":"1806.11354v1","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"1806.11354","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1806.11354","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2019,8,7]]},"article-number":"4653"}}