Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Expressive Quantale-valued Logics for Coalgebras: an Adjunction-based Approach

Harsh Beohar, Sebastian Gurke, Barbara König, Karla Messing, Jonas Forster, Lutz Schröder, Paul Wild

TL;DR

This work develops an adjunction-based framework to derive fixpoint equations for behavioural conformances from modal logics in a coalgebraic setting. It uses Galois connections between predicate and conformance lattices, together with quantale-valued logics, to ensure that the least fixpoint of the logic coincides with the greatest fixpoint of a behaviour function (Hennessy–Milner type theorem). It specializes to coalgebras in Eilenberg–Moore categories for linear-time trace notions, obtaining simple logics and Kantorovich-type liftings that instantiate to bisimilarity, trace equivalence, and trace/pseudometric distances (including for probabilistic automata and directed fuzzy traces). The framework supports compositionality of logics and provides a principled blueprint for deriving fixpoint computations, enabling modular, quantitative analysis of behavioural distances in both branching-time and linear-time settings. Overall, it unifies logic-based specification with category-theoretic fixpoint methods to yield expressive, quantitatively grounded HM-type results for a broad spectrum of coalgebraic systems.

Abstract

We address the task of deriving fixpoint equations from modal logics characterizing behavioural equivalences and metrics (summarized under the term conformances). We rely on earlier work that obtains Hennessy-Milner theorems as corollaries to a fixpoint preservation property along Galois connections between suitable lattices. We instantiate this to the setting of coalgebras, in which we spell out the compatibility property ensuring that we can derive a behaviour function whose greatest fixpoint coincides with the logical conformance. We then concentrate on the linear-time case, for which we study coalgebras based on the machine functor living in Eilenberg-Moore categories, a scenario for which we obtain a particularly simple logic and fixpoint equation. The theory is instantiated to concrete examples, both in the branching-time case (bisimilarity and behavioural metrics) and in the linear-time case (trace equivalences and trace distances).

Expressive Quantale-valued Logics for Coalgebras: an Adjunction-based Approach

TL;DR

This work develops an adjunction-based framework to derive fixpoint equations for behavioural conformances from modal logics in a coalgebraic setting. It uses Galois connections between predicate and conformance lattices, together with quantale-valued logics, to ensure that the least fixpoint of the logic coincides with the greatest fixpoint of a behaviour function (Hennessy–Milner type theorem). It specializes to coalgebras in Eilenberg–Moore categories for linear-time trace notions, obtaining simple logics and Kantorovich-type liftings that instantiate to bisimilarity, trace equivalence, and trace/pseudometric distances (including for probabilistic automata and directed fuzzy traces). The framework supports compositionality of logics and provides a principled blueprint for deriving fixpoint computations, enabling modular, quantitative analysis of behavioural distances in both branching-time and linear-time settings. Overall, it unifies logic-based specification with category-theoretic fixpoint methods to yield expressive, quantitatively grounded HM-type results for a broad spectrum of coalgebraic systems.

Abstract

We address the task of deriving fixpoint equations from modal logics characterizing behavioural equivalences and metrics (summarized under the term conformances). We rely on earlier work that obtains Hennessy-Milner theorems as corollaries to a fixpoint preservation property along Galois connections between suitable lattices. We instantiate this to the setting of coalgebras, in which we spell out the compatibility property ensuring that we can derive a behaviour function whose greatest fixpoint coincides with the logical conformance. We then concentrate on the linear-time case, for which we study coalgebras based on the machine functor living in Eilenberg-Moore categories, a scenario for which we obtain a particularly simple logic and fixpoint equation. The theory is instantiated to concrete examples, both in the branching-time case (bisimilarity and behavioural metrics) and in the linear-time case (trace equivalences and trace distances).
Paper Structure (23 sections, 5 theorems, 13 equations, 2 figures)

This paper contains 23 sections, 5 theorems, 13 equations, 2 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Lattices, Fixpoints and Galois Connections
  4. Quantales and Generalized Distances
  5. Coalgebras and Eilenberg-Moore Categories
  6. Indexed Categories and Fibrations
  7. Adjoint Logic: the General Framework
  8. Adjoint Logic for Coalgebras
  9. Setting up the Adjunction
  10. Characterizing Closure
  11. Towards a Generic Logic Function
  12. Towards a Generic Behaviour Function
  13. Logics for Quantale-valued Simulation Distances
  14. The Adjoint Setup in an Eilenberg-Moore Category
  15. Logic and Behaviour Function for Coalgebras in Eilenberg-Moore
  16. ...and 8 more sections

Key Result

Theorem 4

Let $\alpha\colon \mathbb{L} \to \mathbb{B}$, $\gamma\colon \mathbb{B} \to \mathbb{L}$ be a Galois connection between complete lattices $\mathbb{L}, \mathbb{B}$, and let $\mathop{\mathrm{\mathsf{log}}}\nolimits\colon \mathbb{L}\to\mathbb{L}$, $\mathop{\mathrm{\mathsf{beh}}}\nolimits\colon \mathbb{B}

Figures (2)

  • Figure 1: The adjoint setup with $\mathop{\mathrm{\mathsf{log}}}\nolimits_X= \mathcal{P}(c^\bullet)\circ \Lambda_X \circ \mathop{\mathrm{\mathsf{cl}}}\nolimits'_X \cup\ \Theta_X$ and $\mathop{\mathrm{\mathsf{beh}}}\nolimits_X= c^* \circ \mathop{\mathrm{\kappa}}\nolimits_X \cup\ \alpha_X(\Theta_X)$.
  • Figure 2: The adjoint setup for algebras, where $\mathop{\mathrm{\mathsf{beh}}}\nolimits_{LX}=(c^\#)^*\circ \mathop{\mathrm{\kappa}}\nolimits_{LX} \land \alpha_{LX}(\Theta_{LX})$ and $\mathop{\mathrm{\mathsf{log}}}\nolimits'_X=\mathcal{P}(c^\bullet) \circ \Lambda_X' \cup \Theta_X$.

Theorems & Definitions (16)

  • Definition 1
  • Example 2
  • Definition 3
  • Theorem 4: bgkm:hennessy-milner-galois
  • Remark 5
  • Example 6
  • Proposition 7: bgkm:hennessy-milner-galois
  • Example 8
  • Proposition 9
  • Example 10
  • ...and 6 more