证明余归纳全局互模拟距离的连续性：一个未竟的故事

我们提出了一种进程间全局互模拟距离的概念，它在某种程度上超越了文献中已有的主要基于互模拟博弈的互模拟距离概念。我们的提议基于变换的代价：我们需要修改被比较的其中一个进程多少才能获得另一个进程。我们最初的定义仅涵盖有限进程，但余归纳方法允许我们将其扩展以涵盖无限但有穷树。在展示了我们距离的许多有趣性质之后，我们意图证明关于投影的连续性，但不幸的是该问题仍然开放。尽管如此，我们获得了若干部分结果，本文给出了这些结果。