双相似距离的动态计算
On-the-Fly Computation of Bisimilarity Distances
摘要：
我们提出了一个连续时间马尔可夫链（CTMCs）之间的距离，并通过比较三种不同的算法方法：迭代，线性规划，和飞行研究计算它的问题。在FoSSaCS'12上发表的一项工作中，Chen等人将Desharnais等人的离散时间马尔可夫链之间的双相似距离表征为可以使用椭球方法求解的线性规划的最优解。受他们的结果的启发，我们提出了一种新的线性规划表征计算的距离在连续时间设置。与以前的建议不同，我们的建议有许多约束条件，这些约束条件由CTMC大小的多项式限定。特别是，这证明了我们提出的距离可以在多项式时间内计算。尽管其理论上的重要性，所提出的线性规划的表征原来是在实践中效率低下。然而，在我们之前在TACAS'13上提出的令人鼓舞的工作结果的驱动下，我们提出了一种高效的动态算法，与其他提到的解决方案不同，该算法计算两个给定状态之间的距离，避免了对状态空间的详尽探索。该技术通过使用贪婪策略连续地细化目标距离的过近似来工作，这确保了仅当当前近似被改进时才进一步探索状态空间。一组一致的（伪）随机生成的CTMCs上进行的测试表明，我们的算法提高了，平均而言，相应的迭代和线性规划方法的效率与数量级。
英文摘要：
We propose a distance between continuous-time Markov chains (CTMCs) and study the problem of computing it by comparing three different algorithmic methodologies: iterative, linear program, and on-the-fly. In a work presented at FoSSaCS'12, Chen et al. characterized the bisimilarity distance of Desharnais et al. between discrete-time Markov chains as an optimal solution of a linear program that can be solved by using the ellipsoid method. Inspired by their result, we propose a novel linear program characterization to compute the distance in the continuous-time setting. Differently from previous proposals, ours has a number of constraints that is bounded by a polynomial in the size of the CTMC. This, in particular, proves that the distance we propose can be computed in polynomial time. Despite its theoretical importance, the proposed linear program characterization turns out to be inefficient in practice. Nevertheless, driven by the encouraging results of our previous work presented at TACAS'13, we propose an efficient on-the-fly algorithm, which, unlike the other mentioned solutions, computes the distances between two given states avoiding an exhaustive exploration of the state space. This technique works by successively refining over-approximations of the target distances using a greedy strategy, which ensures that the state space is further explored only when the current approximations are improved. Tests performed on a consistent set of (pseudo)randomly generated CTMCs show that our algorithm improves, on average, the efficiency of the corresponding iterative and linear program methods with orders of magnitude.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
