$\epsilon$-Distance via L\'evy-Prokhorov Lifting

TL;DR

This paper introduces an $oldsymbol{ ext{ extit{ extepsilon}}}$-distance based on the Lévy-Prokhorov metric, providing a new, intuitive, and computationally accessible behavioral pseudometric for probabilistic processes with coalgebraic characterization.

Contribution

It demonstrates that $ ext{ extepsilon}$-distance is the greatest fixpoint of a functional using Lévy-Prokhorov distance, extending the coalgebraic framework for probabilistic process metrics.

Findings

$ ext{ extepsilon}$-distance is a fixpoint of a functional with a functor based on Lévy-Prokhorov distance.

Provides a coalgebraic characterization of $ ext{ extepsilon}$-couplings and $ ext{ extepsilon}$-bisimulations.

$ ext{ extepsilon}$-distance is easy to understand and compute, suitable for systems with approximate behaviors.

Abstract

The most studied and accepted pseudometric for probabilistic processes is one based on the Kantorovich distance between distributions. It comes with many theoretical and motivating results, in particular it is the fixpoint of a given functional and defines a functor on (complete) pseudometric spaces. Other notions of behavioural pseudometrics have also been proposed, one of them ($\epsilon$-distance) based on $\epsilon$-bisimulation. $\epsilon$-Distance has the advantages that it is intuitively easy to understand, it relates systems that are conceptually close (for example, an imperfect implementation is close to its specification), and it comes equipped with a natural notion of $\epsilon$-coupling. Finally, this distance is easy to compute. We show that $\epsilon$-distance is also the greatest fixpoint of a functional and provides a functor. The latter is obtained by replacing the Kantorovich distance in the lifting functor with the L\'evy-Prokhorov distance. In addition, we show that $\epsilon$-couplings and $\epsilon$-bisimulations have an appealing coalgebraic characterization.