自1962年Petri网^[1]的概念提出以来, 经过半个多世纪的发展, 其已成为描述与分析并发系统最重要的形式化工具之一.除在并发程序语言形式化验证中的重要应用外, Petri网模型还被广泛应用于生物、化学、金融、网络、安全等不同领域的建模和分析^[2-9].其中, Ball等人定义了并行库系统(parameterized library system, 简称PLS), 在此基础上实现了多线程程序的模型检测工具^[2], 并证明了PLS系统上的一些验证问题与Petri网上的验证问题等价; Aalst用Petri网对工作流管理系统进行建模, 用Petri网理论来验证工作流过程的正确性^[3]; Heiner等人^[4]用Petri网对生化反应过程建模, 实现了对生化系统中短时间内的行为进行有效的分析等.国内的研究者也对类似问题进行了深入研究, 特别是将Petri网理论广泛应用于对网络及安全等领域的验证.代表性的工作包括:北京交通大学Lei教授等人用Petri网对无线网络系统建模, 以实现对无线网络的性能的有效分析^[5]; 清华大学林闯教授等人在Petri网的基础上定义了私有Petri网, 对恶意软件造成的私有信息泄露行为进行分析^[6]; 以及同济大学Yu教授等人用Petri网对电子商务的支付过程建模, 验证电子商务支付系统的安全性^[7]等.

与Petri网等价的数学模型向量加法系统(vector addition system, 简称VAS)具有数学描述上的简洁性, 且现实中并发系统的状态和迁移往往都可以用向量描述, 故VAS本身也具有重要的理论和应用价值.VAS模型验证的核心问题之一是可达性(reachability)问题, 即对给定的VAS模型, 判断从一个初始格局出发能否到达一个指定的目标格局.令人遗憾的是:虽然关于VAS已经有了大量的理论和应用研究, 也有了一些高效的实现工具, 但对可达性问题的复杂性, 至今仍没有给出令人满意的回答.另一方面, VAS是极为简洁的系统, 在实际研究中, 人们根据不同的应用背景提出了一些重要的扩展模型(如下推向量加法系统PVAS、交互向量加法系统AVASS、分枝向量加法系统BVASS、带数据的Petri网模型PND(Petri nets with data)等).但对这些模型的相关验证问题的研究都处于初始阶段.

本文第1节形式化定义向量加法系统及一些重要的验证问题.第2节为本文重点, 总结一般VAS上可达性问题的主要结论和核心研究技术.第3节陈述当维度固定时VAS上可达性问题的主要结论和技术.第4节总结几个重要VAS扩展模型上的验证问题的结论.第5节给出现有主要验证结论一览表.本文覆盖了VAS研究领域的最新进展、关键技术和开放问题.

1 向量加法系统基础 1.1 VAS的形式化定义

向量加法系统(vector addition system, 简称VAS), 可以表示为二元组V=〈d, A〉.d ∈$\mathbb{N}$表示V的维度, A⊆ $\mathbb{Z}$^d表示迁移规则(transition rule)集合.VAS中的一次迁移$u{\xrightarrow{a}_V}v$满足v=u+a, 其中, u, v ∈$\mathbb{N}$^d, a ∈A.VAS的一次从向量u₀到u_n的运行(run)是一个有限长度的迁移序列${u_0}{\xrightarrow{{{a_1}}}_V}{u_1}...{u_{n - 1}}{\xrightarrow{{{a_n}}}_V}{u_n}$, 也可以写作${u_0}{\xrightarrow{{{a_1}...{a_n}}}_V}{u_n}$.用符号σ=a₁…a_n表示迁移规则序列.

带状态的向量加法系统(vector addition system with states, 简称VASS)可以表示为三元组V=〈Q, d, T〉.Q是有限的状态集合, d ∈$\mathbb{N}$表示V的维度, T⊆Qx$\mathbb{Z}$^dxQ表示迁移规则集合.VASS中, 格局(configuration)指的是集合Confs_V=Qx$\mathbb{N}$^d中的元素.VASS中的一次迁移$(q, u){\xrightarrow{t}_V}(q', v)$是满足v=u+a的三元组, 其中, u, v ∈$\mathbb{N}$^d, t=(q, a, q') ∈T.从格局c₀到格局c_n的一次运行是一个有限长度的迁移序列${c_0}{\xrightarrow{{{t_1}}}_V}{c_1}...{c_{n - 1}}{\xrightarrow{{{t_n}}}_V}{c_n}$, 也可以写作:

${c_0}{\xrightarrow{{{t_1}...{t_n}}}_V}{c_n}$

针对上面两个模型, Hopcroft和Pansiot在1979年的工作^[10]中证明了n维VASS可以用n+3维VAS来表达, 因此两者的可达性问题等价.

1.2 验证问题的形式化定义

本节具体给出VAS模型上几个著名验证问题的形式化定义.

可达性(reachability)问题.

输入:VAS V (VASS V), 初始和结束向量u, u'(格局c, c');

问题:是否存在一次从u到u'(从c到c')的运行.

可覆盖(coverability)问题.

输入:VAS V, 初始和结束向量u, u';

问题:是否存在向量u"≥u'(u"的每一维都大于等于u'的相应维), 且存在从u到u"的运行.

有界性(boundedness)问题.

输入:VAS V, 初始向量u;

问题:u可达的向量集合是否有限.

