一句话：系统解决交错 bidirected Dyck 可达性的可判定性与复杂度，改进上界并确立可判定与不可判定边界。
Dyck 可达性是许多静态分析的标准形式，但交错 Dyck 可达性通常不可判定。本文研究双向图上的交错 bidirected Dyck 可达性问题，即 D_k ⊙ D_k 及其各变体。作者给出改进算法与复杂度上下界：将 D_1 ⊙ D_1 从 O(n^7) 改进到 O(n^3·α(n))；证明 D_k ⊙ D_1 可判定，并在线性有界计数器变体上给出 O(n^2·α(n)) 算法及条件二次下界；最后证明完整 D_k ⊙ D_k 不可判定。标准基准实验显示新算法在实践中很快，较先前方法有数量级加速。
Dyck reachability is the standard formulation of a large domain of static analyses, as it achieves the sweet spot between precision and efficiency, and has thus been studied extensively. Interleaved Dyck reachability (denoted D k ⊙ D k ) uses two Dyck languages for increased precision (e.g., context and field sensitivity) but is well-known to be undecidable. As many static analyses yield a certain type of bidirected graphs, they give rise to interleaved bidirected Dyck reachability problems. Although these problems have seen numerous applications, their decidability and complexity has largely remained open. In a recent work, Li et al. made the first steps in this direction, showing that (i) D 1 ⊙ D 1 reachability (i.e., when both Dyck languages are over a single parenthesis and act as counters) is computable in O ( n 7 ) time, while (ii) D k ⊙ D k reachability is NP-hard. However, despite this recent progress, most natural questions about this intricate problem are open. In this work we address the decidability and complexity of all variants of interleaved bidirected Dyck reachability. First, we show that D 1 ⊙ D 1 reachability can be computed in O ( n 3 · α( n )) time, significantly improving over the existing O ( n 7 ) bound. Second, we show that D k ⊙ D 1 reachability (i.e., when one language acts as a counter) is decidable, in contrast to the non-bidirected case where decidability is open. We further consider D k ⊙ D 1 reachability where the counter remains linearly bounded. Our third result shows that this bounded variant can be solved in O ( n 2 · α( n )) time, while our fourth result shows that the problem has a (conditional) quadratic lower bound, and thus our upper bound is essentially optimal. Fifth, we show that full D k ⊙ D k reachability is undecidable. This improves the recent NP-hardness lower-bound, and shows that the problem is equivalent to the non-bidirected case. Our experiments on standard benchmarks show that the new algorithms are very fast in practice, offering many orders-of-magnitude speedups over previous methods.
@article{paperbot1591,
title = {The decidability and complexity of interleaved bidirected Dyck reachability},
author = {Adam Husted Kjelstrøm and Andreas Pavlogiannis},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {POPL},
year = {2022},
doi = {10.1145/3498673}
}