一句话：刻画 Valence 系统双向可达性的复杂度，证明多数可判定存储机制下复杂度降至多项式时间。
无限状态系统的可达性问题通常具有极高复杂度，因此人们希望通过添加迁移得到双向系统等过近似，使可达性更高效判定。本文在 Valence 系统框架下研究双向可达性。Valence 系统由有限控制状态和一个由有限图指定的无限存储构成，通过选取不同图可统一建模向量加法系统中的计数器、下推栈、整数计数器及其组合。作者给出双向可达性的完整复杂度图谱，并与一般可达性进行对比。结果表明，对几乎所有已知可达性可判定的存储机制，双向可达性的复杂度都严格下降，许多情形甚至降到多项式时间。
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.