Document Open Access Logo

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

Authors Keri D'Angelo , Sebastian Gurke , Johanna Maria Kirss, Barbara König , Matina Najafi, Wojciech Różowski , Paul Wild

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2024.20.pdf
  • Filesize: 0.82 MB
  • 19 pages

Document Identifiers

Author Details

Keri D'Angelo
  • Cornell University, USA
Sebastian Gurke
  • Universität Duisburg-Essen, Germany
Johanna Maria Kirss
  • University of Copenhagen, Denmark
Barbara König
  • Universität Duisburg-Essen, Germany
Matina Najafi
  • Amirkabir University of Technology, Iran
Wojciech Różowski
  • University College London, UK
Paul Wild
  • FAU Erlangen-Nürnberg, Germany

Funding

Sebastian Gurke, Barbara König and Paul Wild: were supported by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) - project number 434050016 (SpeQt).
  • Kirss, Johanna Maria: was supported by NSF grant DMS-2216871.
  • Różowski, Wojciech: partially supported by ERC grant Autoprobe (no. 101002697).

Acknowledgements

We would like to thank Avi Craimer for helpful discussions and the organizers of the ACT Adjoint School for enabling us to meet and write this paper together!

Cite AsGet BibTex

Keri D'Angelo, Sebastian Gurke, Johanna Maria Kirss, Barbara König, Matina Najafi, Wojciech Różowski, and Paul Wild. Behavioural Metrics: Compositionality of the Kantorovich Lifting and an Application to Up-To Techniques. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 20:1-20:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Models of computation
Keywords
  • behavioural metrics
  • coalgebra
  • Galois connections
  • quantales
  • Kantorovich lifting
  • up-to techniques

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, and Radu Mardare. On-the-fly exact computation of bisimilarity distances. Logical Methods in Computer Science, 13(2:13):1-25, 2017. URL: https://doi.org/10.23638/LMCS-13(2:13)2017.
  2. Paolo Baldan, Filippo Bonchi, Henning Kerstan, and Barbara König. Coalgebraic behavioral metrics. Logical Methods in Computer Science, 14(3), 2018. Selected Papers of the 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). URL: https://doi.org/10.23638/LMCS-14(3:20)2018.
  3. Harsh Beohar, Sebastian Gurke, Barbara König, and Karla Messing. Hennessy-Milner theorems via Galois connections. In Proc. of CSL '23, volume 252 of LIPIcs, pages 12:1-12:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPIcs.CSL.2023.12.
  4. Harsh Beohar, Sebastian Gurke, Barbara König, Karla Messing, Jonas Forster, Lutz Schröder, and Paul Wild. Expressive quantale-valued logics for coalgebras: an adjunction-based approach. In Proc. of STACS '24, volume 289 of LIPIcs, pages 10:1-10:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPIcs.STACS.2024.10.
  5. Filippo Bonchi, Barbara König, and Daniela Petrişan. Up-to techniques for behavioural metrics via fibrations. Mathematical Structures in Computer Science, 33(4-5):182-221, 2023. URL: https://doi.org/10.1017/s0960129523000166.
  6. Filippo Bonchi, Daniela Petrisan, Damien Pous, and Jurriaan Rot. A general account of coinduction up-to. Acta Informatica, 54(2):127-190, 2017. URL: https://doi.org/10.1007/s00236-016-0271-4.
  7. Filippo Bonchi and Damien Pous. Checking NFA equivalence with bisimulations up to congruence. In Proc. of POPL '13, pages 457-468. ACM, 2013. URL: https://doi.org/10.1145/2429069.2429124.
  8. Filippo Bonchi, Alexandra Silva, and Ana Sokolova. The power of convex algebras. In Proc. of CONCUR '17, volume 85 of LIPIcs, pages 23:1-23:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2017.23.
  9. Konstantinos Chatzikokolakis, Daniel Gebler, Catuscia Palamidessi, and Lili Xu. Generalized bisimulation metrics. In Proc. of CONCUR '14. Springer, 2014. LNCS/ARCoSS 8704. URL: https://doi.org/10.1007/978-3-662-44584-6_4.
  10. Keri D'Angelo, Sebastian Gurke, Johanna Maria Kirss, Barbara König, Matina Najafi, Wojciech Różowski, and Paul Wild. Behavioural metrics: Compositionality of the Kantorovich lifting and an application to up-to techniques, 2024. arXiv:2404.19632. URL: https://doi.org/10.48550/arXiv.2404.19632.
  11. Luca de Alfaro, Marco Faella, and Mariëlle Stoelinga. Linear and branching system metrics. IEEE Transactions on Software Engineering, 35(2):258-273, 2009. URL: https://doi.org/10.1109/TSE.2008.106.
  12. Josée Desharnais, Vineet Gupta, Radha Jagadeesan, and Prakash Panangaden. Metrics for labelled Markov processes. Theoretical Computer Science, 318:323-354, 2004. URL: https://doi.org/10.1016/j.tcs.2003.09.013.
  13. Dirk Hofmann. Topological theories and closed objects. Adv. Math., 215(2):789-824, 2007. URL: https://doi.org/10.1016/j.aim.2007.04.013.
  14. Bart Jacobs. Categorical Logic and Type Theory, volume 141 of Studies in Logic and the Foundation of Mathematics. Elsevier, 1999. Google Scholar
  15. Bart Jacobs. A bialgebraic review of deterministic automata, regular expressions and languages. In Essays Dedicated to Joseph A. Goguen, pages 375-404. Springer, 2006. LNCS 4060. URL: https://doi.org/10.1007/11780274_20.
  16. Bart Jacobs. Introduction to Coalgebra. Towards Mathematics of States and Observations. Cambridge University Press, December 2016. URL: https://doi.org/10.1017/CBO9781316823187.
  17. Bart Jacobs, Alexandra Silva, and Ana Sokolova. Trace semantics via determinization. Journal of Computer and System Sciences, 81(5):859-879, 2015. URL: https://doi.org/10.1016/j.jcss.2014.12.005.
  18. Shin-ya Katsumata and Tetsuya Sato. Codensity liftings of monads. In Proc. of CALCO '15, volume 35 of LIPIcs, pages 156-170. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. URL: https://doi.org/10.4230/LIPIcs.CALCO.2015.156.
  19. Mayuko Kori, Kazuki Watanabe, Jurriaan Rot, and Shin ya Katsumata. Composing codensity bisimulations. In Proc. of LICS '24, pages 52:1-52:13. ACM, 2024. URL: https://doi.org/10.1145/3661814.3662139.
  20. Francis William Lawvere. Metric spaces, generalized logic, and closed categories. Rendiconti del seminario matématico e fisico di Milano, 43(1):135-166, 1973. URL: https://doi.org/10.1007/BF02924844.
  21. Radu Mardare, Prakash Panangaden, and Gordon Plotkin. Quantitative algebraic reasoning. In Proc. of LICS '16, pages 700-709. ACM, 2016. URL: https://doi.org/10.1145/2933575.2934518.
  22. E. J. McShane. Extension of range of functions. Bull. Amer. Math. Soc., 40(12):837-842, 1934. Google Scholar
  23. Damien Pous. Complete lattices and up-to techniques. In Proc. of APLAS '07, pages 351-366. Springer, 2007. LNCS 4807. URL: https://doi.org/10.1007/978-3-540-76637-7_24.
  24. J.J.M.M. Rutten. Universal coalgebra: a theory of systems. Theoretical Computer Science, 249:3-80, 2000. URL: https://doi.org/10.1016/S0304-3975(00)00056-6.
  25. Davide Sangiorgi. Introduction to Bisimulation and Coinduction. Cambridge University Press, 2011. Google Scholar
  26. Alexandra Silva, Filippo Bonchi, Marcello M. Bonsangue, and Jan J. M. M. Rutten. Generalizing determinization from automata to coalgebras. Logical Methods in Computer Science, 9(1:09), 2013. URL: https://doi.org/10.2168/LMCS-9(1:9)2013.
  27. Alfred Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 5:285-309, 1955. Google Scholar
  28. Franck van Breugel and James Worrell. A behavioural pseudometric for probabilistic transition systems. Theoretical Computer Science, 331:115-142, 2005. URL: https://doi.org/10.1016/j.tcs.2004.09.035.
  29. Cédric Villani. Optimal Transport - Old and New, volume 338 of A Series of Comprehensive Studies in Mathematics. Springer, 2009. Google Scholar
  30. Hassler Whitney. Analytic extensions of differentiable functions defined in closed sets. Transactions of the American Mathematical Society, 36(1):63-89, 1934. Google Scholar
  31. Paul Wild and Lutz Schröder. Characteristic logics for behavioural metrics via fuzzy lax extensions. In Proc. of CONCUR '20, volume 171 of LIPIcs, pages 27:1-27:23. Schloss Dagstuhl, 2020. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2020.27.
  32. Paul Wild and Lutz Schröder. Characteristic logics for behavioural hemimetrics via fuzzy lax extensions. Log. Methods Comput. Sci., 18(2), 2022. URL: https://doi.org/10.46298/lmcs-18(2:19)2022.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact