2026-07-22T14:05:05Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:20792 2024-08-29T05:40:57Z ddc:004 open_access

Behavioural Metrics: Compositionality of the Kantorovich Lifting and an Application to Up-To Techniques D'Angelo, Keri Gurke, Sebastian Kirss, Johanna Maria König, Barbara Najafi, Matina Różowski, Wojciech Wild, Paul behavioural metrics coalgebra Galois connections quantales Kantorovich lifting up-to techniques Behavioural distances of transition systems modelled via coalgebras for endofunctors generalize traditional notions of behavioural equivalence to a quantitative setting, in which states are equipped with a measure of how (dis)similar they are. Endowing transition systems with such distances essentially relies on the ability to lift functors describing the one-step behavior of the transition systems to the category of pseudometric spaces. We consider the category theoretic generalization of the Kantorovich lifting from transportation theory to the case of lifting functors to quantale-valued relations, which subsumes equivalences, preorders and (directed) metrics. We use tools from fibred category theory, which allow one to see the Kantorovich lifting as arising from an appropriate fibred adjunction. Our main contributions are compositionality results for the Kantorovich lifting, where we show that that the lifting of a composed functor coincides with the composition of the liftings. In addition, we describe how to lift distributive laws in the case where one of the two functors is polynomial (with finite coproducts). These results are essential ingredients for adapting up-to-techniques to the case of quantale-valued behavioural distances. Up-to techniques are a well-known coinductive technique for efficiently showing lower bounds for behavioural distances. We illustrate the results of our paper in two case studies. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Keri D'Angelo and Sebastian Gurke and Johanna Maria Kirss and Barbara König and Matina Najafi and Wojciech Różowski and Paul Wild 2024 Is Part Of LIPIcs, Volume 311, 35th International Conference on Concurrency Theory (CONCUR 2024) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CONCUR.2024.20 urn:nbn:de:0030-drops-207921 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.20 eng https://creativecommons.org/licenses/by/4.0/legalcode