互模拟距离的即时计算
计算机科学中的逻辑
2019-03-14 v2
摘要
我们提出了一种连续时间马尔可夫链（CTMC）之间的距离，并通过比较三种不同的算法方法论来研究其计算问题：迭代法、线性规划法和即时法。在FoSSaCS'12上发表的一项工作中，Chen等人将Desharnais等人提出的离散时间马尔可夫链间的互模拟距离刻画为一个线性规划的最优解，该线性规划可用椭球法求解。受其结果启发，我们提出了一种新颖的线性规划刻画来计算连续时间设定下的距离。与以往方案不同，我们的方案具有数量受CTMC规模的多项式界定的约束条件。这特别证明了我们提出的距离可在多项式时间内计算。尽管具有理论重要性，所提出的线性规划刻画在实践中却效率低下。然而，受我们之前在TACAS'13上发表的令人鼓舞的结果驱动，我们提出了一种高效的即时算法，该算法不同于上述其他解决方案，它计算两个给定状态间的距离时避免了状态空间的穷举探索。该技术通过使用贪婪策略逐步细化目标距离的过近似来工作，确保仅当当前近似值得到改进时才进一步探索状态空间。在一组一致的（伪）随机生成的CTMC上进行的测试表明，我们的算法平均将相应的迭代法和线性规划法的效率提高了数个数量级。
引用
@article{arxiv.1702.08306,
title = {On-the-Fly Computation of Bisimilarity Distances},
author = {Giorgio Bacci and Giovanni Bacci and Kim G. Larsen and Radu Mardare},
journal= {arXiv preprint arXiv:1702.08306},
year = {2019}
}