Hennessy-Milner Theorems via Galois Connections

TL;DR

This paper presents a unified Galois connection framework for deriving soundness and expressiveness results in modal logics that characterize behavioral equivalences and metrics, covering both qualitative and quantitative cases.

Contribution

It introduces a general, compositional approach using Galois connections to derive Hennessy-Milner theorems for a broad spectrum of behavioral equivalences and metrics.

Findings

Derived a new fixpoint characterization of directed trace metrics

Established conditions for logical equivalences to be induced by fixpoint equations

Unified treatment of qualitative and quantitative behavioral semantics

Abstract

We introduce a general and compositional, yet simple, framework that allows us to derive soundness and expressiveness results for modal logics characterizing behavioural equivalences or metrics (also known as Hennessy-Milner theorems). It is based on Galois connections between sets of (real-valued) predicates on the one hand and equivalence relations/metrics on the other hand and covers a part of the linear-time-branching-time spectrum, both for the qualitative case (behavioural equivalences) and the quantitative case (behavioural metrics). We derive behaviour functions from a given logic and give a condition, called compatibility, that characterizes under which conditions a logically induced equivalence/metric is induced by a fixpoint equation. In particular this framework allows us to derive a new fixpoint characterization of directed trace metrics.