Papers for

system model checkers

Papers whose findings have a practical use for this group, as judged from the abstract. Open a paper to read what it means in practice.

Integer reachability complexity depends on transfer graph structure

Integer reachability in VASS with transfers: a refined complexity analysis

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.

Thu 1 OctFormal Languages and Automata TheoryComputational Complexity
The gist
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.
Open → 2610.01440v1