Computing Distinguishing Formulae for Threshold-Based Behavioural Distances

TL;DR

This paper introduces a unified framework for behavioral distances in quantitative systems, enabling polynomial-time extraction of distinguishing formulae in modal logics, with applications to probabilistic and fuzzy transition systems.

Contribution

It develops a generic approach for deriving distinguishing formulae for behavioral distances using modal logics, applicable to various types of quantitative systems.

Findings

Polynomial-time extraction of distinguishing formulae for epsilon-bisimulation distance.

Application of the framework to Markov chains, metric transition systems, and fuzzy systems.

New results in probabilistic knowledge representation using a modal logic with a 'generally' modality.

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 $\epsilon$-bisimulation distance of Markov chains, which has recently been shown to coincide with the behavioural distance induced by the popular L\'evy-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 $\epsilon$, 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 $\epsilon$-bisimulation distance of Markov chains in a quantitative logic featuring a `generally' modality used in probabilistic knowledge representation.