VAS的可达性关系(reachability relation)用→^*表示, 对于两个向量u, u' ∈$\mathbb{N}$^d, 如果u到u'可达, 那么(u, u') ∈→^*.值得一提的是, VAS模型验证的核心问题是可达性问题.实际应用中, 很多具体的验证问题都可以归约到可达性问题.

2 VAS上的验证问题的复杂性 2.1 主要结论

VAS模型上的覆盖性和有界性都已经有了确定的结论.最早是Lipton和Rackoff^{[11, 12]}给出的EXPSPACE-完备的结果.Rosier对他们的证明做了细化, 得到了更精确的, 几乎完全匹配的上下界^[13].

Lipton在1976年证明了可达性问题有EXPSPACE的算法下界^[11].可判定结果则用了更长的时间:Sacerdote与Tenney在1977年给出了关于此问题的部分结论^[14]; Mayr在1981年完善了原结果, 并给出了可判定性的完整证明, 但该证明非常复杂^[15]; Kosaraju在1982年对证明进行了简化^[16]; 1992年, Lambert在前人工作的基础上给出了清晰的可判定性证明^[17].他们工作中的主要证明技术被称为KLMST分解.遗憾的是, 基于KLMST分解的算法没有给出复杂性上界.近年, 关于VAS模型可达性结论的主要进步是Leroux等人自2009年开始的一系列工作:Leroux^[18]利用KLMST分解给出了基于前向递归不变量的较简洁的可达性判定算法; 基于此思想, 首次给出了不基于KLMST的判定算法^{[19, 20]}.这两个证明为VAS可达性问题建立了非常重要的几何直观, 并使得研究算法复杂性成为可能.新进展是Leroux等人在LICS 2015会议上给出的基于理想(ideal)的分解算法^[21], 并首次给出了可达性问题的上界结论: ${F_{{\omega ^3}}}.$但这是一个超原始递归的界, 且与Lipton给出的EXPSPACE-难下界之间存在巨大差距.可以看出:一般VAS模型上的可达性及相关问题在历经数十年的研究后, 依然保持着其神秘性.

2.2 VAS主要研究技术及其特点

VAS上的可达性验证是领域内最受关注也最重要的问题.经过近40年的研究, 研究者已发展了一套独立、有效的研究技术.下面从验证算法的上界和下界两方面来介绍现有主要研究成果, 重点是对关键证明技术的总结和分析.

2.2.1 上界技术

迄今为止, VAS可达性验证的技术可以分为两大类:2011年之前的技术都属于KLMST分解算法(或对该算法的精化)以及2011年Leroux提出的基于递归不变量的算法.下面重点陈述此类算法并对其局限和未来可能的工作做分析.

●  KLMST分解算法

前文说过一般的VAS和VASS的可达性问题等价, 本节将在VAS的定义下介绍KLMST分解算法.KLMST分解算法会维护一个标记证据图序列(marked witness graph sequence)集, 对其中不满足完美(perfect)条件(等价于Kosaraju文中的q条件^[16])的标记证据图作分解.如果分解结束时集合不为空, 则原可达性问题可达; 否则不可达.Leroux在2015年给出了KLMST算法的上界${F_{{\omega ^3}}} $, 本节将给出这个复杂性类的定义.该分解算法用了Karp- Miller覆盖树^[22], 其构造算法有F_ω的下界^[23], 由此得出KLMST算法的下界.这与目前的上界${F_{{\omega ^3}}}$之间也有差距.

首先引入大于所有自然数的元素ω, 并定义N_ω=$\mathbb{N}$∪{ω}.对于所有的z ∈ $\mathbb{Z}$ , ω+z=z+ω=ω.在集合F⊆{1, 2, …, d}上定义映射${\pi _F}:\mathbb{N}_\omega ^d \to \mathbb{N}_\omega ^d$, π_F在集合F的维度上保持不变, 将F之外的维度映射到ω.证明中用到的核心概念是证据图(witness graph).这是一个有限的强连通有向图G=(S, E), 其中:点集为$S \subseteq \mathbb{N}_\omega ^d$; 边集为E⊆SxAxS, 任意一边(u, a, v) ∈E满足u+a=v.对于e ∈E, D(e)=a.易见:证据图中的所有点, 在某一维度上是否为ω是一致的.记取值为ω的分量集合为I, 记$\bar I = \{ 1, 2, ..., d\} \backslash I$.

KLMST分解算法使用的重要工具是标记证据图(marked witness graph) M=(G, cⁱⁿ, sⁱⁿ, c^out, s^out), 其中:G是证据图; sⁱⁿ, s^out是G中的两个点, 代表图的输入节点(input vertices)和输出节点(output vertices); ${c^{in}}, {c^{out}} \in \mathbb{N}_\omega ^d$表示输入限制(input constraint)和输出限制(output constraint).对于i ∈{1, 2, …, d}, 如果sⁱⁿ(i)≠ω, 那么cⁱⁿ(i)=sⁱⁿ(i), 输出节点和输出限制也有同样的关系.记cⁱⁿ, c^out中取值为ω的分量集合为Iⁱⁿ, I^out:

$\overline {{I^{in}}} = \{ 1, 2, ..., d\} \backslash {I^{in}}, \overline {{I^{out}}} = \{ 1, 2, ..., d\} \backslash {I^{out}}.$

Ω_M表示所有的运行$u\xrightarrow{{{a_1}...{a_n}}}v$的集合, 其中, ${c^{in}} = {\pi _{\overline {{I^{in}}} }}(u), {c^{out}} = {\pi _{\overline {{I^{out}}} }}(v)$, π_T(a₁)…π_T(a_n)是M中的一条路径.标记证据图序列(marked witness graph sequence)是标记证据图和迁移规则交叉组成的序列:ξ=M₀, a₁, M₁, …, a_k, M_k, 其中, ${M_j} = ({G_j}, c_j^{in}, s_j^{in}, c_j^{out}, s_j^{out})$, Ω_ξ表示所有运行${u_0}\xrightarrow{{{\sigma _0}}}{v_0}\xrightarrow{{{a_1}}}{u_1}\xrightarrow{{{\sigma _1}}}{v_1}...\xrightarrow{{{a_k}}}{u_k}\xrightarrow{{{\sigma _k}}}{v_k}$的集合, 其中, ${u_j}\xrightarrow{{{\sigma _j}}}{v_j} \in {\Omega _{{M_j}}}$.定义L_ξ为多元组(u₀, ψ₀, ν₀, …, u_k, ψ_k, ν_k)的集合, 其中, ψ_i:E_i→$\mathbb{N}$满足${v_i} = {u_i} + \sum\limits_{e \in {E_i}} {{\psi _i}(e)\Delta (e)} $.

标记证据图序列ξ如果满足以下3个条件, 则称ξ满足完美条件.

(1) 可泵性(pumpability):对一个标记证明图M, Ω_M中存在运行使得在I中的维度都能达到无穷大, 则称M是向前可泵的(forward pumpable).类似地, 可以定义向后可泵的(backward pumpable).如果ξ中的所有标记证据图都是向前、向后可泵的, 那么称ξ满足可泵性;

(2) 边无界性(edge unboundedness):对于ξ中的每一个标记序列图M_j, Ψ_j表示L_ξ中所有ψ_j的集合.对于所有e ∈E_j, 如果supΨ_j(e)=ω, 那么称ξ满足边无界性;

(3) 输入/输出限制无界性(input/output constraint unboundedness):对于ξ中的每一个标记序列图M_j, U_j, V_j表示L_ξ中所有u_j, v_j的集合, 如果$\sup {U_j} = c_j^{in}, \sup {V_j} = c_j^{out}$, 那么称ξ满足输入/输出限制无界性.

KLMST分解算法将会构建标记证据图序列集合的序列Ξ₀, Ξ₁, Ξ₂, ….初始的Ξ₀={ξ₀}, ξ₀=M₀=(G₀, u, (ω, …, ω), u', (ω, …, ω)), G₀=({s}, {s}xAx{s}), s=(ω, …, ω).算法的每一步, 若当前集合Ξ_i为空, 则算法回答“不可达”; 若Ξ_i不为空, 则会检测Ξ_i中的每一个标记证据图序列, 选出其中一个不满足完美条件的标记证据图序列ξ, 将其分解成有限的标记证据图序列集合dec(ξ), Ξ_i+1=(Ξ_i\{ξ})∪dec(ξ).如果所有标记证据图序列都满足完美条件, 则算法终止, 回答“可达”.对满足完美条件的标记证据图序列ξ最重要的结论是:

引理2.1^[21].标记证据图序列ξ是否满足完美条件, 是指数空间内可判定的.

另一方面, 对不满足完美条件的标记证据图序列ξ, 将对ξ作分解.若ξ中存在一个标记证明图M是不可泵的, 假设它在第i ∈I维有上界, 那么分解后的标记证据图将具体化第i维的数值, I=I∪{i}; 若ξ不满足边无界, 其中, e出现的次数有上界, 那么会在标记证据图中去掉e这条边, 得到一个由e连接的标记证据图序列; 若ξ不满足输入限制无界, 假如第i ∈Iⁱⁿ维不满足, 那么将输入限制替换为有限多种可能的数值, Iⁱⁿ=Iⁱⁿ∪{i}, ξ不满足输出限制无界.为方便理解, 我们构造了具体例子介绍分解算法.

例:对V=〈3, A〉, A={a₁=(2, -1, 0), a₂=(0, -1, 1), a₃=(-1, 1, -1), a₄=(2, 1, -1)}, u=(0, 0, 3), u'=(1, 2, 0), 问u到u'是否可达.

初始的ξ₀=M₀如图 1所示.

记p=(p₁, p₂, p₃, p₄) ∈$\mathbb{N}$⁴表示每条规则使用的次数.解线性方程组$\sum\limits_{i \in \{ 1, 2, 3, 4\} } {{a_i}{p_i}} = u' - u, p = (1, 0, 1, 0) + n(0, 3, 2, 1)$, n ∈$\mathbb{N}$.规则a₁只会出现1次, 不满足边无界条件.算法将ξ₀中的a₁边去掉, 将其分解成多个由a₁连接的标记证据图.得到标记证据图序列${\xi _1} = {M'_0}, {a_1}, {M'_1}$.如图 2所示.

${M'_0} = ({G'_0}, (0, 0, 3), (\omega, \omega, \omega ), (\omega, \omega, \omega ), (\omega, \omega, \omega )), {M'_1} = ({G'_1}, (\omega, \omega, \omega ), (\omega, \omega, \omega ), (1, 2, 0), (\omega, \omega, \omega ))$

