Behavioural Metrics: Compositionality of the Kantorovich Lifting and an Application to Up-To Techniques
D’Angelo K, Gurke S, Kirss JM, König B, Najafi M, Różowski W, Wild P (2024)
Publication Language: English
Publication Type: Conference contribution
Publication year: 2024
Journal
Publisher: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Book Volume: 311
Pages Range: 20
Conference Proceedings Title: 35th International Conference on Concurrency Theory (CONCUR 2024)
Event location: Calgary, AB
ISBN: 9783959773393
DOI: 10.4230/LIPIcs.CONCUR.2024.20
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.
Authors with CRIS profile
Involved external institutions
Cornell University
United States (USA) (US)
Universität Duisburg-Essen (UDE)
Germany (DE)
University of Copenhagen
Denmark (DK)
Amirkabir University of Technology (AUT) / دانشگاه صنعتی امیرکبیر
Iran, Islamic Republic of (IR)
University College London (UCL)
United Kingdom (GB)
United States (USA) (US)
Universität Duisburg-Essen (UDE)
Germany (DE)
University of Copenhagen
Denmark (DK)
Amirkabir University of Technology (AUT) / دانشگاه صنعتی امیرکبیر
Iran, Islamic Republic of (IR)
University College London (UCL)
United Kingdom (GB)
How to cite
APA:
D’Angelo, K., Gurke, S., Kirss, J.M., König, B., Najafi, M., Różowski, W., & Wild, P. (2024). Behavioural Metrics: Compositionality of the Kantorovich Lifting and an Application to Up-To Techniques. In Rupak Majumdar, Alexandra Silva (Eds.), 35th International Conference on Concurrency Theory (CONCUR 2024) (pp. 20). Calgary, AB, CA: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing.
MLA:
D’Angelo, Keri, et al. "Behavioural Metrics: Compositionality of the Kantorovich Lifting and an Application to Up-To Techniques." Proceedings of the 35th International Conference on Concurrency Theory, CONCUR 2024, Calgary, AB Ed. Rupak Majumdar, Alexandra Silva, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2024. 20.
BibTeX: Download