The complexity of bidirected reachability in valence systems.

We study the complexity of bidirected reachability problems arising in many areas of program analysis. We formulate the problem abstractly in terms of bidirected valence automata over graph monoids, an algebraic framework that generalizes many models of automata with storage, including CFL-reachability, interleaved Dyck reachability, vector addition systems over naturals or integers, and models involving complex combinations of stacks and counters. Our main result is a characterization of the decidability and complexity of the bidirected reachability problem for different graph classes. In particular, we characterize the complexity of bidirected reachability for every graph class for which reachability is known to be decidable. We show that there is a remarkable drop in complexity in going from the reachability to the bidirected reachability problems for many natural models studied previously. Our techniques are algebraic, and exploit the underlying group structure of the bidirected problem. As a consequence of our results, we characterize the complexity of bidirectional reachability of a number of open problems in program analysis, such as the complexity of different subcases of bidirectional interleaved Dyck reachability.