一种基于抽象解释的高效模拟算法

目前已有一些计算模拟预序的算法。设 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 的算法相比，具有良好的对比结果。