关于概率双模拟距离的连续性

概率双模拟距离为标记马尔可夫链提供了行为差异的定量度量，但它在转移概率的扰动下可能是不连续的。这种缺乏连续性的情况削弱了其对经验推导模型的适用性，在这些模型中，转移概率通常是近似值。最近，我们（CAV 2025）引入了鲁棒概率双模拟作为距离为零时连续性的充分条件。在本文中，我们证明它也是一个必要条件，即两个状态是鲁棒概率双模拟的，当且仅当对于任何足够小的转移概率扰动，它们的概率双模拟距离都很小。我们进一步将鲁棒性扩展到非双模拟状态对，以建立概率双模拟距离连续性的完整表征。基于这种表征，我们开发了一种多项式时间算法来决定连续性。最后，我们用实验评估补充了我们的理论贡献，展示了所提出方法在实践中的应用。我们的结果表明，与计算概率双模拟距离相比，决定连续性的额外步骤需要最小的额外成本。