Reachability in pushdown vector addition systems with states (PVASS) is among the longest standing open problems in Theoretical Computer Science. We show that the problem is decidable in full generality. Our decision procedure is similar in spirit to the KLMST algorithm for VASS reachability, but works over objects that support an elaborate form of procedure summarization as known from pushdown reachability.

翻译：带状态的推送向量加法系统（PVASS）中的可达性问题是理论计算机科学中长期悬而未决的开放问题之一。我们证明该问题在完全一般性下是可判定的。我们的判定程序在本质上类似于VASS可达性的KLMST算法，但操作对象支持从推送可达性中已知的复杂过程摘要化形式。