对数时间内的增量死状态检测

在抽象转换系统中识别活状态和死状态是形式验证中一个反复出现的问题；例如，在我们近期关于高效判定SMT中正则表达式约束的工作中就出现了该问题。然而，用于增量维护可达性信息（即在状态被访问时、整个状态空间被探索之前）的最先进图算法假设，可以在任何时候从任何状态添加新边，而在许多应用中，出边是在每个状态被探索时从该状态添加的。为了形式化后一种情况，我们提出了引导式增量有向图（GID），即支持标记闭合状态（不会接收进一步出边的状态）的增量图。我们的主要结果是，对于$m$条边，GID中的死状态检测可在每条边$O(\log m)$的摊销时间内解决，这优于Bender、Fineman、Gilbert和Tarjan（BFGT）针对一般增量有向图提出的每条边$O(\sqrt{m})$的复杂度。我们为GID引入了两种算法：一种确立了该对数时间界，另一种则探索了一种基于惰性启发式的方法。为了实现同类实验比较，我们使用Rust语言中的通用有向图接口，实现了这两种算法、两个更简单的基线以及最先进的BFGT基线。我们的评估显示，在一系列图类、随机图以及源自正则表达式基准测试的图中，对于最大的输入图，我们的算法相比BFGT实现了$110$至$530$倍的加速。