一句话：证明了双向交错 Dyck 可达性的首个可判定变体 D1⊙D1 属于 PTIME，并证明 k≥2 时为 NP-hard，且其过近似更精确。
许多程序分析需要推理成对匹配动作，如调用/返回、加锁/解锁等，这类问题常可形式化为带标号有向图上的 Dyck 可达性。交错 Dyck 可达性 Dk⊙Dk 是自然扩展，但一般情形不可判定；其在双向图上的变体复杂度此前未知。本文研究双向图上的交错 Dyck 可达性，建立了首个可判定变体 D1⊙D1 可达性，并证明该问题属于 PTIME；同时证明当每种 Dyck 语言含 k≥2 种括号时，Dk⊙Dk 可达性是 NP-hard。作者实现了 D1⊙D1 的多项式时间算法，并将其作为 Dk⊙Dk 的过近似方法：先将双向 Dk⊙Dk 松弛为双向 D1⊙D1 再精确求解。实验上将该方法与已有 Dk⊙Dk 过近似算法比较，发现尽管 D1⊙D1 表达力更弱，基于它的过近似却能得到更精确的解。
Many program analyses need to reason about pairs of matching actions, such as call/return, lock/unlock, or set-field/get-field. The family of Dyck languages { D k }, where D k has k kinds of parenthesis pairs, can be used to model matching actions as balanced parentheses. Consequently, many program-analysis problems can be formulated as Dyck-reachability problems on edge-labeled digraphs. Interleaved Dyck-reachability (InterDyck-reachability), denoted by D k ⊙ D k -reachability, is a natural extension of Dyck-reachability that allows one to formulate program-analysis problems that involve multiple kinds of matching-action pairs. Unfortunately, the general InterDyck-reachability problem is undecidable. In this paper, we study variants of InterDyck-reachability on bidirected graphs , where for each edge ⟨ p , q ⟩ labeled by an open parenthesis ”( a ”, there is an edge ⟨ q , p ⟩ labeled by the corresponding close parenthesis ”) a ”, and vice versa . Language-reachability on a bidirected graph has proven to be useful both (1) in its own right, as a way to formalize many program-analysis problems, such as pointer analysis, and (2) as a relaxation method that uses a fast algorithm to over-approximate language-reachability on a directed graph. However, unlike its directed counterpart, the complexity of bidirected InterDyck-reachability still remains open. We establish the first decidable variant (i.e., D 1 ⊙ D 1 -reachability) of bidirected InterDyck-reachability. In D 1 ⊙ D 1 -reachability, each of the two Dyck languages is restricted to have only a single kind of parenthesis pair. In particular, we show that the bidirected D 1 ⊙ D 1 problem is in PTIME. We also show that when one extends each Dyck language to involve k different kinds of parentheses (i.e., D k ⊙ D k -reachability with k ≥ 2), the problem is NP-hard (and therefore much harder). We have implemented the polynomial-time algorithm for bidirected D 1 ⊙ D 1 -reachability. D k ⊙ D k -reachability provides a new over-approximation method for bidirected D k ⊙ D k -reachability in the sense that D k ⊙ D k -reachability can first be relaxed to bidirected D 1 ⊙ D 1 -reachability, and then the resulting bidirected D 1 ⊙ D 1 -reachability problem is solved precisely. We compare this D 1 ⊙ D 1 -reachability-based approach against another known over-approximating D k ⊙ D k -reachability algorithm. Surprisingly, we found that the over-approximation approach based on bidirected D 1 ⊙ D 1 -reachability computes more precise solutions, even though the D 1 ⊙ D 1 formalism is inherently less expressive than the D k ⊙ D k formalism.
@article{paperbot1172,
title = {On the complexity of bidirected interleaved Dyck-reachability},
author = {Yuanbo Li and Qirun Zhang and Thomas Reps},
journal = {Proceedings of the ACM on Programming Languages},
volume = {5},
number = {POPL},
year = {2021},
doi = {10.1145/3434340}
}