{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T05:24:04Z","timestamp":1776317044301,"version":"3.50.1"},"reference-count":63,"publisher":"Cambridge University Press (CUP)","issue":"4-5","license":[{"start":{"date-parts":[[2023,7,10]],"date-time":"2023-07-10T00:00:00Z","timestamp":1688947200000},"content-version":"unspecified","delay-in-days":100,"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":[[2023,4]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Up-to techniques are a well-known method for enhancing coinductive proofs of behavioural equivalences. We introduce up-to techniques for behavioural metrics between systems modelled as coalgebras, and we provide abstract results to prove their soundness in a compositional way.<\/jats:p><jats:p>In order to obtain a general framework, we need a systematic way to lift functors: we show that the Wasserstein lifting of a functor, introduced in a previous work, corresponds to a change of base in a fibrational sense. This observation enables us to reuse existing results about soundness of up-to techniques in a fibrational setting. We focus on the fibrations of predicates and relations valued in a quantale. To illustrate our approach, we provide an example on distances between regular languages.<\/jats:p>","DOI":"10.1017\/s0960129523000166","type":"journal-article","created":{"date-parts":[[2023,7,10]],"date-time":"2023-07-10T10:07:36Z","timestamp":1688983656000},"page":"182-221","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":3,"title":["Up-to techniques for behavioural metrics via fibrations"],"prefix":"10.1017","volume":"33","author":[{"given":"Filippo","family":"Bonchi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4193-2889","authenticated-orcid":false,"given":"Barbara","family":"K\u00f6nig","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniela","family":"Petri\u015fan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2023,7,10]]},"reference":[{"key":"S0960129523000166_ref53","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129598002527"},{"key":"S0960129523000166_ref57","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-00389-0_11"},{"key":"S0960129523000166_ref3","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22944-2_7"},{"key":"S0960129523000166_ref1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40313-2_9"},{"key":"S0960129523000166_ref10","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.07.019"},{"key":"S0960129523000166_ref54","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2007.09.023"},{"key":"S0960129523000166_ref19","doi-asserted-by":"crossref","unstructured":"Chatzikokolakis, K. , Gebler, D. , Palamidessi, C. and Xu, L. (2014). Generalized bisimulation metrics. In: CONCUR, LNCS\/ARCoSS, vol. 8704, Springer.","DOI":"10.1007\/978-3-662-44584-6_4"},{"key":"S0960129523000166_ref52","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00056-6"},{"key":"S0960129523000166_ref59","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1997.614955"},{"key":"S0960129523000166_ref17","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429124"},{"key":"S0960129523000166_ref28","doi-asserted-by":"publisher","DOI":"10.1016\/j.aim.2007.04.013"},{"key":"S0960129523000166_ref43","unstructured":"Milner, R. and Sangiorgi, D. (1992). Techniques of weak bisimulation up-to. In: CONCUR, LNCS, vol. 630, Springer-Verlag."},{"key":"S0960129523000166_ref37","doi-asserted-by":"publisher","DOI":"10.1109\/LICS52264.2021.9470656"},{"key":"S0960129523000166_ref44","doi-asserted-by":"publisher","DOI":"10.1109\/LICS52264.2021.9470717"},{"key":"S0960129523000166_ref7","unstructured":"Baldan, P. , Bonchi, F. , Kerstan, H. and K\u00f6nig, B. (2018). Coalgebraic behavioral metrics. Logical Methods in Computer Science 14 (3). Selected Papers of the 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)."},{"key":"S0960129523000166_ref49","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2934564"},{"key":"S0960129523000166_ref61","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.09.035"},{"key":"S0960129523000166_ref16","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-016-0271-4"},{"key":"S0960129523000166_ref6","unstructured":"Baldan, P. , Bonchi, F. , Kerstan, H. and K\u00f6nig, B. (2015). Towards trace metrics via functor lifting. In: CALCO, LIPIcs, vol. 35, 35\u201349."},{"key":"S0960129523000166_ref27","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1998.2725"},{"key":"S0960129523000166_ref21","doi-asserted-by":"crossref","unstructured":"Danielsson, N. 2017. Up-to techniques using sized types. In: POPL, vol. 2, ACM, 43:1\u201343:28.","DOI":"10.1145\/3158131"},{"key":"S0960129523000166_ref23","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2003.09.013"},{"key":"S0960129523000166_ref35","volume-title":"Lecture Notes in Mathematics","volume":"64","author":"Kelly","year":"1982"},{"key":"S0960129523000166_ref26","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2015.03.047"},{"key":"S0960129523000166_ref31","volume-title":"Categorical Logic and Type Theory","author":"Jacobs","year":"1999"},{"key":"S0960129523000166_ref2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS52264.2021.9470555"},{"key":"S0960129523000166_ref18","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785673"},{"key":"S0960129523000166_ref36","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2011.03.023"},{"key":"S0960129523000166_ref11","doi-asserted-by":"crossref","unstructured":"Blanchette, J. C. , Bouzy, A. , Lochbihler, A. , Popescu, A. and Traytel, D. (2017). Friends with benefits \u2013 implementing corecursion in foundational proof assistants. In: ESOP, LNCS, vol. 10201, Springer, 111\u2013140.","DOI":"10.1007\/978-3-662-54434-1_5"},{"key":"S0960129523000166_ref42","volume-title":"Communication and Concurrency","author":"Milner","year":"1989"},{"key":"S0960129523000166_ref14","unstructured":"Bonchi, F. , K\u00f6nig, B. and Petrisan, D. (2018b). Up-to techniques for behavioural metrics via fibrations. arXiv:https:\/\/org\/10.1017\/1806.110641806.11064."},{"key":"S0960129523000166_ref62","volume-title":"A Series of Comprehensive Studies in Mathematics","volume":"338","author":"Villani","year":"2009"},{"key":"S0960129523000166_ref58","first-page":"1","article-title":"Compositional bisimulation metric reasoning with probabilistic process calculi","volume":"12","author":"Tini","year":"2017","journal-title":"Logical Methods in Computer Science"},{"key":"S0960129523000166_ref20","unstructured":"Chatzikokolakis, K. , Palamidessi, C. and Vignudelli, V. (2016). Up-to techniques for generalized bisimulation metrics. In: CONCUR, LIPIcs, vol. 59, 35:1\u201335:14."},{"key":"S0960129523000166_ref24","volume-title":"Monographs in Theoretical Computer Science","author":"Droste","year":"2009"},{"key":"S0960129523000166_ref39","first-page":"1","article-title":"Metric spaces, generalized logic, and closed categories","volume":"1","author":"Lawvere","year":"2002","journal-title":"Reprints in Theory and Applications of Categories"},{"key":"S0960129523000166_ref13","doi-asserted-by":"crossref","unstructured":"Bonchi, F. , K\u00f6nig, B. and K\u00fcpper, S. (2017a). Up-to techniques for weighted systems. In: TACAS, LNCS, vol. 10205, Springer, 535\u2013552.","DOI":"10.1007\/978-3-662-54577-5_31"},{"key":"S0960129523000166_ref56","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exab051"},{"key":"S0960129523000166_ref12","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209169"},{"key":"S0960129523000166_ref9","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0060439"},{"key":"S0960129523000166_ref5","unstructured":"Baldan, P. , Bonchi, F. , Kerstan, H. and K\u00f6nig, B. (2014). Behavioral metrics via functor lifting. In: FSTTCS, LIPIcs, vol. 29, 403\u2013415."},{"key":"S0960129523000166_ref22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27836-8_11"},{"key":"S0960129523000166_ref33","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2014.12.005"},{"key":"S0960129523000166_ref45","unstructured":"Mio, M. and Vignudelli, V. (2020). Monads and quantitative equational theories for nondeterminism and probability. In: CONCUR, LIPIcs, vol. 171, 28:1\u201328:18."},{"key":"S0960129523000166_ref50","doi-asserted-by":"crossref","unstructured":"Pous, D. and Sangiorgi, D. (2011). Enhancements of the coinductive proof method. In: Sangiorgi, D. and Rutten, J. (eds.) Advanced Topics in Bisimulation and Coinduction, Cambridge University Press.","DOI":"10.1017\/CBO9780511792588"},{"key":"S0960129523000166_ref8","unstructured":"Baldan, P. , K\u00f6nig, B. and Padoan, T. (2020). Abstraction, up-to techniques and games for systems of fixpoint equations. In: CONCUR, LIPIcs, vol. 171, Schloss Dagstuhl \u2013 Leibniz Center for Informatics, 25:1\u201325:20."},{"key":"S0960129523000166_ref25","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46678-0_15"},{"key":"S0960129523000166_ref29","doi-asserted-by":"publisher","DOI":"10.1007\/s10485-020-09597-8"},{"key":"S0960129523000166_ref30","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429093"},{"key":"S0960129523000166_ref48","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-76637-7_24"},{"key":"S0960129523000166_ref51","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-019-00497-w"},{"key":"S0960129523000166_ref60","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48224-5_35"},{"key":"S0960129523000166_ref41","doi-asserted-by":"publisher","DOI":"10.1007\/s10208-011-9093-5"},{"key":"S0960129523000166_ref63","first-page":"1","article-title":"Characteristic logics for behavioural hemimetrics via fuzzy lax extensions","volume":"18","author":"Wild","year":"2022","journal-title":"Logical Methods in Computer Science"},{"key":"S0960129523000166_ref46","doi-asserted-by":"crossref","unstructured":"Parrow, J. and Weber, T. (2016). The largest respectful function. arXiv:https:\/\/org\/10.1017\/1605.041361605.04136.","DOI":"10.2168\/LMCS-12(2:11)2016"},{"key":"S0960129523000166_ref47","doi-asserted-by":"publisher","DOI":"10.1109\/LICS52264.2021.9470696"},{"key":"S0960129523000166_ref4","unstructured":"Balan, A. , Kurz, A. and Velebil, J. (2015). Extensions of functors from Set to inline1165-cat. In: CALCO, LIPIcs, vol. 35, 17\u201334."},{"key":"S0960129523000166_ref55","first-page":"1","article-title":"Generalizing determinization from automata to coalgebras","volume":"9","author":"Silva","year":"2013","journal-title":"Logical Methods in Computer Science"},{"key":"S0960129523000166_ref34","unstructured":"Katsumata, S. and Sato, T. (2015). Codensity liftings of monads. In: CALCO, LIPIcs, vol. 35, 156\u2013170."},{"key":"S0960129523000166_ref15","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603149"},{"key":"S0960129523000166_ref32","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781316823187"},{"key":"S0960129523000166_ref38","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785691"},{"key":"S0960129523000166_ref40","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2934518"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129523000166","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,11]],"date-time":"2023-09-11T02:06:52Z","timestamp":1694398012000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129523000166\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,4]]},"references-count":63,"journal-issue":{"issue":"4-5","published-print":{"date-parts":[[2023,4]]}},"alternative-id":["S0960129523000166"],"URL":"https:\/\/doi.org\/10.1017\/s0960129523000166","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,4]]},"assertion":[{"value":"\u00a9 The Author(s), 2023. 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"}]}}