Behavioural Conformances based on Lax Couplings
Paul Wild, Lutz Schröder
TL;DR
We address the problem of defining behavioural conformances for diverse state-based systems in a uniform coalgebraic framework by introducing lax couplings that bypass non-existent exact couplings. The core method, the distributorial Wasserstein extension, builds on $ ext{V}$-valued predicate liftings and $ ext{V}$-distributors to yield $ ext{L}$-simulations and distances across a range of functors, including metric streams and metric-labelled Markov chains. Key contributions include a general theory of distributorial lax extensions, exact-square preservation conditions, and a suite of running examples (simulations, modal transition systems, MLMC) that demonstrate unbalanced transport distances and enhanced conformance notions. The work further explores dualities between Kantorovich and Wasserstein constructions, supported by a representation theorem, and points to future directions in unbalanced transport and broader metric structures within the coalgebraic paradigm.
Abstract
Behavioural conformances -- e.g. behavioural equivalences, distances, preorders -- on a wide range of system types (non-deterministic, probabilistic, weighted etc.) can be dealt with uniformly in the paradigm of universal coalgebra. One of the most commonly used constructions for defining behavioural distances on coalgebras arises as a generalization of the well-known Wasserstein metric. In this construction, couplings of probability distributions are replaced with couplings of more general objects, depending on the functor describing the system type. In many cases, however, the set of couplings of two functor elements is empty, which causes such elements to have infinite distance even in situations where this is not desirable. We propose an approach to defining behavioural distances and preorders based on a more liberal notion of coupling where the coupled elements are matched laxly rather than on-the-nose. We thereby substantially broaden the range of behavioural conformances expressible in terms of couplings, covering, e.g., refinement of modal transition systems and behavioural distance on metric labelled Markov chains.