Integer reachability complexity depends on transfer graph structure
Integer reachability in VASS with transfers: a refined complexity analysis
Formal Languages and Automata TheoryComputational Complexity
Summary
Finding if a system can reach a certain state with integer counters is a known hard problem. The authors studied systems that include special transfer operations and discovered that certain patterns in these transfers make the problem much more complex. They identified parts of these systems called "bad counters" that determine how difficult it is to verify reachability. When there are few bad counters, the problem is easier to check; if there are many, it becomes much harder.
What this means in practice
- •For system model checkers: Determine which transfer patterns in VASS models make reachability checking computationally feasible or hard.
- •For formal verification engineers: Design verification procedures tailored to systems with limited complex transfer structures for more efficient reachability analysis.
A theory result. No direct application yet.
Authors
Tymoteusz Kucharek, Piotr Hofman
Abstract
Integer reachability is NP-complete for vector addition systems with states (VASS), but becomes PSPACE-complete in the presence of transfer operations. We refine this complexity gap for single-transfer VASS by identifying structural features of transfers responsible for the increase in complexity. Each system induces a transfer graph whose vertices are counters and whose edges represent possible transfers. We classify its vertices as good or bad, according to the branching and cyclic structure of their reachable subgraphs. Let $b$ be the number of bad vertices. We show that every positive instance admits a polynomially verifiable certificate of size $|I|^{O(b+1)}$, where $|I|$ is the input size. Consequently, integer reachability for single-transfer VASS can be decided in nondeterministic time $|I|^{O(b+1)}$; in particular, it belongs to NP for every class with a bounded number of bad counters. Conversely, we show that bad counters provide sufficient structural power to encode space-bounded computation. For every transfer graph with $b$ bad vertices, we construct a single-transfer VASS that encodes the acceptance of a Turing machine using $b^{O(1)}$ tape cells. This yields PSPACE-hardness for every polynomial-time constructible family of transfer graphs containing linearly many bad vertices. Our results isolate the transfer patterns responsible for the complexity of integer reachability.