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

陈蔚骏 等: 向量加法系统可达性问题复杂性下界研究综述 33

Sciences, 1986, 32(1): 105–135. [doi: 10.1016/0022-0000(86)90006-1]
[43] Czerwiński W, Lasota S, Lazić R, Leroux J, Mazowiecki F. Reachability in fixed dimension vector addition systems with states. In: Proc.
of the 31st Int’l Conf. on Concurrency Theory (CONCUR 2020). Dagstuhl Publishing, 2020. 48. [doi: 10.4230/LIPIcs.CONCUR.2020.48]

附中文参考文献
[16] 张文博, 龙环. 向量加法系统验证问题研究综述. 软件学报, 2018, 29(6): 1566–1581. http://www.jos.org.cn/1000-9825/5465.htm [doi:
10.13328/j.cnki.jos.005465]
[17] 杨启哲. 向量加法系统模型研究 [博士学位论文]. 上海: 上海交通大学, 2022. [doi: 10.27307/d.cnki.gsjtu.2022.000038]

附录 A

表 A1 本文数学符号对照表

符号 含义 符号 含义
N 自然数集 a,b,c, x,y,z ∈ X 计数器
Z 整数集 x, y, z 与 x,y,z 互补的计数器
ω 最小的极限序数 i, j, k 常用于表示自然数
N ω 自然数集的扩充 N∪{ω} {x i } i , {y i } i , {z i } i 表示一族作用相似的计数器
d, D 维度 n 输入规模
d
u,v ∈ N ,Z d d维自然数/整数向量 f,g,h : N → N 自然数上的函数
∥ · ∥ 向量的无穷范数 t(n), s(n) 时间函数、空间函数
| · | 某个集合的基数 NL, NP,... 各种经典复杂性类
0 d , 0 全零向量 ⩽ p , ⩽ L 多项式时间归约, 对数空间归约
V 某个VAS或VASS ι 序数
A ⊆ Z d VAS迁移规则集合 {F ι } ι 快速增长函数谱系
a ∈ A 某条VAS迁移规则 {F ι } ι 快速增长函数类谱系
Q 状态集 {F ι } ι 快速增长复杂性类谱系
p,q,r ∈ Q 状态 O, Ω, Θ 渐进复杂性记号
d
T ⊆ Q×Z × Q VASS迁移规则集合 poly(n) 多项式函数
t ∈ T 某条VASS迁移规则 inv 不变量
α,β,... ∈ Q×N d VASS格局 τ 乘法三元组或 inv -三元组
π ∈ T ∗ 可达性证据 Ampl 放大器
α→ V β 在 V 中 α 到 可达 Gen 生成器
β
V的一进制和二进制编码长度 Z 控制计数器集合
|V| 1 , |V| 2
M 各类自动机 B 常用于表示上界
I 1 , I 2 , I 3 ,... 机器指令 λ 快速增长函数的向量编码
P 计数器程序 Val 解码函数
X 计数器集合 Eval(λ) 编码 λ 的求值变换

作者简介
陈蔚骏, 博士生, 主要研究领域为程序语言, 进程演算, 并发模型.
傅育熙, 博士, 特聘教授, CCF 杰出会员, 主要研究领域为理论计算机科学.
龙环, 博士, 副教授, 博士生导师, CCF 专业会员, 主要研究领域为理论计算机科学.