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

TL;DR

This paper develops a framework for deriving fixpoint equations from modal logics that characterize behavioral equivalences and metrics in coalgebraic systems, using an adjunction-based approach.

Contribution

It introduces an adjunction-based method to derive fixpoint equations for coalgebraic modal logics, extending to both branching and linear-time systems.

Findings

Derived fixpoint equations for behavioral equivalences and metrics

Applied the framework to both branching-time and linear-time coalgebras

Simplified logic and fixpoint equations in the Eilenberg-Moore category setting

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).