基于抽象解释的高效模拟算法
摘要：计算模拟优先关系的算法较多。设Sigma为状态空间，->为转移关系，Psim为模拟等价引发的Sigma的划分。Henzinger, Henzinger, Kopke和Bloom和Paige的算法的时间复杂度为O(|Sigma||->|)，从时间复杂性的角度来看，它们是目前可用的最佳算法。然而，这些算法的缺点是空间复杂度超过状态空间大小的平方。由Gentilini, Piazza, Policriti提出的算法（随后被van Glabbeek和Ploeger修正）似乎在时间和空间复杂度之间提供了最佳的平衡。Gentilini等人的算法的时间复杂度为O(|Psim|^2|->|)，而空间复杂度为O(|Psim|^2 + |Sigma|log|Psim|)。我们在这里提出了一种新的高效模拟算法，它是通过修改Henzinger等人的算法得到的，其正确性基于抽象解释在模型检测中的一些技术。我们的算法的时间复杂度为O(|Psim||->|)，空间复杂度为O(|Psim||Sigma|log|Sigma|)。因此，该算法改进了已知的最佳时间复杂度，同时保持了一个可接受的空间复杂度，一般情况下不超过状态空间大小的平方。实验评估显示，相对于Henzinger, Henzinger和Kopke的算法，我们的算法效果良好。
作者：Francesco Ranzato and Francesco Tapparo
论文ID：0709.4118
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2008-12-05