Kantorovich Functors and Characteristic Logics for Behavioural Distances

TL;DR

This paper explores the theoretical foundations of behavioural distances in quantitative systems, demonstrating that functor liftings preserving isometries are Kantorovich and can be characterized by quantitative modal logics.

Contribution

It generalizes the connection between lax extensions and Kantorovich functors to all functor liftings that preserve isometries, broadening the scope of coalgebraic behavioural distances.

Findings

Every functor lifting that preserves isometries is Kantorovich.

Behavioural distances can be characterized by quantitative modal logics.

The results unify and extend previous coalgebraic approaches.

Abstract

Behavioural distances measure the deviation between states in quantitative systems, such as probabilistic or weighted systems. There is growing interest in generic approaches to behavioural distances. In particular, coalgebraic methods capture variations in the system type (nondeterministic, probabilistic, game-based etc.), and the notion of quantale abstracts over the actual values distances take, thus covering, e.g., two-valued equivalences, (pseudo-)metrics, and probabilistic (pseudo-)metrics. Coalgebraic behavioural distances have been based either on liftings of SET-functors to categories of metric spaces, or on lax extensions of SET-functors to categories of quantitative relations. Every lax extension induces a functor lifting but not every lifting comes from a lax extension. It was shown recently that every lax extension is Kantorovich, i.e. induced by a suitable choice of monotone predicate liftings, implying via a quantitative coalgebraic Hennessy-Milner theorem that behavioural distances induced by lax extensions can be characterized by quantitative modal logics. Here, we essentially show the same in the more general setting of behavioural distances induced by functor liftings. In particular, we show that every functor lifting, and indeed every functor on (quantale-valued) metric spaces, that preserves isometries is Kantorovich, so that the induced behavioural distance (on systems of suitably restricted branching degree) can be characterized by a quantitative modal logic.