The Decidability and Complexity of Interleaved Bidirected Dyck Reachability

TL;DR

This paper investigates the decidability and computational complexity of interleaved bidirected Dyck reachability problems, providing new algorithms, decidability results, and complexity bounds for various cases, advancing understanding in static analysis applications.

Contribution

It improves existing algorithms for $D_1owtie D_1$ reachability, establishes decidability for $D_kowtie D_1$, and proves undecidability for full $D_kowtie D_k$, clarifying the complexity landscape.

Findings

$D_1owtie D_1$ reachability computed in $O(n^3 imes ext{alpha}(n))$ time

Decidability of $D_kowtie D_1$ reachability established

Full $D_kowtie D_k$ reachability shown to be undecidable

Abstract

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\odot 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\odot 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\odot 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\odot D_1$ reachability can be computed in $O(n^3\cdot \alpha(n))$ time, significantly improving over the existing $O(n^7)$ bound. Second, we show that $D_k\odot 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\odot D_1$ reachability where the counter remains linearly bounded. Our third result shows that this bounded variant can be solved in $O(n^2\cdot \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\odot 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.