2021/10/07 by Moses Ganardi, Ganardi, Moses, Rupak Majumdar +3 · 1 citation
Computer Science · Mathematics · #Combinatorics #Computer science #Decidability #Discrete mathematics #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Formal Methods in Verification #Logic, programming, and type systems #Machine Learning and Algorithms #Mathematics #Reachability #cs.FL
paper · pdf · doi:10.48550/arxiv.2110.03654
published in arXiv (Cornell University) (Cornell University) · 27 pages
openalex publication_date 2021/10/07 · arxiv created 2022/06/26 · arxiv updated 2022/06/28 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Reachability problems in infinite-state systems are often subject to extremely high complexity. This motivates the investigation of efficient overapproximations, where we add transitions to obtain a system in which reachability can be decided more efficiently. We consider bidirected infinite-state systems, where for every transition there is a transition with opposite effect. We study bidirected reachability in the framework of valence systems, an abstract model featuring finitely many control states and an infinite-state storage that is specified by a finite graph. By picking suitable graphs, valence systems can uniformly model counters as in vector addition systems, pushdowns, integer counters, and combinations thereof. We provide a comprehensive complexity landscape for bidirected reachability and show that the complexity drops (often to polynomial time) from that of general reachability, for almost every storage mechanism where reachability is known to be decidable.