一句话：通过改进经典分解算法及其终止性证明，将固定维数 VAS 可达性上界降至原始递归，并给出一般情形的 ACKERMANN 上界。
向量加法系统（VAS）的可达性是静态验证及众多可相互归约判定问题的核心。此前即使固定维数，已知上界也不是原始递归的。本文精细改进 Mayr、Kosaraju 与 Lambert 的经典分解算法及其终止性证明，重新分析分解树与递推复杂度，从而在一般情形得到 ACKERMANN 上界，在固定维数得到原始递归上界。该结果虽未达到已知的 TOWER 下界，但对若干相关问题是紧的。
The reachability problem in vector addition systems is a central question, not only for the static verification of these systems, but also for many inter-reducible decision problems occurring in various fields. The currently best known upper bound on this problem is not primitive-recursive, even when considering systems of fixed dimension. We provide significant refinements to the classical decomposition algorithm of Mayr, Kosaraju, and Lambert and to its termination proof, which yield an ACKERMANN upper bound in the general case, and primitive-recursive upper bounds in fixed dimension. While this does not match the currently best known TOWER lower bound for reachability, it is optimal for related problems.