构建行为距离下界的证据

行为距离为概率转移系统中的等价概念（如二分相似性）提供了稳健的替代方案。它们可以定义为最小不动点，其普遍属性允许我们展示状态之间距离的上界，从而表明它们最多相距某些距离。本文我们转而考虑下界问题，展示状态至少相距某些距离。与上界不同，下界可以归纳推理。我们利用这一点，给出一种针对标记马尔可夫链行为距离定义的下界归纳推理系统。该系统灵感来自最近关于二分性（apartness）作为二分相似性归纳对应物的工作。我们系统中的证明将在 soundness 与（近似）completeness 结果下与行为距离 closely match。我们进一步提供了我们归纳推理系统与带量化语义的模态逻辑公式之间的构造性对应关系。这种逻辑曾用于 Rady 和 van Breugel 的最近工作中，以构建行为距离下界的证据。我们的构造在许多示例中提供了更小的 witnessing 公式。