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

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

证明: 给定计数器机器 f(n)-有界可达性问题实例 M、1 , 不妨假定 M 使用的计数器是 x,y,z < X (我们总能通
n
X = X n ∪{x,y,z} 的程序 , 如图 7 所示.
′
′
过重命名达到这个目的), 构造使用计数器 n P

b′ += n ; loop y -=1, x +=1, c -=1;
loop a′ +=1, c′ += n ; loop z -=1, y +=1, c -=1;
n P ; loop b -=1, z +=1, c-=1;
M ′ ; a -=1;
loop loop b +=1, z -=1, c -=1;
zero-test ( x ) ; loop z +=1, y -=1, c -=1;
do half-zero-test ( x ) ; or skip ; loop y +=1, x -=1, c -=1;
loop b -=1; a -=1;
P′ zero-test (x)
M 的执行
图 7 使用放大器和乘法三元组模拟

′
P 可以划分为 3 个阶段.
1) 初始化阶段. 第 1 个 loop 语句构造了一个平凡的乘法三元组, 若其完全执行后 a = A s , 则一定有 c = A s n,
′
′
( ′ ′ ′ ′ )
因此执行 P 前的初始格局是 τ s = a ,b ,c ,A s ,n,X . Ampl n 是一个 f (n) -放大器, 它的程序 P n 不改变 x、y、z 的值,
n
(
X n 的 ′ τ s 出发可以 τ t = a,b,c,A t , f (n),X .
)
′
可以看作计数器集合为 f(n)-放大器, 因此从 Z n -计算出某个
n
2) 模拟阶段. M 由 M 变换而来. 首先对于 M 中形如 x += 的语句, 则 M 中需转换为 x += ; k; 形如 x −=
′
k
′
k b −=
′
k 的语句, 则转换为 x −= ; k, 即借用计数器 b 辅助维持 x+y+z+b 总量不变. 注意, 执行 M 前的格局 τ t 满足
k b +=
x+y+z+b = f (n). 其次, 对跳转语句的模拟是平凡的, halt 语
x = y = z = 0, b = f (n)t, 因此每次执行完模拟后都有
′
句直接忽略. 最后, 考虑 M 中形如“zero? x”的语句, 在 M 中需转换为图 7 中 zero-test(x) 所示的程序模块. 设
zero-test(x)
,
α −−−−−−−→ β, 则计数器 c、a 的减少量分别满足 0 ⩽ ∆c ⩽ 2(α(y)+α(z)+α(b)) = 2( f (n)−α(x)) ∆a = 2. 注意, ∆c =
2 f (n) 当且仅当 α(x) = 0, 并且此时 α、β 在除了 a、c 的计数器上取值是一致的, 此情况称作一次完全的模拟.
′
3) 结束阶段. 乘法三元组中 a 的值指定了对应的模拟测零次数, 若 M 中未完成对应次数的模拟测零, 我们则
a 的清零. 随后非确定地选择执行 1 次或 0 次模块 half-
需要在结束阶段非确定地循环若干次测零模块来完成对
zero-test( x), 即 zero-test( x) 的前 4 行, 此处是为了使得即便 a 的值为奇数也能被置零. 最终, 使用循环语句将
x、y、z、b 清零.
M 存在一个使用了 次测零的 f(n)-有界
k
正确性分析. 假设 0-执行 R, 令 A = 2k, 由 Ampl n 的性质可知: 存在 A s
( ′ ′ ′ ′ ) ( ′ ) ′ ′
R
使得 P n 能够从 τ s = a ,b ,c ,A s ,n,X n 出发 Z-计算出 τ t = a,b,c,A t , f (n),X n 使得 A t ⩾ A. 考虑 P 的执行 , 它在初
′ R, 因
始化阶段恰好循环 A s 次, 使得执行 P n 前初始格局恰好是 , Z-执行完程序 P n 可以构造出 . 随后用 R 模拟
τ s
τ t
为 R 中每个格局都满足 x+y+z ⩽ f (n), 这是可以做到的. zero-test 模块的性质保证存在一条路径使得最终执行完
′ A t −2k 次且每次模拟测零都是完全
M 后的格局 β 满足 β(a) = A t −2k, β(c) = (A t −2k) f (n), 让结束阶段循环恰好

的, 则最终 a = c = 0. 由于执行完 P n 后, a、b、c 外计数器的值为 0 且不再改变, 计数器 a、b、c 也被清零了, 可以
确定终止格局为 0.
)
(
′
′
′
′
′
′
′
反之, 假设 P 存在一个 0-执行 R , 则在初始化阶段, R 对某个 A s 构造出了 τ s = a ,b ,c ,A s ,n,X . 由于模拟阶
n
P n 后就为 0. 由此可知, ′ P n 的部分
段和结束阶段不改变 Z 中计数器的值, 因此这些计数器在执行完 R 中对应程序
( )
′
是 Z 执行, 存在 A t 使得执行后格局为 τ t = a,b,c,A t , f (n),X . 最终 a,c = 0, 因此模拟阶段和结束阶段共进行了 A t /2
n
次模拟测零和至多 1 次半模拟测零, 得到满足 β(c) = 0 的格局 β, 从而每一次模拟测零都是完全的, 且对应的待测
零计数器确实是 0. 考虑 R 对应程序 M 的部分, 可以诱导出一个 M 的完全执行 R; 因为 R 维持了 x+y+z ⩽ f (n),
′
′
′
因此 R 是 f(n)-有界的.
综上, M 存在 f(n)-有界 0-执行当且仅当 P 存在 0-执行. P 使用了 |X n |+3 个计数器, 整体上是多项式长的, 因
′
′
此 CM f(n)-bounded reachability ⩽ p VASS reachability. 当 |X n | 是个与 n 无关的常数 d 时, 该结论可以更精细地表述
为 CM f(n)-bounded reachability ⩽ p (d + 3)-VASS reachability. 证毕.
此引理为本节核心内容, 其主要贡献如下.
1) 引入了基于乘法三元组的通用模拟测零技术.
2) 介绍了给定一族 f(n)-放大器 {Ampl n } 后, 模拟 f(n)-有界计数器机器的一般方法.