Behavioural Metrics: Compositionality of the Kantorovich Lifting and an Application to Up-To Techniques

TL;DR

This paper develops a compositional framework for lifting functors to quantale-valued relations, enabling the application of up-to techniques to behavioral distances in transition systems modeled by coalgebras.

Contribution

It introduces a fibred category approach to the Kantorovich lifting, proving compositionality and lifting distributive laws for polynomial functors, facilitating advanced behavioral distance analysis.

Findings

Proves that lifting of composed functors equals composition of liftings.

Provides methods to lift distributive laws with polynomial functors.

Demonstrates applicability through two case studies.

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.