Computing Distinguishing Formulae for Threshold-Based Behavioural Distances

这篇论文提出了一种统一的**基于阈值的行为距离（Threshold-Based Behavioural Distances）**的代数框架，旨在为定量系统（如概率系统、模糊系统、度量转换系统等）提供细粒度的行为比较方法。文章的核心在于建立行为距离与逻辑特征之间的紧密联系，并提出了在多项式时间内提取区分公式（Distinguishing Formulae）的高效算法。

以下是对该论文的详细技术总结：

1. 研究问题 (Problem)

• 背景：在带有定量信息的系统中，传统的二值行为等价性（如双模拟）往往过于粗糙，无法捕捉系统行为的细微差异。行为距离（Behavioural Distances）提供了更稳定的比较手段。
• 挑战：
  • 现有的行为距离定义多种多样（如概率系统中的 $\varepsilon$-双模拟距离、度量转换系统中的距离、模糊系统中的 Hausdorff 距离等），缺乏统一的理论框架。
  • 虽然已知某些距离（如 Markov 链上的 Lévy-Prokhorov 距离）具有逻辑特征，但缺乏通用的逻辑刻画方法。
  • 关键难点：如何高效地计算区分公式？即，给定两个状态，如果它们的行为距离大于某个阈值 $\varepsilon$，如何构造一个逻辑公式来“证伪”它们的相似性？现有的算法往往在公式大小（树大小）上呈指数级，或者缺乏多项式时间的提取算法。

2. 方法论 (Methodology)

作者基于**通用代数（Universal Coalgebra）**框架，引入了一类特殊的模态算子，构建了统一的理论体系：

• 2-to-V 谓词提升（2-to-V Predicate Liftings）：
  • 这是框架的核心。作者选择了一组将二值谓词（$2^X$）提升为区间 $[0,1]$ 上定量谓词（$V^X$）的模态算子。
  • 典型例子：概率算子 $P$，将集合 $A$ 映射为概率分布 $\mu$ 在 $A$ 上的概率值 $\mu(A)$。
• 基于 $\varepsilon$-(bi-)模拟的定义：
  • 定义了一种允许偏差为 $\varepsilon$ 的模拟关系（$\varepsilon$-simulation）。如果状态 $x$ 和 $y$ 在允许偏差 $\varepsilon$ 下满足所有模态算子的约束，则称它们为 $\varepsilon$-模拟。
  • 行为距离 $d_\Lambda(x, y)$ 定义为使得 $x$ 和 $y$ 成为 $\varepsilon$-模拟的最小 $\varepsilon$ 值（下确界）。
• 松弛扩展（Lax Extensions）与 Kantorovich 构造：
  • 作者证明了这种基于 $\varepsilon$-模拟的距离等价于由特定**定量松弛扩展（Quantitative Lax Extension）**诱导的距离。
  • 通过Sugeno 积分，将 2-to-V 的模态算子转化为 V-to-V 的 Sugeno 模态算子（Sugeno Modalities）。
  • 证明了由 Sugeno 模态算子诱导的 Kantorovich 松弛扩展与上述基于阈值的松弛扩展是等价的。
• 博弈策略与公式提取：
  • 引入了Codensity 博弈（Codensity Game），其中 Spoiler（破坏者）试图证明两个状态不相似，而 Duplicator（复制者）试图证明它们相似。
  • 利用 Spoiler 的获胜策略，通过动态规划算法，从博弈路径中提取区分公式。

3. 主要贡献 (Key Contributions)

1. 统一的理论框架：

   • 提出了一个通用的代数框架，涵盖了多种已知行为距离，包括：
     • Markov 链上的 $\varepsilon$-距离（即 Lévy-Prokhorov 距离）。
     • 度量转换系统（Metric Transition Systems）上的行为距离。
     • 模糊转换系统（Fuzzy Transition Systems）上的 Hausdorff 距离。
   • 证明了这些距离在代数上等价于由特定 2-to-V 模态算子诱导的阈值松弛扩展。

