Computing Distinguishing Formulae for Threshold-Based Behavioural Distances
Jonas Forster, Lutz Schröder, Paul Wild, Barbara König, Pedro Nora
TL;DR
The paper develops a coalgebraic framework for threshold-based behavioural distances using $2$-to-$\mathcal{V}$ predicate liftings, unifying $\varepsilon$-bisimulation with distribution- and metric-based distances via modal liftings. It proves that the threshold distance $d_{\Lambda}$ coincides with a Kantorovich-type lax extension $\mathbf{L}_{\Lambda}$ and is captured by a Sugeno-based quantitative logic $\mathcal{L}(\mathsf S[\Lambda])$, with $\mathsf S[\Lambda]$ providing the semantic bridge. For finitely branching systems, both a two-valued logic up to $\varepsilon$ and the quantitative Sugeno logic are expressive and admit polynomial-time extraction of distinguishing formulae from Spoiler strategies, yielding witnesses of $d_{\Lambda}(x,y)>\varepsilon$. These results generalize and connect prior work on Lévy-Prokhorov, Kantorovich, and related distances, and yield new polynomial-time explainability results for threshold-based behavioural distances across probabilistic, fuzzy, and metric transition systems.
Abstract
Behavioural distances generally offer more fine-grained means of comparing quantitative systems than two-valued behavioural equivalences. They often relate to quantitative modalities, which generate quantitative modal logics that characterize a given behavioural distance in terms of the induced logical distance. We develop a unified framework for behavioural distances and logics induced by a special type of modalities that lift two-valued predicates to quantitative predicates. A typical example is the probability operator, which maps a two-valued predicate $A$ to a quantitative predicate on probability distributions assigning to each distribution the respective probability of $A$. Correspondingly, the prototypical example of our framework is $ε$-bisimulation distance of Markov chains, which has recently been shown to coincide with the behavioural distance induced by the popular Lévy-Prokhorov distance on distributions. Other examples include behavioural distance on metric transition systems and Hausdorff behavioural distance on fuzzy transition systems. Our main generic results concern the polynomial-time extraction of distinguishing formulae in two characteristic modal logics: A two-valued logic with a notion of satisfaction up to $ε$, and a quantitative modal logic. These results instantiate to new results in many of the mentioned examples. Notably, we obtain polynomial-time extraction of distinguishing formulae for $ε$-bisimulation distance of Markov chains in a quantitative logic featuring a `generally' modality used in probabilistic knowledge representation.