一句话：将概率互模拟距离刻画为随机博弈解，并给出首个实用的策略迭代计算算法。
本文研究概率自动机上 Deng 等人提出的概率互模拟距离，它是 Segala–Lynch 概率互模拟的定量推广。作者利用 Mémoli 对 Hausdorff 距离的对偶表示，将该距离刻画为一个简单随机博弈的解，进而用 Condon 的简单策略迭代算法计算距离。由于原算法要求博弈 stopping，而所得博弈一般非 stopping，作者证明该扩展类仍可终止。此前算法复杂度属于 UP∩coUP 和 PPAD，但实践低效；本文算法据称是首个实用方案。此外，论文还证明该距离可界定两个状态满足任意 ω-正则性质（如 LTL 公式）的最大/最小概率之差。
The probabilistic bisimilarity distance of Deng et al. has been proposed as a robust quantitative generalization of Segala and Lynch's probabilistic bisimilarity for probabilistic automata. In this paper, we present a characterization of the bisimilarity distance as the solution of a simple stochastic game. The characterization gives us an algorithm to compute the distances by applying Condon's simple policy iteration on these games. The correctness of Condon's approach, however, relies on the assumption that the games are stopping. Our games may be non-stopping in general, yet we are able to prove termination for this extended class of games. Already other algorithms have been proposed in the literature to compute these distances, with complexity in $\textbf{UP} \cap \textbf{coUP}$ and \textbf{PPAD}. Despite the theoretical relevance, these algorithms are inefficient in practice. To the best of our knowledge, our algorithm is the first practical solution. The characterization of the probabilistic bisimilarity distance mentioned above crucially uses a dual presentation of the Hausdorff distance due to M\'emoli. As an additional contribution, in this paper we show that M\'emoli's result can be used also to prove that the bisimilarity distance bounds the difference in the maximal (or minimal) probability of two states to satisfying arbitrary $\omega$-regular properties, expressed, eg., as LTL formulas.
@article{paperbot1342,
title = {Computing Probabilistic Bisimilarity Distances for Probabilistic Automata},
author = {Giorgio Bacci and Giovanni Bacci and Kim G. Larsen and Radu Mardare and Qiyi Tang and Franck van Breugel},
journal = {Logical Methods in Computer Science},
volume = {Volume 17, Issue 1},
year = {2021},
doi = {10.23638/lmcs-17(1:9)2021}
}