2. 逻辑特征化（Logical Characterization）：

   • 二值逻辑：定义了一种带有“满足度 $\varepsilon$"概念的二值模态逻辑。证明了在有限分支系统中，该逻辑的行为距离与阈值行为距离一致（Hennessy-Milner 定理的定量版本）。
   • 定量逻辑：构建了基于 Sugeno 模态算子的非扩张（Non-expansive）定量模态逻辑。证明了该逻辑的特征距离（Logical Distance）精确等于阈值行为距离。
   • 具体实例：在概率情况下，Sugeno 模态算子对应于概率知识表示中常用的 "Generally"（一般地） 模态算子，从而证明了 "Generally" 模态算子诱导 Lévy-Prokhorov 距离。

3. 多项式时间区分公式提取算法：

   • 提出了两个算法（Algorithm 1 和 Algorithm 2），分别从 Spoiler 的获胜策略中提取二值和定量的区分公式。
   • 复杂度突破：
     • 提取的公式具有多项式有向无环图（DAG）大小（尽管树大小在最坏情况下可能是指数级的，但 DAG 大小是多项式的）。
     • 在模态算子满足“多项式时间可解”的假设下（如概率、模糊、度量系统），整个提取过程可在多项式时间内完成。
   • 这是首次为 Lévy-Prokhorov 距离（Markov 链）提供多项式时间的区分公式提取算法。

4. 主要结果 (Results)

• 等价性定理：
  • 基于 $\varepsilon$-模拟的行为距离 $d_\Lambda$ 等于由阈值松弛扩展 $L_\Lambda$ 诱导的距离。
  • $L_\Lambda$ 等于由 Sugeno 模态算子诱导的 Kantorovich 松弛扩展 $K_{S[\Lambda]}$。
• 表达性定理（Expressiveness）：
  • 对于有限分支系统，逻辑距离等于行为距离。即，如果 $d_\Lambda(x, y) > \varepsilon$，则存在一个区分公式 $\varphi$，使得 $x$ 满足 $\varphi$ 而 $y$ 不满足（或在定量逻辑中，$y$ 的满足度显著低于 $x$）。
• 算法复杂度：
  • 区分公式的模态秩（Modal Rank）为二次方（$O(k^2)$，其中 $k$ 是状态对数量）。
  • 公式的 DAG 大小为四次方（$O(k^4)$）。
  • 在多项式时间可解的模态算子下，计算区分公式的时间复杂度为多项式级。

5. 意义与影响 (Significance)

• 理论统一：该工作将分散在不同系统类型（概率、模糊、度量）中的行为距离理论统一在一个基于通用代数和 Sugeno 积分的框架下，揭示了它们背后的共同结构。
• 算法突破：
  • 解决了长期存在的难题：为 Lévy-Prokhorov 距离（在机器学习和隐私保护中非常重要）提供了高效的区分公式提取算法。
  • 克服了传统方法中公式大小呈指数级爆炸的问题，通过 DAG 表示和动态规划实现了多项式时间复杂度。
• 实际应用：
  • 形式化验证：为定量系统的验证提供了可计算的逻辑工具，能够精确量化系统行为的差异。
  • 机器学习与隐私：Lévy-Prokhorov 距离在分布比较、共形预测（Conformal Prediction）和差分隐私中应用广泛。该论文提供的逻辑特征和高效算法有助于在这些领域进行更精细的分析和验证。
  • 知识表示：确认了 "Generally" 模态算子在概率知识表示中的理论地位，将其与行为距离直接联系起来。

总结：
这篇论文通过引入基于阈值的代数框架和 Sugeno 模态算子，不仅统一了多种行为距离的定义，还给出了构造区分公式的高效多项式时间算法。这不仅丰富了通用代数的理论体系，也为定量系统的形式化验证和机器学习中的分布比较提供了强有力的计算工具。特别是针对 Markov 链的 Lévy-Prokhorov 距离的多项式时间算法，是该领域的一个重要进展。