Behavioural Metrics: Compositionality of the Kantorovich Lifting and an Application to Up-To Techniques
Keri D'Angelo, Sebastian Gurke, Johanna Maria Kirss, Barbara König, Matina Najafi, Wojciech Różowski, Paul Wild
TL;DR
This work develops a category-theoretic framework for quantitative coalgebraic semantics via Kantorovich liftings to quantale-valued relations. By embedding liftings in a fibred adjunction between V-valued predicates and V-graphs, it derives compositionality results for liftings, proving a positive result for polynomial functors with finite coproducts and identifying limitations in mixed cases. It further shows how to lift distributive laws in polynomial settings, enabling up-to techniques that streamline reasoning about behavioural distances. The approach provides concrete mechanisms to handle trace-like metrics and determinization-inspired conformances, with case studies illustrating practical benefits and limitations of Kantorovich versus Wasserstein liftings in quantale-valued settings.
Abstract
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.