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.

翻译：行为距离通常比二值行为等价提供更精细的量化系统比较手段。它们常与量化模态相关联，这些模态生成量化模态逻辑，通过诱导的逻辑距离来刻画给定的行为距离。我们针对由一类特殊模态所诱导的行为距离与逻辑建立了一个统一框架，这类模态将二值谓词提升为量化谓词。典型示例是概率算子，它将二值谓词$A$映射为概率分布上的量化谓词，该谓词为每个分布分配$A$的相应概率。相应地，我们框架的原型示例是马尔可夫链的$ε$-双模拟距离，该距离最近被证明与流行的分布Lévy-Prokhorov距离所诱导的行为距离相一致。其他示例包括度量转移系统上的行为距离与模糊转移系统上的Hausdorff行为距离。我们的主要通用结果涉及在两种特征模态逻辑中多项式时间提取区分公式：一种具有"满足度不超过$ε$"概念的二值逻辑，以及一种量化模态逻辑。这些结果可实例化为前述众多示例中的新结论。值得注意的是，我们获得了在量化逻辑中为马尔可夫链$ε$-双模拟距离多项式时间提取区分公式的方法，该量化逻辑采用了概率知识表示中使用的"通常"模态。