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

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

test( s i ) 等效实现对 y i 的测零; zero-test( ) 同理. 因为有两处会跳转到 zero-test( s i ) 的入口 zt i 处, 这里分别用 flagx
x i
i
和 flagy 作为信号, 确保完成测零后准确跳转回对应的位置 ( rx i 或 ry ). 最终完整的程序如图 6 中 zero-test( s i+1 )
i i
所示.
注意到, 若我们将 zero-test( s i+1 ) 中的“ s i+1 +=1; s i+1 −=1;”这一句替换成“ x i+1 +=1;”, 最终可以构造出 x i+1 = A i+1 .
至此, 我们足以完成测零的模拟和对 x n + x n = A n 的递归构造. 如下定理成立.
定理 6 [34] . 一般 VASS 可达性问题是 EXPSPACE-难的.
2 n n a、b、c. 用前文阐述的方法构
证明: 给定 2 - 有界计数器机器可达性实例 ⟨M,1 ⟩, 不妨设其使用的计数器为
(
造出 a = b = c = A n , 此过程需要使用辅助计数器 x i 、x i 、y i 、y i 、s i 、s i 、 flagx 和 flagy i ∈ [n−1]). 随后用计数器
i i
程序 P 模拟 M 的每条语句, 并将测零语句替换成对应的模块, 例如“zero? a ” 应该替换为“zero-test( a); zero-test( a);”
(只使用 zero-test( a) 会对调 a、a 的值, 需要使用 zero-test( a) 对调回来). 易知若 M 有完全运行则 P 也有完全运行,
8n−2 个计数器, 整体长度至多存在一个多
否则 P 会在某次模拟测零的过程中终止执行. 同时, 最终的程序只使用
2 n
项式的放大, 因此可以在多项式时间内构造完毕, 从而有 2 -BCM reachability ⩽ p CP reachability. 最终由引理 2 得
出结论: 一般 VASS 可达性问题是 EXPSPACE-难的. 证毕.
3.1.2 Lipton 方法的局限性与启发
Lipton 给出了一般 VASS 可达性问题复杂性的首个非平凡下界, 他的证明方法是开创性的. 但后继研究表明,
这种方法有较大的局限性. 本节将详尽分析其局限性与相应改进思路.
● 技术局限. 回顾定理 6 证明中所有模拟测零模块的行为都是完全确定的, 以至于最终并不需要判定“ P 存在

0-执行”这么强的条件, 只需判定 P 存在完全执行即可. 换而言之, 我们实际上证明的是: 一般 VASS 的可覆盖性问
题是 EXPSPACE-难的. 另外, 在程序 P 末尾添加“loop a +=1;” 语句可以使得若 M 存在 0-执行当且仅当 P 停机后
终止格局的取值情况有无限种, 于是一般 VASS 的有界性问题也是 EXPSPACE-难的. 1978 年, Rackoff [13] 给出了
可覆盖性问题和有界性问题的上界, 故有如下命题.
命题 3 [13,34] . 一般 VASS 的可覆盖性问题和有界性问题都是 EXPSPACE-完备的.
换言之, Lipton 的证明思路存在 EXPSPACE“壁垒”: 无法使用类似的归约方法得到任何严格更难的复杂性下
界 (如 Tower-难). 但由于可达性问题上下界之间差距巨大, 人们倾向于相信其一定具有严格更高的下界. 为了得
到这样的突破, 我们须在归约时构造一类行为并非完全确定的程序, 使其执行完全后至少有一个计数器的值无法
确定. 换言之, 我们须通过判定这些计数器最终的取值是 0 来保证程序中所有模拟测零是成功的; 若我们的程序不
满足此性质, 则此次构造能够证明出的下界一定不比 Lipton 的高.
● 正面启发. 从 Lipton 的证明中还可以提炼出一种模拟测零的思路.
1) 构造不变量: 若需要对 x 进行模拟测零, 维护形如 x+ x = f (n) 的不变量是有帮助的, 其中, f (n) 与用于归约
的问题有关.
2) 复用计数器: 多次模拟测零时, 不能为每一次模拟单独写一个独立的程序片段, 否则可能会造成使用的计数

器数量超指数量级. 我们更应当思考如何去复用计数器, 例如对 x、y 测零时, 可以通过类似 reset 的模块将它们的
s
值统一记录到某个计数器 s 上, 通过对 的模拟测零间接实现原目的.
x 的值转移到 上. 注
s
结合上述两点, 我们可以观察到: 若已构造出 x+ x = f (n), 每次对 x 测零时我们不妨将
s
意, 此过程会对调 x、x 的值, 为了恢复原值我们需要再操作一次. 假设待模拟机器 M 一共进行了 m 次测零且 初
始化为 0, 则完全执行后都应当满足 s ⩽ 2mf (n), 同时若 s = 2mf (n) 则说明每次测零时 x = f (n) 都成立, 即原机器
M 是否存在 0-执行.
M 的 m 次测零都成功了. 最终, 通过判定停机后 s = 2mf (n) 是否成立即可说明
上述方法依然存在问题: 首先, 2m f (n) 往往是个大数, 无法在归约的时候直接构造出来; 其次, m 的精确值大
部分情况下都是未知的. 针对第 1 点的解决方案是: 既然可以构造 x+ x = f (n), 我们不妨初始化 s = 2mf (n), 每次
m ∈ N 构造出
转移不是增加 s 而是减少 s, 最终判定 s = 0 是否成立即可. 而后者要求我们必须能够针对无限个
s = 2mf (n), 这样总会有充分大的 m 可以覆盖 M 的测零次数, 随后我们在 M 停机前添加若干次测零使得最终总测