Goncharov S, Hofmann D, Nora P, Schröder L, Wild P (2023)
Publication Type: Conference contribution
Publication year: 2023
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
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.
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