Kantorovich Functors and Characteristic Logics for Behavioural Distances

Goncharov S, Hofmann D, Nora P, Schröder L, Wild P (2023)

Publication Type: Conference contribution

Publication year: 2023

Journal

Lecture Notes in Computer Science Springer Verlag

Publisher: Springer Science and Business Media Deutschland GmbH

Book Volume: 13992 LNCS

Pages Range: 46-67

Conference Proceedings Title: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

Event location: Paris, FRA

ISBN: 9783031308284

DOI: 10.1007/978-3-031-30829-1_3

Abstract

Behavioural distances measure the deviation between states in quantitative systems, such as probabilistic or weighted systems. There is growing interest in generic approaches to behavioural distances. In particular, coalgebraic methods capture variations in the system type (nondeterministic, probabilistic, game-based etc.), and the notion of quantale abstracts over the actual values distances take, thus covering, e.g., two-valued equivalences, (pseudo)metrics, and probabilistic (pseudo)metrics. Coalgebraic behavioural distances have been based either on liftings of Set -functors to categories of metric spaces, or on lax extensions of Set -functors to categories of quantitative relations. Every lax extension induces a functor lifting but not every lifting comes from a lax extension. It was shown recently that every lax extension is Kantorovich, i.e. induced by a suitable choice of monotone predicate liftings, implying via a quantitative coalgebraic Hennessy-Milner theorem that behavioural distances induced by lax extensions can be characterized by quantitative modal logics. Here, we essentially show the same in the more general setting of behavioural distances induced by functor liftings. In particular, we show that every functor lifting, and indeed every functor on (quantale-valued) metric spaces, that preserves isometries is Kantorovich, so that the induced behavioural distance (on systems of suitably restricted branching degree) can be characterized by a quantitative modal logic.

Authors with CRIS profile

Sergey Goncharov Lehrstuhl für Informatik 8 (Theoretische Informatik) Pedro Nora Lehrstuhl für Informatik 8 (Theoretische Informatik) Lutz Schröder Lehrstuhl für Informatik 8 (Theoretische Informatik) Paul Wild Lehrstuhl für Informatik 8 (Theoretische Informatik)

Involved external institutions

Center for Research & Development in Mathematics and Applications / Centro de Investigação e Desenvolvimento em Matemática e Aplicações (CIDMA) PT Portugal (PT)

How to cite

APA:

Goncharov, S., Hofmann, D., Nora, P., Schröder, L., & Wild, P. (2023). Kantorovich Functors and Characteristic Logics for Behavioural Distances. In Orna Kupferman, Pawel Sobocinski (Eds.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (pp. 46-67). Paris, FRA: Springer Science and Business Media Deutschland GmbH.

MLA:

Goncharov, Sergey, et al. "Kantorovich Functors and Characteristic Logics for Behavioural Distances." Proceedings of the 26th International Conference on Foundations of Software Science and Computational Structures, FOSSACS 2023, held as part of the 26th European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, FRA Ed. Orna Kupferman, Pawel Sobocinski, Springer Science and Business Media Deutschland GmbH, 2023. 46-67.

BibTeX: Download