Page 15 - 《软件学报》2026年第1期

12 软件学报 2026 年第 37 卷第 1 期

play: for i :=1 to n for i := n to 1
∀play i ; ∃play ; i reset i
assert c = C reset c ; halt;
P play P reset
图 5 子集和博弈问题对应的 CSA 程序

,
A i e i , f i 的情况类似. 若
对于每个 i ∈ [n] a i , b i 仅有一个非零, 例如若 a i = 1 则 ∀ 玩家该步选择了 ; P play 能执行
∑
n
完毕, 则寻找到了使得 (x i +y i ) = C 成立的一组数, 即 ∃ 玩家通过一轮博弈.
i=1
n
随后, 我们需要合理重置进程使得最终恰好能够遍历 ∀ 玩家的 2 种不同选择. 定义如下程序模块.
n−i
reset i =do assert e i = 2 , f i =0 reset e i , f i ;
or assert e i =0, f i = 2 reset e i , f i ;
n−i
n−i
do assert a i = 2 , b i =0; goto play;
n−i
n−i
or assert a i = 2 , b i = 2 reset , ;
a i b i
重置阶段的程序如图 5 中的 P reset 所示. 最终完整的程序 P 由 P play 顺序复合上 P reset 构成 .
接着证明该构造的正确性: 易知 P 的任意一次执行 R 总会因为重置阶段的 goto play 语句不断地回到程序的
R 划分为若干段从 play R 1 ,R 2 ,... ”. 注意以下事实.
起点, 我们可以以此为断点将 处开始的执行“
( n−i )
● 若 j = 0 mod 2 , 则 R j 一定成功执行了 reset i 中的语句, 否则 R j 会因为不满足断言而中断.借此可以推断
n
若 R 为完全的执行, 则 R 恰好可以分割为 2 段.
n
● 对于一次完全的执行 R = R 1 ,...,R 2 n , 可以将每段执行的下标 j ∈ [2 ] 编码为 n-比特二进制数 j (2) . 若 j (2) 从左
i
起第 i 位为 0, 则说明博弈阶段 R j 增加了 ; 若 j (2) 从左起第 位为 1, 则说明博弈阶段 R j 增加了 . 结合 a i ,b i 的含
b i
a i
义可知, R 恰好遍历博弈树的所有分支.
● 若 R j 的执行没有中断, 则 ∃ 玩家能够赢得 对应的分支. 若 R 是完全的, 则 ∃ 玩家有必胜策略.
j
n 归纳进行证明, 其证明细节在此不再赘述, 感兴趣的读者可以参考文献 [19].
上述事实均可通过对
∑
n
综上, ∀x 1 ∈ {A 1 ,B 1 } ∃y 1 ∈ {E 1 ,F 1 }...∀x n ∈ {A n ,B n } ∃y n ∈ {E n ,F n } (x i +y i ) = C ⇐⇒ P 存在 0-执行. 将计数器
i=1
按照 a 1 , b 1 , e 1 , f 1 ,..., a n , b n , e n , f n , c 的顺序从小到大编号, 使得 P 中对某一计数器进行断言时, 编号更大的计数器
值都已知 (为 0), 这满足 CSA 的迁移规则要求, 从而 P 等价于一个 CSA. 由于所有计数器的值都不超过 b = 2 +
n
∑
(a i +b i +e i + f i ), 因此 P 是 b-安全的. 若 P 使用二进制编码, 则此构造能在对数空间完成. 证毕.
i∈[n]
现公式 (6) 中的所有归约已完成证明, 注意, 引理 8 的证明要求 CSA 必须是二进制编码的, 故后续归约使用
的 BCA 及 2-VASS 也必须是二进制编码的. 由引理 1 可得如下引理.
引理 9 [21] . 二进制编码下的 2-VASS 可达性问题是 PSPACE-难的.
结合第 2.2.1 节给出的上界, 最终得到如下定理.
定理 3 [21] . 二进制编码下的 2-VASS 可达性问题是 PSPACE-完备的.
3 d-VASS 的下界证明技术
本节先对一般 VASS 可达性问题的 Ackermann-完备性及其关于维度的参数复杂性结论做一个简要的回顾,
随后分节讨论几个重要的下界证明技术及各自的启发和局限.
20 世纪 80–90 年代, Mayr 等人 [25] 、Kosaraju 等人 [26] 、Lambert 等人 [27] 、Sacerdote 等人 [28] 就此问题进行了大
量深入的研究, 提出并简化了判定 VASS 可达性问题的算法, 即著名的 KLMST 分解算法. 2015 年, Leroux 等人 [29,30]
给出了 KLMST 算法的首个上界结论, 证明了一般 VASS 可达性问题在 F ω 3 中. 通过对原算法的不断优化, 在
2017 年和 2019 年, 上界先后被降到了 F ω 2 [31] 和 F ω [32] . 其中, 文献 [32] 的主定理是一个关于维度的精细结论, 即:
对于任意的 d ⩾ 3, d-VASS 可达性问题在 F d+4 中. 相较于最初的 F ω 3 上界, 此结论是一个巨大的提升, 但仍远未达
到最优. 2024 年, 国内研究者 Fu 等人 [33] 基于几何维度 (geometric dimension) 的概念进一步改进了 KLMST 算法,
并得到了目前关于 d-VASS 可达性问题的最优上界.