arXiv:2511.18103cs.LOcs.CL2025-11

提出一种新方法比较概率模型,能精确衡量系统差异并保证计算可行性。

Comparing Labeled Markov Chains: A Cantor-Kantorovich Approach

  • 基于康托尔-坎托罗维奇距离,将模型对比转化为多阶段总变差之和。
  • 证明精确计算该距离是#P难问题,且距离越小则有限轨迹概率误差越低。
  • 给出可计算的近似算法,适合形式化验证与模型抽象评估场景。

标记马尔可夫链(LMC)是建模复杂概率语言的重要工具。本文研究近期提出的康托尔-坎托罗维奇(CK)距离,发现其可表述为折扣后有限时域总变差距离的加权和,属于自然康托尔拓扑下的折扣线性距离。我们从计算复杂度、连续性及逼近性三个维度分析该距离:证明其精确计算为#P难;给出CK距离上界与两LMC间近似关系的函数关系;并表明有界CK距离意味着有限时域轨迹概率误差有界。最后,我们提出一个可计算的近似方案,其本身也属于#P难。整体结果为CK距离提供了坚实的理论基础,并厘清了其与已有距离度量的关系。

原文摘要 · Abstract (English)

Labeled Markov Chains (or LMCs for short) are useful mathematical objects to model complex probabilistic languages. A central challenge is to compare two LMCs, for example to assess the accuracy of an abstraction or to quantify the effect of model perturbations. In this work, we study the recently introduced Cantor-Kantorovich (or CK) distance. In particular we show that the latter can be framed as a discounted sum of finite-horizon Total Variation distances, making it an instance of discounted linear distance, but arising from the natural Cantor topology. Building on the latter observation, we analyze the properties of the CK distance along three dimensions: computational complexity, continuity properties and approximation. More precisely, we show that the exact computation of the CK distance is #P-hard. We also provide an upper bound on the CK distance as a function of the approximation relation between the two LMCs, and show that a bounded CK distance implies a bounded error between probabilities of finite-horizon traces. Finally, we provide a computable approximation scheme, and show that the latter is also #P-hard. Altogether, our results provide a rigorous theoretical foundation for the CK distance and clarify its relationship with existing distances.

概率模型距离度量形式验证

Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。