Identifying live and dead states in an abstract transition system is a recurring problem in formal verification; for example, it arises in our recent work on efficiently deciding regex constraints in SMT. However, state-of-the-art graph algorithms for maintaining reachability information incrementally (that is, as states are visited and before the entire state space is explored) assume that new edges can be added from any state at any time, whereas in many applications, outgoing edges are added from each state as it is explored. To formalize the latter situation, we propose guided incremental digraphs (GIDs), incremental graphs which support labeling closed states (states which will not receive further outgoing edges). Our main result is that dead state detection in GIDs is solvable in $O(\log m)$ amortized time per edge for $m$ edges, improving upon $O(\sqrt{m})$ per edge due to Bender, Fineman, Gilbert, and Tarjan (BFGT) for general incremental directed graphs. We introduce two algorithms for GIDs: one establishing the logarithmic time bound, and a second algorithm to explore a lazy heuristics-based approach. To enable an apples-to-apples experimental comparison, we implemented both algorithms, two simpler baselines, and the state-of-the-art BFGT baseline using a common directed graph interface in Rust. Our evaluation shows $110$-$530$x speedups over BFGT for the largest input graphs over a range of graph classes, random graphs, and graphs arising from regex benchmarks.

翻译：在抽象转移系统中识别活跃状态与死状态是形式化验证中的一个反复出现的问题；例如，在我们近期关于SMT中高效判定正则约束的研究中便出现了该问题。然而，当前最先进的用于增量式维护可达性信息（即在状态被访问时且在整个状态空间被探索之前）的图算法假设新边可在任意时刻从任意状态添加，而在许多应用中，出边是在每个状态被探索时从其添加。为形式化后一种情况，我们提出引导式增量有向图（GIDs），这类增量图支持标记封闭状态（即不会再有新出边的状态）。我们的主要结果是：在GIDs中，死状态检测可在每条边均摊$O(\log m)$时间内解决（其中$m$为边数），相较于Bender、Fineman、Gilbert与Tarjan（BFGT）针对一般增量式有向图提出的每条边$O(\sqrt{m})$的复杂度有所改进。我们为GIDs引入两种算法：第一种建立了对数时间界，第二种则探索基于懒惰启发式的方法。为实现公平的实验比较，我们在Rust中使用通用有向图接口实现了两种算法、两种更简单的基线方法以及最先进的BFGT基线方法。评估显示，在多种图类、随机图以及正则表达式基准测试生成的图上，对于最大输入图，我们的方法相较于BFGT实现了$110$-$530$倍的加速。