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

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

′ P d 如图 15 所示.
增减都需要同时作用在 a、c 上. 记 eval 为引入对 a、c 同步操作后的 eval d , 程序
d
考虑 P d 的某个 Z d -执行, 观察可知: 执行完前 3 行之后得到了一个对应 λ 0 = ((n+1)e d ,n) 的好格局 , 且
α 0
α 0 (A 0 ) , 0. 设执行 loop eval 后得到 β, 执行 loop rdec d,0 后得到 . γ(B 1 ) = ... = γ(B d ) = γ(A d+1 ) = 0,
′
γ Z d -执行保证了
d
β 也是好的. 应用引理 15 得: λ k = Eval (λ 0 ) = (0 d ,β(B 0 )), 其
(k)
因此 γ 是个好格局, 根据 rdec d,0 的性质可推断出 β 对应
中, k 是 eval 执行的次数. 根据变换 Eval 的定义可知: β(B 0 ) = Val(λ k ) = Val(λ 0 ) = F (n+1) (n) = F d+1 (n). 最终 a, b, c
′
d d
分别记录了 β(A 0 ), β(B 0 )+1, β(A 1 ), 终止格局为一个乘法三元组 τ t = (a,b,c,β(A 0 ),1+ F d+1 (n)).

0 b += n , d b += n + ;
1
1
0 a +=1, 1 a += n + , …, a += n + , 1 d a + 1 += (n + 1 )(n + ) 2 , a +=1, c += n + ; 1
d
loop a 0 +=1, 1 a += n + , …, a += n + , 1 d a + 1 += (n + 1 )(n + ) 2 , a +=1, c += n + ;
1
1
d
loop eval d ′
loop rdec d ,0
loop dec ( B )
0
reset ( B ) b +=1;
图 15 使用 eval d 构造 P d

|X d | = 4d +10 |Z d | = 2d +5, 根据推论 2 可知: (4d +10) -VASS a d+1 是
,
由于 的可达性问题是 F d+1 - 难的. 注意到
个全程没有使用过的计数器, 可以去掉, 最终有如下定理.
定理 10. d ⩾ 3 时, (4d +5)- VASS 可达性问题是 F d - 难的.
, 每个量需要两个计数器维持, 因此整体
● 技术局限. 上述方法的瓶颈在于需要构造两组量 {B i } i∈[d] 0 , {A i } i∈[d+1] 0
需要 4d +O(1) 个计数器. 但核心程序 eval d 只使用了 loop at most (1+ B 0 ) times 语句, 并没有要求对 i ⩾ 1 维持 b i +
b i = B i . 事实上, 后者是 rdec d,i 程序的要求, 而 rdec d,i 用于维持不变量 A i+1 = (1+ B i )A i , 若能找到新不变量使得 B i −=1
后对 A i+1 的副作用与 B i 无关, 则 i ⩾ 1 时便不再需要 , 从而节省 d +Θ(1) 个计数器.
b i
3.4.2 优化: 指数形式不变量
为了尽可能地复用计数器, Leroux 在文献 [38] 中使用了新不变量: 对 i ∈ [d] 0 , 维持 A i+1 = 2 A i . 每次 B i −=1 后
B i
c
只需令 A i+1 /=2 即可, 不再与 B i 具体的值有直接关联. 另外, 他还使用了一个全局计数器 来维持 a i +c = A i , 使得
原来所有的 a i 均可以舍去, 最终只需使用 2d +O(1) 个计数器. 本节将对此做详细介绍.
首先, 我们引入必要的计数器: 对 i ∈ [d], 令 b i = B i ; 令 b 0 +b 0 = B 0 ; 对 i ∈ [d +1], 令 a i +c = A i ; 令 a 0 +a 0 = A 0 ;
额外引入 b+b = B. 令 α 是这些计数器的一个格局, 给定 λ, 若 α 满足对任意 i ∈ [d] 0 都有 α(A i+1 ) = 2 α(B i ) α(A i ), 且
( )
,
α(B i ) = λ α(B) = 2 α(B 0 ) , α b 0 = α(c) = α(a 0 ) = b = 0, 则称 α 是对应 λ 的好格局. 同理, 可以定义什么样的格局是坏
的或合法的. 若 λ 非平凡, i 0 = index(λ), 设 β 是一个从 α 得到的对应 Eval(λ) 的好格局, 则 β 依然需要满足公式 (15).
至于 β 在 {A j } j∈[d+1] 0 上, 为使改动尽量少, 我们不妨令 β(X d+1 ) = α(X d+1 ), 计算可知:


 A 0 2 −α(B 0 ) , i = 0



 α(A 0 ), 1 ⩽ i ⩽ i 0 −1


 2α(A 1 ), i = i 0
β(A i ) =  (18)




 α(A i ), i 0 +1 ⩽ i ⩽ d +1
根据公式 (18) 构造 eval d,i , 如图 16 所示.

i b -=1, b − +=1;
1
i
loop dec ( a ... ,a + d 1 ), c +=1;
1 ,
loop at most A 0 times
1 ,
c -=1, a +=1, inc ( a ... ,a + d 1 ); loop at most (1 B+
i
loop at most B 0 times 0 b -=1, 0 b +=1 0 ) times
i b − 1 +=1, loop at most B times
loop at most A 0 times
0 a -=1, b +=1;
loop at most B times
c -=1, i a +=1, inc ( a ... ,a + d 1 );
, i
update , d i ( B )
eval update ,1 ( B )
, d i d
图 16 新不变量下 eval d,i 的构造

图 16 中, loop at most A 0 times 等模块与第 3.4.1 节定义一致. 在构造 eval d,i 时使用了 update ( B), 作用是更
d,i
,
,
新 B 的值, 但易知只有当 i 0 = 1 时需要修改 B, 因此对 i > 1 update ( B 0 ) 是一段空程序; 对 i = 1 update ( B 0 ) 如
d,i d,1