Coalgebraic Behavioral Metrics

TL;DR

The paper develops a unified, coalgebraic approach to behavioral metrics by lifting endofunctors $H$ from sets to pseudometric spaces via $\overline{H}$, enabling the construction of distances on $HX$ from a base distance on $X$. It introduces two transport-inspired liftings, Wasserstein and Kantorovich, analyzes their (non)coincidence, and shows that with a final coalgebra these liftings yield a branching-time metric that respects bisimilarity; linear-time (trace) metrics are obtained by lifting distributive laws and monads to enable generalized powerset constructions. The authors establish a fixed-point framework for behavioral distance, prove metric properties of the distance on final coalgebras, and demonstrate how to compute distances via iterative methods. They develop the category $\mathrm{PMet}$, prove its bicompleteness, and provide concrete examples including probabilistic systems, deterministic automata, and metric transition systems, illustrating how trace and bisimulation metrics arise as special cases. Overall, the work provides a principled, reusable toolkit for deriving and analyzing quantitative behavioral equivalences in a wide range of state-based models.

Abstract

We study different behavioral metrics, such as those arising from both branching and linear-time semantics, in a coalgebraic setting. Given a coalgebra $α\colon X \to HX$ for a functor $H \colon \mathrm{Set}\to \mathrm{Set}$, we define a framework for deriving pseudometrics on $X$ which measure the behavioral distance of states. A crucial step is the lifting of the functor $H$ on $\mathrm{Set}$ to a functor $\overline{H}$ on the category $\mathrm{PMet}$ of pseudometric spaces. We present two different approaches which can be viewed as generalizations of the Kantorovich and Wasserstein pseudometrics for probability measures. We show that the pseudometrics provided by the two approaches coincide on several natural examples, but in general they differ. If $H$ has a final coalgebra, every lifting $\overline{H}$ yields in a canonical way a behavioral distance which is usually branching-time, i.e., it generalizes bisimilarity. In order to model linear-time metrics (generalizing trace equivalences), we show sufficient conditions for lifting distributive laws and monads. These results enable us to employ the generalized powerset construction.

Figures (3)

• Figure 1: A pts
• Figure 2: A metric transition system
• Figure 3: Lifting example

Theorems & Definitions (17)

• Definition 2: Pseudometric, Pseudometric Space
• Lemma 1: Lattice of Pseudometrics
• proof
• Lemma 2
• Lemma 3
• Definition 3: Nonexpansive Function, Isometry
• Lemma 4: Composition of Nonexpansive Functions
• proof
• Definition 4: Category of Pseudometric Spaces
• Theorem 4.1