Kantorovich functors and characteristic logics for behavioural distances

DOI10.1007/978-3-031-30829-1_3MaRDI QIDQ6091180zbMATH OpenFDO

Authors S. S. Goncharov, Dirk Hofmann, Pedro Nora, Lutz Schröder, Paul Wild

Publication date 24 November 2023

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/2202.07069

Mathematics Subject Classification ID

Theory of software (68Nxx) Theory of computing (68Qxx)

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.

Cites work

• (Metric) bisimulation games and real-valued modal logics for coalgebras
• A behavioural pseudometric for probabilistic transition systems
• A quantified coalgebraic van Benthem theorem
• Abstract and concrete categories: the joy of cats
• An introduction to quantaloid-enriched categories
• Associative functions. Triangular norms and copulas
• Bisimulation for labelled Markov processes
• Bisimulation through probabilistic testing
• Coalgebraic behavioral metrics
• Computer Science Logic
• Exponentiable functors between quantaloid-enriched categories
• Exponentiation in \({\mathcal V}\)-categories
• Expressive logics for coalgebras via terminal sequence induction
• Expressivity of coalgebraic modal logic: the limits and beyond
• Fibrational bisimulations and quantitative reasoning: extended version
• Hausdorff coalgebras
• scientific article; zbMATH DE number 5761737 (Why is no real title available?)
• scientific article; zbMATH DE number 19040 (Why is no real title available?)
• scientific article; zbMATH DE number 1231637 (Why is no real title available?)
• scientific article; zbMATH DE number 1796614 (Why is no real title available?)
• scientific article; zbMATH DE number 2172008 (Why is no real title available?)
• scientific article; zbMATH DE number 7559483 (Why is no real title available?)
• Lax extensions of coalgebra functors and their logic
• Metrics for weighted transition systems: axiomatization and complexity
• Neighbourhood Structures: Bisimilarity and Basic Model Theory
• On Choosing and Bounding Probability Metrics
• Ordered topological structures
• Quantaloids, enriched categories and automata theory
• Quantitative Behavioural Reasoning for Higher-order Effectful Programs
• Universal coalgebra: A theory of systems

Cited in

(9)

• scientific article; zbMATH DE number 7559483 (Why is no real title available?)
• Proving behavioural apartness
• A complete quantitative axiomatisation of behavioural distance of regular expressions
• Relational connectors and heterogeneous simulations
• Composing codensity bisimulations
• Correspondences between codensity and coupling-based liftings, a practical approach
• Quantitative graded semantics and spectra of behavioural metrics
• Compact quantitative theories of convex algebras
• Generalized Kantorovich-Rubinstein duality beyond Hausdorff and Kantorovich

This page was built for publication: Kantorovich functors and characteristic logics for behavioural distances

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6091180)