The Decidability and Complexity of Interleaved Bidirected Dyck Reachability
share
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. 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.
READ FULL TEXT