Aarhus University Seal

The Decidability and Complexity of Interleaved Bidirected Dyck Reachability

Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaperJournal articleResearchpeer-review


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 circle dot 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 circle dot 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 circle dot 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 circle dot D-1 reachability can be computed in O(n(3) . alpha(n)) time, significantly improving over the existing O(n(7)) bound. Second, we show that D-k circle dot 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 circle dot D-1 reachability where the counter remains linearly bounded. Our third result shows that this bounded variant can be solved in O(n(2) . alpha(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 circle dot 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.

Original languageEnglish
Article number12
JournalProceedings of the ACM on Programming Languages
Number of pages26
Publication statusPublished - Jan 2022

    Research areas

  • static analysis, CFL/Dyck reachability, bidirected graphs, complexity, POINTS-TO ANALYSIS, CFL-REACHABILITY, FLOW-ANALYSIS, ALGORITHMS

See relations at Aarhus University Citationformats

ID: 264073098