Coalgebraic Behavioral Metrics

TL;DR

This paper develops a coalgebraic framework for defining behavioral pseudometrics that measure the distance between states in systems, unifying branching and linear-time semantics through functor liftings and generalizations of Kantorovich and Wasserstein metrics.

Contribution

It introduces a novel coalgebraic approach to derive behavioral metrics, including conditions for lifting functors and monads to pseudometric spaces, unifying different semantics.

Findings

Two approaches generalize Kantorovich and Wasserstein metrics.

The two pseudometrics coincide in natural examples but differ generally.

Conditions are provided for lifting distributive laws and monads, enabling the generalized powerset construction.

Abstract

We study different behavioral metrics, such as those arising from both branching and linear-time semantics, in a coalgebraic setting. Given a coalgebra $\alpha\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.