接着构造从${M'_0}, M'$的输入限制出发的Karp-Miller树以及从输出限制出发的反向的Karp-Miller树, 如图 3所示.可以看出: ${M'_0}$不是向前可泵的, $M'$不是向后可泵的.ξ₁不满足可泵条件.算法将${G'_0}$中不可泵的维度具体化, 因为不可泵的维度上取值是有限的, 得到的依然是一个有限的图.ξ₁可以分解为集合Ξ₂, 图 4是集合Ξ₂中的一个元素, 记作ξ₂: ${\xi _2} = {M''_0}, {a_1}, {M''_1}, {M''_0} = ({G''_0}, (0, 0, 3), (\omega, 0, 3), (\omega, 1, 2), (\omega, 1, 2)), {M''_1} = ({G''_1}, (\omega, 0, 2), (\omega, 0, 2), (\omega, 2, 0), (1, 2, 0))$.

这里的ξ₂是满足完美条件的标记证据图序列, 算法不会再对其分解.算法结束时Ξ_i至少包含ξ₂, 因此u到u'可达.

为了说明上述计算过程会终止, 为标记证据图序列ξ定义一个秩函数(ranking function)r.这个秩函数会将ξ映射到三元组的多重集合, 包含每一个标记向量图的(|I|, |E|, |Iⁱⁿ|+|I^out|).例如r(ξ₀)={(3, 4, 0)}, r(ξ₁)={(3, 3, 3), (3, 3, 3)}, r(ξ₂)={(1, 9, 1), (1, 6, 1)}.在Dershowitz定义的多重集合的序下^[24], 对于所有的ξ ∈dec(ξ), 有r(ξ) > r(ξ').因为这个在多重集合上的序是一个良序(well order), 由良序的性质, 所有秩函数严格递减的ξ序列都是有限的.又因为每次对ξ分解得到的集合dec(ξ)也是有限集, 由柯尼格引理, KLMST分解算法一定终止.

下面对KLMST分解算法作复杂度分析, 这里非常重要的是引入了一类所谓的非初等(non-elementary)复杂性类, 它的定义依赖于集合论中的序数理论.

对于序列ξ₀, ξ₁, ξ₂, …满足ξ_n+1 ∈dec(ξ_n), 有r(ξ₀) > r(ξ₁) > r(ξ₂) > ….分解过程中, 这个序列长度的上界记做L.序数a < ε₀(${\varepsilon _0} = {\omega ^{{\omega ^{{\omega ^ \ldots }}}}}$)有唯一的康托范式$\alpha = {\omega ^{{\alpha _1}}}{c_1} + ... + {\omega ^{{\alpha _n}}}{c_n}$, 其中, c₁, …, c_n ∈$\mathbb{N}$, 序数a₁ > a₂ > … > a_n.也可以等价地写作$\alpha = {\omega ^{{\alpha _1}}} + ... + {\omega ^{{\alpha _m}}}$, 序数a₁≥a₂≥…≥a_m.对于两个序数$\alpha = {\omega ^{{\alpha _1}}} + ... + {\omega ^{{\alpha _n}}}$和$\beta = {\omega ^{{\beta _1}}} + ... + {\omega ^{{\beta _m}}}, \alpha \oplus \beta = {\omega ^{{\gamma _1}}} + ... + {\omega ^{{\gamma _{n + m}}}}$, 其中, γ₁≥γ₂≥…≥γ_m+n是α_i和β_i的重排序.

我们可以把秩函数r的取值等价地看做${\omega ^{{\omega ^3}}}$以下的序数.对于标记证据图M, 序数b_M=ω²|I|+ω|E|+(|Iⁱⁿ|+|I^out|).对于标记证据图序列$\xi = {M_0}, {a_1}, {M_1}, ..., {a_k}, {M_k}, {\beta _\xi } = \mathop \oplus \limits_{1 \leqslant j \leqslant k} {\omega ^{{\beta _{{M_j}}}}}$.例如在前面的例子中,

${\beta _{{\xi _0}}} = {\omega ^{{\omega ^2} \cdot 3 + \omega \cdot 4}}, {\beta _{{\xi _1}}} = {\omega ^{{\omega ^2} \cdot 3 + \omega \cdot 3 + 3}} \cdot 2, {\beta _{{\xi _2}}} = {\omega ^{{\omega ^2} + \omega \cdot 9 + 1}} + {\omega ^{{\omega ^2} + \omega \cdot 6 + 1}}.$

给定$\alpha = {\omega ^{{\alpha _1}}}{c_1} + ... + {\omega ^{{\alpha _n}}}{c_n}$, 定义$N(\alpha ) = \mathop {\max }\limits_{1 \leqslant j \leqslant n} \{ {c_i}, N({\alpha _i})\} .N({\xi _0}) = 4, N({\xi _1}) = 3, N({\xi _2}) = 9$.注意, 控制函数(control function) g:$\mathbb{N}$→$\mathbb{N}$是严格增函数.g_α是一个超限递归定义的函数:g₀(n)=0, g_α+1(n)=1+g_α(g(n)), g_λ(n)=g_λ(n)(n).其中, λ是极限序数.λ(n)的超限递归定义是:(γ+ω^β+1)(n)=γ+ω^β(n+1), (γ+ω^λ')(n)=γ+ω^λ(n).

例:$\omega (n) = n + 1, {\omega ^{{\omega ^3}}}(n) = {\omega ^{{\omega ^3}(n)}} = {\omega ^{{\omega ^2}(n + 1)}}$;

g_k(n)=k, g_ω(n)=g_n+1(n)=n+1, g_ω+1(n)=1+g_ω(g(n))=2+g(n).

为了研究复杂性, 还需要定义控制函数$H(n) = n + 1, {H_{{\omega ^2}}}(n) = {H_{\omega (n + 1)}}(n) = ({2^{n + 1}} - 1)(n + 1), {H_{{\omega ^3}}}(n)$是一个Non-elementary函数, ${H_{{\omega ^\omega }}}(n)$是非原始递归函数.

定义g^k(n)=g(g^k-1(n))表示函数g迭代k次, ${g^\alpha }(n) = {g^{{g^\alpha }(n)}}(n)$.最后可以定义复杂性类:

${\mathcal{F}_{ < \alpha }} = \bigcup\limits_{\beta < {\omega ^\alpha }} {FSPACE({H^\beta }(n))}, {F_{h, \alpha }} = \bigcup\limits_{p \in {\mathcal{F}_{ < \alpha }}} {SPACE({h^{{\omega ^\alpha }}}(p(n)))}, {F_\alpha } = {F_{H, \alpha }}.$

在KLMST分解中, 假设ξ=M₀, a₁, M₁, …, a_k, M_k, ξ' ∈dec(ξ).

可以看出, N(β_ξ)不超过$||\xi || = {\max _{0 \leqslant j \leqslant k}}(2d, k, |{E_j}|, |I_j^{in}| + |I_j^{out}|, |{I_j}|)$.我们将会构造控制函数g, 使得||ξ||≤g(||ξ||).在ξ不满足边无界或输入/输出限制无界条件的情况下, ||ξ'||的大小相比||ξ||有一个不超过指数的放大; 而在x不满足可泵条件时, 因为用到了Karp-Miller树, 有$||\xi '|| \leqslant {H^{{\omega ^{d + 1}}}}||\xi |{|^4}$ ^[25], 我们可以构造控制函数g(x)= ${H^{{\omega ^{d + 1}}}}(p(x))$, 其中, p(x)是给定的多项式函数.这个控制函数在VAS的维度d固定时是在$\mathcal{F}$_<ω中的原始递归函数, 当维度d作为输入的一部分时, 是在$\mathcal{F}$_<ω+1中的非原始递归函数.

综上, 在KLMST分解中构造的标记证据图序列的大小有上界g^L(n), 其中, $L = {g_{{\omega ^{{\omega ^3}}}}}(n)$.因此, KLMST分解算法用到的空间不超过${g^{{\omega ^{{\omega ^3}}}}}(n)$.因此, VAS可达性问题属于复杂性类${F_{g, {\omega ^3}}}$.因为${F_{g, {\omega ^3}}} = {F_{{\omega ^3}}}$ ^[26], 所以有如下结论.

定理2.2^[21]. VAS的可达性问题上界不超过${F_{{\omega ^3}}}.$

研究展望:关于KLMST分解的最新研究是2015年Leroux定义了理想的概念^[21], 给出了对KLMST分解的另一个直观解释:KLMST分解是对路径集合的理想的分解.这可能对VAS的其他扩展模型的验证问题有启发作用.此外, KLMST分解的算法目前已知的上界${F_{{\omega ^3}}}$和下界F_ω有一个差距, 与VAS可达性问题本身的下界EXPSPACE-hard之间有一个更大的差距, 这些都值得进一步研究.

● 基于递归不变量(inductive invariant)的算法

基于递归不变量(inductive invariant)算法.这个算法有两个半可判定过程:第1个不断枚举所有的动作序列以证明可达, 第2个枚举所有的Presburger公式证明不可达.Leroux证明了如果向量u到向量u'不可达, 那么存在一个可以用Presburger公式表示的向量集合, 向量u在这个集合中, 而向量u'不在这个集合中^[16].并且这个集合相对于可达性关系是一个前向递归不变量, 即, 所有集合中的向量的下一步依然在这个集合中.因此, 这个Presburger集合就是不可达的一个证明(witness).目前, 这个方法只有可判定的结果, 没有算法复杂性上界.

如果集合S⊆$\mathbb{Z}$^d可以写成如下形式: $L(C, P) = \left\{ {x|\exists c \in C, \exists {\alpha _1}, ..., {\alpha _k} \in \mathbb{N}, \exists {p_1}, ..., {p_k} \in P, x = c + \sum\limits_{i = 1}^k {{\alpha _i}{p_i}} } \right\}$, 其中, C, P⊆$\mathbb{Z}$^d, 则称S是半线性集(semi linear set).Hopcroft等人证明了5维以下的VAS的可达集是可被有效计算的半线性集^[10].集合S⊆$\mathbb{Z}$^d如果可以被Presburger算术FO($\mathbb{Z}$, +, ≤, 0, 1)中的公式表示, 那么称S是Presburger集合.Ginsburg等人证明了, 集合S是Presburger集合当且仅当S是半线性集^[27].

最近, Leroux对一般情况下VAS的可达集给出了更加精确的描述.2011年, Leroux定义了Lambert集合和Petri集合的概念^[19], 证明了在一般情况下, VAS的可达集是Lambert集合, 可达性关系的集合是Petri集合.其中, Petri集合一定是Lambert集合; Lambert集合一定也是Presburger集合.下面给出这些集合的定义.

集合P⊆$\mathbb{Z}$^d满足0 ∈P, P+P⊆P, 则称P为周期集合(periodic set).对于周期集合P, 如果$\mathbb{Q}$_≥0P在FO($\mathbb{Q}$, +, ≤, 0, 1)上可定义, 则称P是多胞周期集合(polytope periodic set).如果集合L⊆$\mathbb{Z}$^d是有限个集合的并, 其中每个集合可以表示为b+P, b ∈$\mathbb{Z}$^d, P⊆$\mathbb{Z}$^d是多胞周期集合, 则称L是Lambert集合.如果集合X⊆$\mathbb{Z}$^d, 满足对于任意Presburger集合S⊆$\mathbb{Z}$^d, S∩X是Lambert集合, 则称X是Petri集合.

例:周期集合${P_1} = \{ (m, n) \in {\mathbb{N}^2}|m \leqslant \sqrt 2 n\} $不是多胞周期集合.周期集合P₂={(0, 0)}∪{(2ⁿ, 1)|n ∈$\mathbb{N}$}∪ {(m, n)|m≥1, b≥2, m, n ∈$\mathbb{N}$}. ${\mathbb{Q}_{ \geqslant 0}}{P_2} = \{ (0, 0)\} \cup \mathbb{Q}_{ > 0}^2$在FO($\mathbb{Q}$, +, ≤, 0, 1)上可定义, P₂是多胞周期集合.因此, P₂是Lambert集合.同时, P₂不是Petri集合, 因为对于Presburger集合$\mathbb{N}$×{1}, P₂∩($\mathbb{N}$×{1})={(2ⁿ, 1)|n ∈$\mathbb{N}$}不是Lambert集合.

对给定自反传递的关系R⊆$\mathbb{Z}$^dx$\mathbb{Z}$^d, 集合X, Y⊆$\mathbb{Z}$^d.定义:

$pos{t_R}(X) = \bigcup\limits_{x \in X} {\{ y \in {\mathbb{Z}^d}|(x, y) \in R\} }, pr{e_R}(Y) = \bigcup\limits_{y \in Y} {\{ x \in {\mathbb{Z}^d}|(x, y) \in R\} } $

若post_R(X)⊆X, 则称X是相对于关系R的前向递归不变量(forward inductive invariant); 若pre_R(Y)⊆Y, 则称Y是相对于关系R的后向递归不变量(backward inductive invariant).定义R的区分(separators) (X, Y):X, Y⊆$\mathbb{Z}$^d并且都是Presburger集合, 满足R^*∩(XxY)是空集.如果关系R本身是Petri集合, 则称R是Petri关系.

Leroux证明了下面的重要结论:

引理2.3^[19]. VAS的可达性关系是一个Petri关系.

进一步得到关于Petri关系的一个主要结论是:

引理2.4^[19].若R^*⊆$\mathbb{Z}$^dx$\mathbb{Z}$^d是一个Petri关系, X', Y'⊆$\mathbb{Z}$^d是两个Presburger集合, R^*∩(X'×Y')=∅, 那么存在一个区分(X, Y), 其中, X是前向递归不变量, Y是后向递归不变量, 满足X'⊆X, Y'⊆Y.

如果u到u'不可达, $\mathbb{Z}$^d就可以划分为前向递归不变量X和后向递归不变量Y, X, Y都是Presburger集合, 其中,u ∈X, u' ∈Y.因此有一个判定VAS不可达的半可判定过程:通过不断枚举Presburger公式表示的向量集合, 判断其是否包含u而不包含u'.

研究展望:注意到, 基于前向递归不变量的算法不依赖于KLMST分解算法.不过, 该算法的复杂性目前仍然是公开的.这个复杂性依赖于最短的可达路径长度和最短的能够表示一个可以区分起点和终点的前向递归不变量的Presburger公式长度.值得一提的是:虽然VAS可能会有一个有限的Ackermann大小的可达集合, 但该算法中表示前向递归不变量的Presburger集合是可达集合的一个超集, 因此该算法还是可能有比F_ω更好的下界.

总结:目前, VAS可达性的上界算法主要有KLMST分解算法和基于递归不变量的算法.KLMST分解算法试图去分析可达路径, 最终得到的标记证据图序列可以看出路径的结构.该算法会有F_ω的下界和${F_{{\omega ^3}}}$的上界.基于递归不变量的算法更加直观, 同时枚举所有的路径以证明可达, 和所有的前向递归不变量以证明不可达.但该算法的复杂性分析似乎比KLMST分解算法更难.

2.2.2 下界技术

Lipton在1976年给出了VAS可达性问题的EXPSPACE的算法下界.Lipton首先提出了并行程序(parallel programs)的模型, 证明了并行程序上的可接受问题(the acceptance problem)可以多项式时间归约到VAS的可达性问题.然后, 递归构造了可以模拟3个有界的计数器的并行程序(这里的计数器可以做加法、减法、测0操作), 计数器的界是这个并行程序的双指数大小.而用3个双指数大小的计数器可以来模拟任意需要指数空间的图灵机, 因此可以得到VAS的可达性问题EXPSPACE-hard的下界.

其中, Lipton用到的直观概念是并行程序(parallel programs).并行程序是三元组P=〈F, d, x〉, 其中, F是并行的流程图(flowcharts)的集合, d是维数, x=(x₁, …, x_d) ∈$\mathbb{N}$^d是所有流程图共同维护的d维向量.每个流程图是有限的有向图, 包含4种节点:起始节点、接受节点、猜测节点、赋值节点.如图 5所示.

并行程序的格局(configuration)可以表示为c=〈p₁, …, p_m, x₁, …, x_d〉, m=|F|.其中, p_i表示第i个流程图当前节点的编号.并行程序的初始格局C₀中, p_i是第i个流程图的起始节点, x_i=0.

并行程序每一步运行$\langle {p_1},...,{p_m},{x_1},...,{x_d}\rangle { \to _P}\langle {p'_1},...,{p'_m},{x'_1},...,{x'_d}\rangle $需要满足以下中的一个条件.

(1) 存在i ∈{1, 2, …, m}, p_i是起始节点, $p'_i$是p_i唯一的后继节点.对于所有的$j \ne i, {p'_j} = {p_j}$; 对于所有的j, ${x'_j} = {x_j}$;

(2) 存在i ∈{1, 2, …, m}, p_i是猜测节点, $p'_i$是p_i两个后继节点中的一个.对于所有的$j \ne i, {p'_j} = {p_j}$; 对于所有的j, ${x'_j} = {x_j}$;

(3) 存在i ∈{1, 2, …, m}, p_i是赋值节点, $p'_i$是p_i唯一的后继节点.对于所有的$j \ne i, {p'_j} = {p_j}$; 对于所有的j, ${x'_j} = {x_j} + {c_j} \geqslant 0$.

用$ \to _P^*$表示→_P的传递闭包.并行程序的可接受问题(acceptance problem)问是否存在一个格局C=〈p₁, …, p_m, x₁, …, x_d〉, 使得${C_0} \to _P^*C$, 其中, 存在一个i, 使得p_i是接受节点.可以证明, 并行程序上的可接受问题和VAS的可达性问题满足如下关系:

引理2.5^[11].并行程序上的可接受问题可以多项式时间归约到VAS的可达性问题.

我们可以通过研究并行程序上可接受问题的下界来回答VAS可达性问题的下界.注意, 并行程序可以模拟计数器的加法和测零操作.加法操作的模拟比较直观; 模拟测零操作的思路是用两维向量x, x' ∈$\mathbb{N}$, 令它们始终保持$x + x' = {A_k} = {2^{{2^k}}}$的关系.这样, 判断x是否为0, 等价于判断x'是否能够等于A_k.Lipton递归地构造一个并行程序中的程序块${\alpha _{{x_i}}}$, 程序块${\alpha _{{x_i}}}$可以在${x_i} + {x'_i} = {A_i}$的条件下测试x_i是否为0:如果x_i为0, 则该程序块将走YES出口, 并互换${x_i}, x'$的值; 如果x_i不为0, 则该程序块将走NO出口.

●  i=1时, 程序块如图 6所示.

●  i > 1时, 设置辅助变量${u_i} + {u'_i} = {A_{i - 1}}, {v_i} + {v'_i} = {A_{i - 1}}, {b_i} + {c_i} = 0$.u_i, v_i分别控制两层循环, 赋值节点${x_i} + 1, {x'_i} - 1$将会经过$A_{i - 1}^2 = {A_i}$次.程序块${\alpha _{{{v'}_i}}}, {\alpha _{{{u'}_i}}}$的作用类似于${\alpha _{{x_{i - 1}}}}$, 但为保证构造出的并行程序大小在多项式范围内, 加入了新的流程图, 如图 7(b), 用来调用程序块${\alpha _{{x_{i - 1}}}}$.b_i, c_i在程序块中起到了调用和返回的作用.

将变量${x'_i}({u'_{i + 1}}, {v'_{i + 1}})$赋值为A_i, 只需要把图程序块赋值节点${x_i} + 1, {x'_i} - 1$替换成${x'_i} + 1$即可.而模拟计数器的测0操作只需执行两次程序块, 第2个程序块中需要将其中的${x_k}, {x'_k}$互换, 作用是将${x_k}, {x'_k}$的值再交换回来.第2个程序块中不会走到NO出口(如图 8所示).

因此, 并行程序上的可接受问题是EXPSPACE-hard.

由引理2.5, VAS可达性问题的下界也是EXPSPACE-hard.

定理2.6^[11]. VAS可达性问题的下界是EXPSPACE-hard.

研究展望:在关于下界的研究方面, 已有技术的核心是VAS系统可以模拟双指数大小的计数器, 由此其可达性问题的下界是EXPSPACE-hard.类似的技术可以推广到下推向量加法系统.下推向量加法系统在向量加法系统的基础上增加了一个栈, Lazic证明了它可以模拟界是2↑↑n的计数器^[28], $\left. {2 \uparrow \uparrow n = {2^{{2^{{ \cdots ^2}}}}}} \right\}n{个}2$.因此, 下推向量加法系统上的可达性问题是Non-elementary的.特别值得一提的是, 可以看出, 这类下界证明的共同点都是巧妙的“计数”.我们认为, 这类方法可以被推广到其他模型的研究中.

3 固定维度时验证问题的复杂性 3.1 主要结论

在前面的讨论中, 向量的维度d是输入的一部分.而在实际应用中, 问题的维度往往存在固定的上界. Hopcroft和Pansiot在1979年的工作^[10]中指出:当VAS的维数在5之内时, 其可达集是一个可被有效计算的半线性集.由于n维VASS可以用n+3维VAS表示, 这就等价于得出了2维之内VASS可达性问题、等价性问题(equivalence)、包含问题(containment)等的可判定结论.他们同时用反例说明了该技术无法被应用到3维及更高维度的VASS的研究.

关于低维度VASS的研究结果主要包括:Hasse与Kreutzer等人^[29]在2009年证明了1-VASS(即1维VASS, 等价于4维VAS)的可达性问题在一进制编码下是NL-完备的, 而在二进制编码下是NP-完备的.Haase在其博士论文^[30]中证明了同一模型在输入是二进制编码时的有界性问题和可覆盖问题都是NP-完备的.而对2-VASS, Howell等人^[31]对Hopcroft的算法进行了分析, 指出原始算法的复杂度是非确定双指数时间(2-NEXPTIME), 并进一步将算法上界改进到了确定双指数时间(2-EXPTIME).而关于二进制编码下2-VASS上可达性问题的最终结果则是在最近几年才得出:Fearnley等人^[32]给出了PSPACE-hard的证明; 紧接着, Blondin等人^[33]在2015年找到了PSPACE的判定算法, 从而证明了该问题实际上是PSPACE-完备的.他们工作的一个额外结论是证明了对固定维度(d≥2维)d-VASS, 有界性和可覆盖性都是PSPACE-完备的.值得一提的是, Blondin等人的工作, 本质上是对Leroux等人^[34]在2004年有关2-VASS具有平坦性(flatness)证明的精化.当限制为输入是一进制编码时, 2-VASS可达性问题在2016年被证明是NL-完备的^[35].到目前为止, 在可达性问题上没有关于3-VASS或更高维度模型的结果:既没有更准确的下界结论, 也没有任何非平凡(即优于${F_{{\omega ^3}}}$)的判定算法.下面总结其中代表性的研究技术, 并指出未来可能的工作方向.

3.2 固定维度VASS主要研究技术及其特点

目前, 固定维度VASS的复杂性结果集中在2维及以下, 即:当向量维度大于2时, 仅有平凡结论(即2维问题的下界和维度无限制时的上界).因此, 这里集中讨论2维及2维以下模型相关的研究技术.

3.2.1 上界技术(算法) 3.2.1.1 二维VASS的平坦化(flatness)

已有d维(d≤2)VASS的算法都依赖于一个重要的结论:此维度限制下的VASS是可平坦化的.对给定的VASS V=(Q, T), 其中, Q代表状态集合, T代表迁移规则集合, V的输入规模被定义为|V|=|Q|+|T|×d×log₂|T|.用α₀, β₁, α₁, …, β_k, α_k代表V上一组不含循环、可执行的迁移规则序列, 则一组形如$\rho = {\alpha _0}\beta _1^*{\alpha _1}...\beta _k^*{\alpha _k}$的串, 被称为一条线性路径策略(linear path scheme).典型的线性路径策略如图 9所示.

有限条线性路径策略的并集被称为半线性路径方案(semi-linear path scheme).若V的可达关系集合可以表示为一个半线性路径方案, 则我们称V是具有平坦性的(相应称对应的可达关系集合是平坦的).直观上讲, 平坦性意味着对应的可达路径可以被表示为一组只依次含有若干简单环的路径(即, 不存在环的嵌套), 而具有这样结构的路径所对应的可达关系是有效半线性的.对给定的二元关系R_V⊆QxQ, $R_V^*$为R_V的自反传递闭包.Leroux等人的主要结论^[34]是:当2维VASS的初始向量和目标向量中两个分量的值都大于某个可计算的常数时, 对应的二元关系是平坦的.这个性质称做终极平坦性(ultimately flat). $R_V^*$的其他子集能相对简单地证明具有平坦性.最终, $R_V^*$集合是有效半线性集.但Leroux等人的工作中并没有给出对应方案的具体取值范围, 故而无法直接得出更有效的复杂性上界.

直到2015年, Blondin等人^[33]对Leroux的研究进行了量化, 给出了上述常数c的上界(|Q|+T)^O(1).并证明了如果初始格局到目标格局可达, 则在对应的平坦性的关系中, 半线性集合将由一组有效的、指数规模的线性路径策略(即$|\rho |\mathop = \limits^{def} |{\alpha _0}{\beta _1}...{\beta _k}{\alpha _k}|$为输入的指数函数)组成, 特别地, 其中简单环个数(即k)相对输入是多项式大小, 绕每条简单环重复次数的上界相对输入是指数大小.综合上述结果, 算法可猜测(利用非确定性)路径上的中间状态, 并利用多项式空间的计数器控制搜索的上界, 即:对一组可达格局对, 算法必然能在多项式空间内停止并给出一个正面的回答.再根据Savitch定理PSPACE=NPSPACE, 就完成了关于2-VASS可达性具有(确定)多项式空间算法的证明.这是目前关于固定维度VASS最好的结果.

Blondin工作中一个相对独立的结果是, 证明了非确定有限自动机所识别的路径的Parikh像(Parikh image, 用于表达路径中每个字符出现的次数的函数)存在一个多项式规模的使用线性路径策略的表达方式.基于这个结论, 很容易就能证明:当将原始可达性验证问题的条件放宽到整数意义下时, 任意d维VASS上的可达性等价于存在一组有限的、多项式规模的线性路径策略.当然, 这与各维向量值都应限制为自然数下的可达性还有距离.为此, 他们将问题分成了3种子类型.

(1) 初始格局和目标格局的状态相同, 且始末状态两个计数器的值都大于常数c, 但对中间运行情况不做限制;

(2) 初始格局到目标格局的整条路径上, 两个计数器的值都大于常数c;

(3) 初始格局到目标格局的整条路径上, 至少有一个计数器的值不超过常数c.

以上3种情况分别对应于图 10中的3种不同路径类型.

Blondin等人证明了这3种情况下的VASS的可达关系都有指数规模的刻画.具体而言, 类型(3)可规约到维度为1的情况从而化简.类型(2)可以用类型(1)的结论推导得出.对最关键的类型(1), 与d≤2这个限制直接相关的核心技术引理是:

引理3.1^[33].令b ∈Z², P⊆Z²且b ∈P, 令Z是2维空间中的一个象限, 则有$L(b;P) \cap Z = \bigcup\limits_{i \in I} {L({c_i};{P_i})} $, 且对每个i ∈I, 如下结论成立:

●  |P_i|≤2;

●  P_i⊆(P∪L(b; P))∩Z; 且

● 存在e≤P^O(1), 满足{c_i}∪(P_i∩L(b; P))⊆b+cone_{[0, e]}(P).

即:在2维情况下, 对满足引理前提的线性集L(b; P), 考虑其与任意象限的交集, 结果都可以表示为一组简单的半线性路径的并; 或者更具体地说, 由一组周期(period, 即P_i)的基数为2, 且周期和基(base, 即c_i)来自一个简单集合的线性路径组成.值得注意的是, 这个引理对d≥3的情况均不成立.

最后, 通过证明任意2维VASS的可达路径都可分解为多项式规模段类型为类型(1)、类型(2)、类型(3)的路径后, 就完成了2维情况下问题上界的证明.

研究展望:当维数固定时的研究, 是近年关于VASS验证研究的核心.特别值得注意的是:除了上面的引理3.1及其相关推论外, Blondin在文献[33]中的其他结论都可以被直接应用或推广到更高维的情况.因此, 对更高维情况的研究, 重点和难点是对3维及以上的情况找到类似引理3.1的降维结论.

3.2.2 下界技术

下界来自对有界单计数器自动机(bounded one-counter automata)模型上可达性问题的规约.

有界单计数器自动机(可以表示为三元组V=(Q, T, b), 其中, (Q, T)就是1-VASS, 而b ∈N是用二进制表达的计数器值的上界.令B=[0, b], 对给定的初始格局p(u)和目标格局q(v), u, v ∈B.与一般的可达性问题不同的是:可达性关注是否存在从p(u)到q(v)的可行路径, 且路径上每一个中间格局对应的计数器的值都不超过b.即问关系$p(u) \to _B^*q(v)$是否成立.

Fearnley等人^[32]在2013年证明了有界单计数器自动机上的可达性问题是PSPACE-complete.

对任意有界单计数器自动机V=(Q, T, b), 可构造其可达性问题到2-VASS可达性问题的规约.规约的核心是利用界限参数b:构造2-VASS $V'\mathop = \limits^{def} (Q, \{ h(t):t \in T\} )$, 其中, h函数的具体定义是$h(p, z, q)\mathop = \limits^{def} (p, (z, - z), q)$.注意:因为原模型V中u, v ∈B, 所以V'中两个向量对应的计数器的值都不会小于0.此时, 如下的当且仅当关系显然成立:

模型V中$p(u){\xrightarrow{\pi }_B}q(v)$当且仅当模型V'中$p(u, b - u){\xrightarrow{{h(\pi )}}_{{N^2}}}q(v, b - v)$.

研究展望:注意, 这部分所得到的下界结论可以平凡地延伸到维度d≥3的情况.但因为目前对3维的情况了解甚少, 可优先考虑相关算法的研究, 增加对模型的认知之后, 再考虑合适的下界规约.

4 重要扩展模型

随着应用领域研究的推进, 研究者们逐渐意识到现有VASS模型的局限并定义和发展了若干重要的扩展模型.鉴于篇幅限制, 这里只列举领域内近年来备受关注的几个重要模型, 并总结关于这些模型的验证问题的最新结论.

4.1 PVAS

下推向量加法系统(pushdown vector addition system, 简称PVAS)是在VASS模型之上增加了栈及相应的入栈(push)和出栈(pop)操作.

PVAS上一条典型的迁移规则为: $(p, u, X)\xrightarrow{{v, op}}(q, u + v, X')$, 其中, $(p, u)\xrightarrow{v}(q, u + v)$的含义与VASS完全一致, $X\xrightarrow{{op}}X'$用于记录栈的变化(op为栈操作), PVAS为研究同时具有递归与整数变量的程序语言提供了一个简洁的数学模型^[36].

PVAS模型是VASS的非平凡扩展.Leroux等人证明了PVAS终止性和有界性都可判定^[37], 但没有进一步的上界结论; 目前仍不知道PVAS上可覆盖性和可达性问题是否可判定, 仅仅知道它们都是Tower-hard^[28], 复杂性远高于VASS上的对应验证问题.

在维度固定时, 仅当维度为1时有一些进展.Leroux等人证明了1-PVAS可覆盖性是NP-hard, 上界是EXPSPACE^{[38, 39]}, 而有界性问题是NP-hard, 相应的上界是EXPTIME^{[39, 40]}.

关于PVAS非常特殊的一点是, n-PVAS的可达性, 可以规约到n+1-PVAS的可覆盖性, 即, PVAS模型下的可达性问题和可覆盖性问题难度本质上一样.这也从另一个角度说明了PVAS的特殊性.

4.2 AVASS

Alternating VASS最早是由Lincoln等人在研究命题线性逻辑(propositional linear logic)的可判定性时被提出来的.AVASS是一个四元组A=Q, d, T_u, T_f.其中:Q是有限的状态集合; d ∈N代表维度; T_u⊆QxZ^dxQ是一元迁移规则, 如$q\xrightarrow{v}{q_1}$; 而T_f⊆Q³是状态分叉(fork)规则, 如q→q₁∧ q₂.作为例子, 当一元迁移规则作用在格局(q, u)上时, 下一格局是(q₁, u+v); 而当分叉规则作用在同一格局上时, 下一格局是(q₁, u)或(q₂, u).显然, VASS是AVASS的一个特殊子类, 即T_f=∅的情况.

关于AVASS的主要结论是可达性不可判定^[41].Courtois等人证明了:若将求解(格局)可达性削弱为状态可达性, 则问题难度是双指数完备的^[42].当AVASS模型中向量维度固定时, 状态可达性问题(及非终止性问题)难度降低为EXPTIME完备的.值得一提的是:AVASS状态可达性问题的研究可以有效地规约到BPP、VASS与有限状态系统的模拟问题上, 从而得到了新的下界结论.这也成为研究AVASS的重要原因之一.

4.3 BVASS

VASS的计算过程可以理解为一个线性过程.Branching VASS^[43]的计算则是一棵计算树:从叶子节点出发到根节点的过程, 每个非叶子节点的向量值被定义为:该节点的儿子节点所对应的向量值之和, 再加上一个规则向量.得到的模型可有效刻画计算语言学、逻辑、乃至XML等中的一些核心问题, 从而引起研究者的广泛重视.

Lazic^[44]和Demri^[45]分别研究了BVASS的可达性问题以及可覆盖性、有界性问题, 证明了前者是2-EXPSPACE-难的, 而后两个问题是2-EXPTIME-完备的.Lazic等人^{[46, 47]}进一步证明了一般BVASS可达性问题的下界甚至是Tower-hard, 也就是Non-elementary, 即, 任何验证算法不具有现实可行性.但非常有趣的是:与对维度不做限制时的高复杂性相比, 2016年, Gller等人证明了一维BVASS上的可达性、可覆盖以及有界性问题都是多项式时间完备的^[48].这些结果都表明, BVASS并非VASS的平凡扩展.

4.4 PND模型

PND模型是在Petri网中引入数据与数据操作的概念而为相关建模提供了便利, PND模型中, 每个place里不再是存储同样类型的token, 而是转为存储数据, 故而迁移规则相应地变为消耗和产生数据.关于PND, 比较集中的工作是Lazic^[49], Haddad^[50], Rosa-Velardo^[51]等人近年给出的一系列结论, 其中最重要的结论之一是证明了有序数据子模型上的可覆盖性问题是${F_{{\omega ^3}}}$ -完备的.PND研究的最新成果是关于无序数据模型(unordered data Petri nets, 简称UDPN)上可覆盖性问题的研究:2016年, Hofman等人利用Karp-Miller树的构造, 得出了一个超Ackermannian(hyper-Ackermannian)的算法上界^[52], 而此问题目前已知的最好下界是2017年Lazic等给出的Ackermannian-hard^[53].截至目前, PND模型相关问题的上下界之间仍有很大的差距, 这也是未来一个可能的研究方向.

研究展望:本节集中介绍了几个典型的VAS扩展模型, 并对这些模型上的验证问题做了较为简要的总结.这几个模型都具有理论或应用上的重要价值.从已有结论可以看出, 许多关于这些模型的验证问题都丞待解决.我们认为, 其中最值得关注的是:1维和2维PVAS可覆盖问题的上、下界、任意固定维度AVASS的验证问题的复杂性、2维BVASS的可达性问题的复杂性以及UDPN可达性问题的判定性.

5 本文总结

本文总结了加法向量系统验证领域的若干核心问题、最新进展和关键技术; 特别地, 指出了本领域中若干重要开放问题及部分结论的相互联系; 并对一些扩展模型和验证问题间的相互关系做了相应探讨, 提出了未来的研究方向.我们认为:向量加法系统是一个简洁而强大的数学模型, 无论从理论还是应用上而言, 对向量加法系统及其扩展模型上验证问题的深入研究都具有极重要的价值.最后, 作为对加法向量系统验证领域研究现状的小结, 我们将本领域最新结论总结在表 1中(注意, 这里用#表示开放问题).