On the Complexity of Bidirected Interleaved Dyck-Reachability
summary
Shows that bidirected InterDyck reachability is decidable for D1 ⊙ D1 and gives a concrete polynomial-time algorithm that computes all pairs reachable by specially defined “shallow” D1⊙D1 paths using context-free grammar reasoning, region-based enumeration, and a cycle‑rearrangement proof to bound unmatched stacks. Extends with an NP-hard via PAFP reduction lower bound for Dk ⊙ Dk, and provides an implemented and compared solver demonstrating the D1 relaxation often yields a tighter over‑approximation than previous methods.
AI-written summary · about
chapters (9)
- 0:00Introduction
- 2:39Interleaved DyckLanguage
- 4:56General Inner Diversibility
- 7:04D1D1 Reachability
- 11:16Pass
- 13:20Shallow Path
- 16:28Moving Cycles
- 21:44Transform Graph
- 25:42Conclusion
related talks
17mA Better Approximation for Interleaved Dyck Reachability
18mThe Complex(ity) Landscape of Checking Infinite Descent
15mRecursive State Machine Guided Graph Folding for Context-Free Language Reachability
18mPolymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in ...
26mProperty-Directed Reachability as Abstract Interpretation in the Monotone Theory
44mPlaying with Grammars: What Have We Known So Far!
18mParameterized Algorithms and Complexity for Function Merging with Branch Reordering
19mPolymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in(…)