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

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

模拟. 关于 VAS 与 VASS 两大模型的关系, Hopcroft 等人 [12] 在 1979 年证明了如下命题.
命题 1 [12] . 任意 d-VASS 都可以被一个 (d + 3)-VAS 模拟.
此命题的证明思路是为原来 VAS 中的向量额外增加 3 个维度用于编码状态信息, 构造过程是高效的. 基于此
命题, 后文将集中讨论 VASS 上的可达性问题.
1.2 VASS 可达性问题
一般 VASS 可达性问题的形式化定义如下.

一般 VASS 可达性问题 (general VASS reachability)
输入: 一个 VASS V = (d,Q,T), 两个格局 p(u),q(v) ∈ Q×N ;
d
输出: 是否有 p(u)→ V q(v)?
此处“一般 (general)”指的是不对输入的 VASS 模型的维度加任何限制. 此问题的复杂性已有完备性结论. 出
于应用及理论两方面的动机, 目前本领域主要聚焦于固定维度 VASS 的可达性问题, 其表述如下.

d-VASS 可达性问题 (d-VASS reachability)

d

输入: 一个 d-VASS V = (d,Q,T), 两个格局 p(u),q(v) ∈ Q×N ;
输出: 是否有 p(u)→ V q(v)?
注意, 此处 d 是一个固定的参数. 例如研究 2-VASS 可达性问题时, 所有输入的 VASS 实例都必须是 2 维的.
可以进一步限制初始和目标格局的向量都为 0, 从而将以上两个问题的表述简化为: 仅输入 V = (d,Q,T) 与状
态 p,q ∈ Q, 判断是否有 p(0)→ V q(0). 显然这是一般可达性问题的特例, 但其复杂性与原问题相等: 给定一个原可
(
)
}
{
V、p(u)、q(v), 我们可以高效地构造 V = d,Q∪ q s ,q f ,T , 其中, Q 中的新状态, 且
′
′
达性问题实例 q s 、q f 是不在
{ ( )}
′ q s (0)→ V ′ q f (0). 为此, 在讨论 VASS 可达性问题复杂
T = T ∪ (q s ,u, p), q,−v,q f . 这使得 p(u)→ V q(v) 当且仅当
性下界时, 我们约定使用简化版的表述.
研究可达性问题的复杂性时, 我们需要分析算法运行时间或空间与问题规模的关系. 这需要严格定义 VASS
向量常用的两类编码方案, 它们将直接影响复杂性结论. 给定 V = (d,Q,T), 令 |Q|、|T| 分别表示 Q、T 集合的大
小. 对于 t = (p, a,q) ∈ T , 定义它的范数为其中向量的范数, 即 ∥t∥ := ∥a∥, 同时定义 ∥T∥ := max∥t∥. 根据不同进制,
t∈T
VASS V 的规模分别表示如下.
● 在一进制编码 (unary encoding) 下, V 的规模 |V| 1 := |Q|+d ·|T|·∥T∥.
● 在二进制编码 (binary encoding) 下, V 的规模 |V| 2 := |Q|+d ·|T|· log(∥T∥+1) .
⌈
⌉
直观上, 二进制编码在各类算法研究中都是常用方案; 而在一进制编码下 VASS 可以在多项式时间内转换为
−1 的受限 VASS, 后者则与自动机 (automaton) 联系紧密 [18] , 因此其也是
对应的迁移规则只允许对某一维度 +1 或
研究的主要对象之一. 以例 2 中的 V 2 为例, 有 |Q| = 2, |T| = 4, ∥T∥ = k, 从而 |V 2 | 1 = 12k +2 |V 2 | 2 = 12 log(k +1) +2.
⌈
⌉
,
由此可见, 同一个 VASS 在从二进制转换为一进制编码后长度有一个指数量级的放大. 对低维度 VASS 而言这样
的放大将会对复杂性产生较大影响, 特别是导致二进制编码下的可达性问题严格难于一进制编码下的可达性问题;
而高维度和一般 VASS 的复杂性远高于指数复杂性谱系, 此时编码方式对复杂性没有影响, 不必再加以区分.
1.3 计数器自动机、计数器程序
除了 VASS 和 Petri 网模型外, 在理论研究中人们也提出了诸多和 VASS 等价的、更方便研究的模型. 本节介
绍最常用的一种, 其特点是可读性强. 其他一些等价模型将会在相关章节再分别讨论.
计数器机器 (counter machine, CM) 或计数器自动机 (counter automaton, CA) 本质上是一个指令的有限序列
P = (I 1 ,...,I n ), 其中, I 1 ,...,I n 只能为下面 5 类指令 (可带标签).
1) 加法: “ x += a;”. 这里的 a 指代某一常量, x 是某个变量, 一般称为计数器.