2026-07-23T16:34:03Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:9555 2024-03-06T10:44:42Z ddc:004 open_access

Up-To Techniques for Behavioural Metrics via Fibrations Bonchi, Filippo König, Barbara Petrisan, Daniela behavioural metrics bisimilarity up-to techniques coalgebras fibrations 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. 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, for which pseudo-metric spaces are an example. To illustrate our approach we provide an example on distances between regular languages. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Filippo Bonchi and Barbara König and Daniela Petrisan 2018 Is Part Of LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CONCUR.2018.17 urn:nbn:de:0030-drops-95552 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.17 eng https://creativecommons.org/licenses/by/3.0/legalcode