程序分析是软件工程和形式化方法重要的研究领域之一, 人们在最初的程序分析中使用有限系统[1]作为程序模型, 它是由有限的状态集和在状态上有限的迁移规则组成.其表达能力十分有限, 无法对递归、并发等程序特征进行分析.对其扩展后可分别形成下推系统[2]和良结构迁移系统[3].前者给有限系统配备一个栈, 状态迁移的同时进行入栈、出栈操作, 方便建模单线程递归程序; 后者将状态集拓展到无限的良拟序集, 并保证迁移规则具有单调性.为了更好地描述和分析并发程序, Cai和Ogawa将二者结合, 提出良结构下推系统[4], 可以很方便地建模并发递归程序, 其具有强大的表达能力[5], 已经“很接近不可判定的边缘”[6].
我们通过一个自然数程序例子来说明这个模型:只用一个局部变量计算Ackermann函数A(2, n)的程序如图 1所示.并发程序对应多栈, 因此图灵等价, 是不可判定的.很多研究都对并发程序进行了限制, 比如在文献[7]中, 要求程序在函数调用时不能进行进程切换, 直到建模其行为的多重集下推系统栈空才行, 该模型就可被编码为良结构下推系统; 在文献[8]中, 针对用于建模程序的模型, 允许多栈但限制栈高, 也允许栈元素是多重集, 该模型也可以被编码成良结构下推系统.因此尽管并发后的程序相比单进程的程序, 相对应的良结构下推系统的可覆盖性问题的难度可能会上升, 但依旧满足我们提到的下界难度结论.由于我们后面证明的下界结论主要是针对单进程程序的执行, 所以这里不考虑并发性对结果的影响.Ackermann函数A(m, n)是著名的非原始递归函数, 其定义如下所示:
$ A(m, n) = \left\{ {\begin{array}{*{20}{l}} {n + 1, }&{{\mathop{\rm if}\nolimits} \;m = 0}\\ {A(m - 1, 1), }&{{\mathop{\rm if}\nolimits} \;n = 0}\\ {A(m - 1mA(m, n - 1)), }&{{\rm{otherwise}}} \end{array}} \right.. $ |
Ackermann函数是严格单调的.
图 1左侧为计算A(2, n)的程序, *是布尔表达式, 不确定地计算出true或false, 与WSPDS中不允许0测试(测试一个值是否为0)相一致.这段程序只要求第1个参数为固定参数, 主要是为了表明程序的局部变量可以被编码到相对应的良结构下推系统的栈字符集中, 为第4节栈字符为向量集的良结构下推系统可用于建模的相关程序提供一个直觉上的例子.该程序不能精确地计算出A(2, n), 但可以保证计算出的最大值是A(2, n).右侧为与程序对应的WSPDS, 状态对应于左侧程序的行号, 栈字符是函数名x∈{B0, B1, B2}和局部变量自然数x组成的序对.状态间的迁移描述了栈上的操作, 例如在状态3时的迁移(B2, x)→(B2, x-1)(B1, x)表示x≥1时, 将原栈顶(B2, x)替换成(B1, x)后压入(B2, x-1), 这种规则称为入栈规则.状态15到状态8的迁移依次弹出两个元素(B0, x)(B1, x′)后压入新栈顶(B1, x), 这种称为非标准的出栈规则.
递归的自然数程序可以被建模成良结构下推系统, 可将局部的自然数变量编码到栈向量, 可将全局的自然数变量编码到状态向量.用良结构下推系统的栈字符向量编码并发的递归程序的活动的进程数[9].因此, 递归程序的某一点是否可达可以转换成良结构下推系统的可覆盖性问题.
本文展示了基于重置0的证明模型的可覆盖性问题难度下界的通用方法, 所谓重置0是指直接对变量赋值为0.我们证明了一旦一个模型可以正向弱计算和反向弱计算一个函数f, 则其可覆盖性问题的难度的下界就是f难的.另外, 还证明了具有栈字符集为n维向量集的良结构下推系统的可覆盖性问题的下界是Hyper- Ackermann难的.并且利用本文提出的方法重新证明了具有状态集为三维自然数向量集的良结构下推系统的可覆盖性问题的下界是TOWER难的.
对于可覆盖性和可达性的复杂性证明有如下一些工作:Lipton给出最有名的向量加法系统的下界[10].证明了其可覆盖性问题和可达性问题是EXPSPACE的, 主要思想是用并行程序设置固定上界的计数器设置“精确地”0测试.Lazic[11]使用与Lipton相同的方法, 证明了状态为向量集的下推系统的可覆盖性问题的下界是TOWER难的, Schnoebelen等人的工作[12, 13]使用重置0的技巧, 证明了重置Petri网的可覆盖性问题是Ackermann难的, 也是本文借鉴使用的方法.在Schnoebelen等人的证明中, 重置Petri网的维度必须与要得到的其可覆盖性问题的难度Ackermann(m, n)中的参数m相关, 因此整个规约过程相对输入大小不是多项式的.但在良结构下推系统中, 因为有栈的存在, 保证了其可覆盖性问题下界的证明是多项式的, 且独立于参数的大小.Demri等人[14]证明了分支向量加法系统的可覆盖性问题是2EXPTIME完备的.Lazic[15]证明了分支向量加法系统的可达性问题是2EXPSPACE难的.Bonnet[16]证明了允许一个计数器用于0测试的向量加法系统的可达性问题是可判定的.不对称的带状态的向量加法系统的可达性问题是不可判定的[17-19], 但其自底向上的可覆盖性问题是Ackermann完备的[20].
本文第2节介绍后文将用到的一些基础符号和良结构下推系统、Hyper-Ackermann函数和2-计数机器的定义.第3节介绍证明可覆盖性问题的难度的一般性方法.第4节给出证明, 得出栈字符集为n维向量集的良结构下推系统的可覆盖性问题的下界是Hyper-Ackermann的.第5节采用本文提出的方法重新证明状态为向量集的下推系统的可覆盖性问题的下界是TOWER难的, 与Lazic[11]的结果一致.第6节总结全文, 并展望未来工作.
2 预备知识令
在迁移规则中使用→表示迁移关系.用
定义2.1. 一个良结构下推系统是一个三元组, 其中,
● P是有限的状态集, 或者给定一个具体的维度k, P=
● Γ是有限的栈字符集, 或者给定一个具体的维度d, Γ=
● Δ是有限的单调偏函数的集合:P×Γ≤2→P×Γ≤2.
单调性是指对p, q∈P, w, v∈Γ≤2, 若(p, w→q, v)∈Δ, 则对任意p′≥p, w′≫w, 有(p′, w′→q′, v′)∈Δ且q′≥q, v′≫v.这里,≫是≥在Γ*上的按位扩展, 即:a1a2...am≫b1b2…bn, 当且仅当对任意的i, ai≥bi且m=n.如果移除了单调性, 良结构下推系统就会变得图灵完备.
下推向量加法系统是栈字符集有限且状态集为k维自然数向量集的良结构下推系统, 即P=
良结构下推系统的格局
$ \frac{{(p, w \to q, v) \in \Delta }}{{\langle p, ww'\rangle \mapsto \langle q, vw'\rangle }}.$ |
给定初始格局c0=〈p, w〉和目标格局cf=〈q, v〉, 良结构下推系统的可达性问题是判断
例2.1:一个良结构下推系统
$ \Delta = \left\{ \begin{array}{l} {r_1}:p, \alpha \to p + 6, (\alpha - 6)(\alpha - 6), ~{\rm{ if }}~\alpha \ge 6\\ {r_{2}}:p, \varepsilon \to p - 6, 6, ~~~~~~~~~~~~~~~~~~~~~~{\rm{ if }}~p \ge 6 \end{array} \right..$ |
给定初始格局c0=〈6, 0〉, 则存在一个如下的格局迁移序列:
$ \langle 6, 0\rangle \mapsto \langle 0, 60\rangle \mapsto \langle 6, 000\rangle \mapsto \langle 0, 6000\rangle \mapsto \langle 6, 00000\rangle \mapsto ... $ |
可见, 格局〈6, 000〉是从初始格局可达的, 而格局〈0, 5000〉虽然不可达, 但可被覆盖.
2.2 Hyper-Ackermann函数康托尔在1883年提出了序数的概念[21], 引入了无限的序列.ω是最小的无限序数.按照康托尔正规式的表示方法, 每一个limit序数λ都可以被唯一地分解成
$ {\left( {{\omega ^{{d_1}}}.{c_1} + {\omega ^{{d_2}}}.{c_2} + ... + {\omega ^{{d_k}}}.{c_k}} \right)_n} = {\omega ^{{d_1}}}.{c_1} + ... + {\omega ^{{d_{k - 1}}}}.{c_{k - 1}} +\\ {\omega ^{{d_k}}}.\left( {{c_k} - 1} \right) + {\omega ^{{d_{k + 1}}}}.\left( {n + } \right.\left. 1 \right). $ |
定义2.2. Fast-Growing函数族按下标序数为a≤ωω索引定义如下[6]:
$ \begin{array}{l} {F_0}(n) = n + 1, \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;{F_{\alpha + 1}}(n) = F_\alpha ^{n + 1}(n) = \overbrace {{F_\alpha }({F_\alpha }(...{F_\alpha }(n)...))}^{n + 1}, \\ {F_\lambda }(n) = {F_{{\lambda _n}}}(n), \lambda < {\omega ^\omega }, \;\;\;\;\;{F_{{\omega ^\omega }}}(n) = {F_{{\omega ^{n + 1}}}}(n). \end{array}$ |
F1(n)是n的线性函数, F2(n)是n的指数函数,
例2.2:
$ \begin{array}{l} {F_{{\omega ^\omega }}}(3) &= {F_{{\omega ^4}}}(3)\\ ~~~~~~~~~~~~~{\rm{ }} &= {F_{{\omega ^3}.4}}(3)\\ ~~~~~~~~~~~~~{\rm{ }}& = {F_{({\omega ^3}.3 + {\omega ^2}.\left. 4 \right)}}(3) = {F_{({\omega ^3}.3 + {\omega ^2}.\left. {3 + \omega .4} \right)}}(3) = {F_{({\omega ^3}.3 + {\omega ^2}.\left. {3 + \omega .3 + 4} \right)}}(3)\\ ~~~~~~~~~~~~~{\rm{ }} &= {F_{\left( {{\omega ^3}.3 + {\omega ^2}.3 + \omega .3 + 3} \right)}}\left( {{F_{\left( {{\omega ^3}.3 + {\omega ^2}.3 + \omega .3 + 3} \right)}}\left( {{F_{\left( {{\omega ^3}.3 + {\omega ^2}.3 + \omega .3 + 3} \right)}}\\\left( {{F_{\left( {{\omega ^3}.3 + {\omega ^2}.3 + \omega .3 + 3} \right)}}\left( 3 \right)} \right)} \right)} \right)\\ ~~~~~~~~~~~~~{\rm{ }}& = ... \end{array}$ |
引理2.2. Hyper-Ackermann函数是严格单调的, 即对任何n′ > n,
定义2.3. 一个计数机器是一个三元组M=〈P, C, Δ〉, 其中, P是有限的状态集, C是有限的计数器的集合, Δ
$ op:: = {C_i} = 0?{\rm{ | }}{C_i} + + {\rm{ | }}{C_i} > 0?{C_i} - - $ |
计数机器的格局是一个序对〈p, n〉, 其中, p∈P表示当前的状态, n∈
● 若(p, Ci=0?, q)∈Δ且ni=0, 则m=n;
● 若(p, Ci++, q)∈Δ, 则mi=ni+1且对j≠i有mj=nj;
● 若(p, Ci > 0?Ci- -, q)∈Δ且ni > 0, 则mi=ni-1且对j≠i有mj=nj.
给定初始格局〈p0, 0〉和目标格局〈pf, 0〉, 计数机器的可达性问题是判断格局的执行序列
2-计数机器(只有2个计数器)是图灵完备的[22], 其可达性问题是不可判定的.然而, 如果给每个计数器设定一个上界, 即每个计数器的值不超过这个上界值, 则2-计数机器的计算能力就得到了限制, 其可达性问题就是可判定的.例如, 输入的大小为n, 上界值是
这里给定2-计数机器设定一个上界B, 使得在格局迁移的过程中所有的计数器的值的总和不超过上界, 记为
我们的证明技巧基于Schnoebelen等人在文献[12, 13]中提出的将Ackermann-bound的2-计数机器的可达性问题规约到重置Petri网的可覆盖性问题.本节不针对任何具体的模型, 只是给出具体的规约的思路:将以f(x)为界的2-计数机器的可达性问题规约到某个特定模型M的可覆盖性问题, 注意, 这里的f(x)应该是严格单调的函数.
简单来说, 规约由3部分构成.
● 输入为n, MH计算f(n)的值;
● Mb模拟以f(x)为界的2-计数机器;
●
MH根据输入向量n计算一个上界值B, 最大为f(n), 将这个值传递给Mb, 触发Mb的执行.Mb执行后, B的值可能会变小(错误的模拟)或保持不变(正确的模拟).然后将值传递给第3部分
3.1 有界的2-计数机器的模拟
给定2-计数机器M=〈P, C, Δ〉, 有界的2-计数机器
● 若op(C)=Ci++, 则对新状态s
$ \Delta ' = \Delta ' \cup \left\{ {\left( {p, b > 0?b - - , s} \right), \left( {s, {C_i} + + , q} \right)} \right\}$ |
● 若op(C)=Ci=0?, 则Δ′=Δ′
● 若op(C)=Ci > 0?Ci- -, 则对新状态s
$ \Delta ' = \Delta ' \cup \left\{ {\left( p \right., {C_i} > 0?{C_i} - - , \left. s \right), \left( s \right., b + + , \left. q \right)} \right\}.$ |
但是由于很多模型都没有测0能力, 因此本文使用重置0操作代替测0, 即将图 3中的i1=0?用i1=0来代替, 构造相应的模型Mb.Mb的构造如图 4所示.
注意, 在Mb中, i1+i2+b的和可能会变小, 虽然一旦对一个非0的计数器置0, 但却并未对有界计数器增加相应的数量.在Mb的格局迁移过程中, 如果i1=0从未执行或者仅仅执行在对一个值已经为0的变量上, 则所有计数器的和保持不变, Mb精确地模仿了
引理3.1.
● 如果
● 如果Mb中存在
函数f(n)的定义域为k维的自然数向量n, 且严格单调, 即对任意i∈[1...k], 若
$ f\left( {{n_1}, ..., {{n'}_i}, ..., {n_k}} \right) > f\left( {{n_1}, ..., {n_i}, ..., {n_k}} \right).$ |
因为我们要研究的模型不是图灵完备的, f(n)的正向和逆向计算可能不精确, 但这并不影响我们的结论, 因为Mb的格局迁移中不会增大f(n)的值.因此, 如果MH计算出的上界值B不大于f(n), 则经过Mb后, B依旧不大于f(n),
定义3.2. 给定输入n, 如果MH计算出的最大的值为f(n), 则称MH弱计算函数f(n).
给定输入B′, 设
● 若f(n)=B′, 则n∈S;
● 若n∈S, 则f(n)≤B′,
则称
如图 2所示, 模型M的格局的迁移由MH、Mb、
定理3. f是严格单调的k元函数.MH弱计算函数f(n)
● 若在
● 若
证明:
● 在
● 若
本节考虑良结构下推系统的子模型:状态为有限集而栈字符为向量, 即
给定一个良结构下推系统Mr=〈{● },
$ \Delta = \left\{ \begin{array}{l} {r_1}:\left( {{k_n}, {k_{n - 1}}, ..., {k_0}, t, x} \right) \to\\ \left( {{k_n}, {k_{n - 1}}, ..., {k_0} - 1, x, x} \right)\\ {r_2}:\left( {{k_n}, {k_{n - 1}}, ..., {k_0}, t, x} \right) \to\\ \left( {{k_n}, {k_{n - 1}}, ..., {k_0}, 0, x} \right)\left( {{k_n}, {k_{n - 1}}, ..., {k_0}, t - 1, x} \right)\\ {r_3}:\left( {\underbrace {{k_n}, {k_{n - 1}}, ..., {k_i}, ..., 0}_{n + 1}, 0, x} \right) \to \\\left( {\underbrace {{k_n}, {k_{n - 1}}, ..., {k_i} - 1, x + 1, ..., 0}_{n + 1}, 0, x} \right), i \in \left[ {1, n} \right]\\ {r_4}:\left( {\underbrace {0, 0, ..., 0}_{n + 1}, 0, x} \right)\left( {{{k'}_n}, {{k'}_{n - 1}}, ..., {{k'}_0}, t', x'} \right) \to \\\left( {k', {{k'}_{n - 1}}, ..., k', t', x + 1} \right) \end{array} \right.. $ |
按照迁移规则中所示, 栈向量的前n+1个分量都标记了下标, 例如k0就表示该向量的从左向右第n+1个分量.以下描述都直接使用这一表示方法.规则r1对栈顶元素进行在某些分量上值的修改; r2将栈顶元素的第n+1个分量进行修改并压入新向量(kn, kn-1, …, 0, x); r3表示当i在[1, n]区间内(含两端)时, 都可执行r3的迁移; r4表示当栈顶的前n+2个分量都是0时, 可执行出栈操作, 并将最后一个分量值传递给栈顶的下一个元素, 形成新的栈顶.注意, 每条迁移规则都代表单调函数, 例如对r4, 任何向量只要其所有分量值均不小于0, 都有此迁移, 即
$ \left( {{p_n}, {p_{n - 1}}, ..., {p_0}, te, xp} \right)\left( {{{k'}_n}, {{k'}_{n - 1}}, ..., {{k'}_0}, t', x'} \right) \to \left( {{{k'}_n}, {{k'}_{n - 1}}, ..., {{k'}_0}, t', xp + 1} \right). $ |
这里写r4只是方便理解.
引理4.1. Mr可弱计算Hyper-Ackermann函数, 且
$ hyper(n) = \max \left\{ {x + 1{\rm{ }}|{\rm{ }}\left\langle { \bullet , {\rm{ }}\left( {\underbrace {n + 1, 0, ..., 0}_{n + 1}, 0, n} \right) \bot } \right\rangle {\rm{ }}{ \mapsto ^ * }\\{\rm{ }}\left\langle { \bullet {\rm{, }}\left( {\underbrace {0, 0, ..., 0}_{n + 1}, 0, x} \right) \bot } \right\rangle {\rm{ }}} \right\}, $ |
其中,
证明:首先, 因为如定义2.2所示, 给定参数n后, Hyper-Ackermann函数没有升幂操作(除了一开始的
其次, 栈顶元素可分为以下3类.
(1) 栈顶为(kn, kn-1, …, k0, t, x)形式, 对应接下来需要计算的Hyper-Ackermann函数为
(2) 栈顶为
(3) 栈顶为
但是, 因为Mr的迁移规则具有单调性, 相比正确的格局迁移, 可能存在错误的格局迁移, 如应使用r3却使用了r4, 表明
例4.1:利用引理4.1计算
$ \begin{array}{l} \left( {2, 0, 0, 1} \right) \bot \mathop \mapsto \limits^{{r_3}} \left( {1, 2, 0, 1} \right) \bot \mathop \mapsto \limits^{{r_1}} \left( {1, 1, 1, 1} \right) \bot \mathop \mapsto \limits^{{r_2}} \left( {1, 1, 0, 1} \right)\left( {1, 1, 0, 1} \right) \\\bot \mathop \mapsto \limits^{{r_1}} \left( {1, 0, 1, 1} \right)\left( {1, 1, 0, 1} \right) \bot \\ \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\mathop \mapsto \limits^{{r_2}} \left( {1, 0, 0, 1} \right)\left( {1, 0, 0, 1} \right)\left( {1, 1, 0, 1} \right) \\\bot \mathop \mapsto \limits^{{r_3}} \left( {0, 2, 0, 1} \right)\left( {1, 0, 0, 1} \right)\left( {1, 1, 0, 1} \right)\\ \bot \mathop \mapsto \limits^{{r_1}} \left( {0, 1, 1, 1} \right)\left( {1, 0, 0, 1} \right)\left( {1, 1, 0, 1} \right) \bot \\ \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\mathop \mapsto \limits^{{r_2}} \left( {0, 1, 0, 1} \right)\left( {0, 1, 0, 1} \right)\left( {1, 0, 0, 1} \right)\left( {1, 1, 0, 1} \right) \\\bot \mathop \mapsto \limits^{{\rm{ }}{r_1}} \left( {0, 0, 1, 1} \right)\left( {0, 1, 0, 1} \right)\left( {1, 0, 0, 1} \right)\left( {1, 1, 0, 1} \right) \bot\\ \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\mathop \mapsto \limits^{{r_2}} \left( {0, 0, 0, 1} \right)\left( {0, 0, 0, 1} \right)\left( {0, 1, 0, 1} \right)\left( {1, 0, 0, 1} \right)\left( {1, 1, 0, 1} \right)\\ \bot \mathop \mapsto \limits^{{r_4}} \left( {0, 0, 0, 2} \right)\left( {0, 1, 0, 1} \right)\left( {1, 0, 0, 1} \right)\left( {1, 1, 0, 1} \right) \bot \\ \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\mathop \mapsto \limits^{{r_4}} \left( {0, 1, 0, 3} \right)\left( {1, 0, 0, 1} \right)\left( {1, 1, 0, 1} \right) \\\bot \mathop \mapsto \limits^{{r_1}} \left( {0, 0, 3, 3} \right)\left( {1, 0, 0, 1} \right)\left( {1, 1, 0, 1} \right) \bot \\ \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\mathop \mapsto \limits^{{r_2}} \left( {0, 0, 0, 3} \right)\left( {0, 0, 2, 3} \right)\left( {1, 0, 0, 1} \right)\left( {1, 1, 0, 1} \right) \\\bot \mathop \mapsto \limits^{{r_4}} \left( {0, 0, 2, 4} \right)\left( {1, 0, 0, 1} \right)\left( {1, 1, 0, 1} \right) \bot \\ \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\mathop \mapsto \limits^{{r_2}} \left( {0, 0, 0, 4} \right)\left( {0, 0, 1, 4} \right)\left( {1, 0, 0, 1} \right)\left( {1, 1, 0, 1} \right)\\ \bot \mathop \mapsto \limits^{{r_4}} \left( {0, 0, 1, 5} \right)\left( {1, 0, 0, 1} \right)\left( {1, 1, 0, 1} \right) \bot \\ \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\mathop \mapsto \limits^{{\rm{ }}{r_2}} \left( {0, 0, 0, 5} \right)\left( {0, 0, 0, 5} \right)\left( {1, 0, 0, 1} \right)\left( {1, 1, 0, 1} \right) \\\bot \mathop \mapsto \limits^{{r_4}} \left( {0, 0, 0, 6} \right)\left( {1, 0, 0, 1} \right)\left( {1, 1, 0, 1} \right) \bot \\ \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\mathop \mapsto \limits^{{r_4}} \left( {1, 0, 0, 7} \right)\left( {1, 1, 0, 1} \right)\\ \bot \mathop \mapsto \limits^{{\rm{ }}{r_3}} \left( {0, 8, 0, 7} \right)\left( {1, 1, 0, 1} \right)\\ \bot \mathop \mapsto \limits^{{r_1}} \left( {0, 7, 7, 7} \right)\left( {1, 1, 0, 1} \right) \bot \mathop \mapsto \limits^{{r_2}} ... \end{array} $ |
最后的(0, 7, 7, 7)(1, 1, 0, 1)表示
如果仅仅把Mr的迁移规则逆过来, 就构造了逆向弱计算Hyper-Ackermann值对应参数的良结构下推系统
引理4.2.
定理4. 给定特定的良结构下推系统, 其状态集有限, 栈字符集为n+3维的良拟序集, 则其可覆盖性问题的下界是Hyper-Ackerman难的.
证明:因为重置0操作是单调的, n+3维的良结构下推系统可以作为Mb.Mb, Mr和
本节考虑良结构下推系统的子模型:状态为向量而栈字符为有限集, 即
给定一个良结构下推系统
引理5.1. Mp可弱计算
$ \underbrace {{2^2}^{^{{ {\mathinner{\mkern2mu\raise1pt\hbox{.}\mkern2mu \raise4pt\hbox{.}\mkern2mu\raise7pt\hbox{.}\mkern1mu}} ^2}}}}_n = \left\{ \begin{array}{l} \max \left\{ {x\left| {\left\langle {\left( {1, 0, 2} \right), \underbrace {aa...a}_{n - 2} \bot } \right\rangle { \mapsto ^ * }\left\langle {\left( {0, 0, x} \right), \bot } \right\rangle } \right.} \right\}{\rm{, }}~n \ge {\rm{2}}\\ 2, ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~n = 1 \end{array} \right., $ |
其中,
证明:对格局〈(n, t, x), ω
● 当n=1时显然成立;
● 当n=2时, tower(2)=22=4.对Mp有如下格局迁移序列:
● 假设n=k时题设成立, 则有
$ \begin{array}{l} \langle \left( {0, 0, x} \right), a \bot \rangle \mathop \mapsto \limits^{{r_3}} \langle \left( {x - 1, 0, 2} \right), \bot \rangle \mathop \mapsto \limits^{{r_1}} \langle \left( {x - 2, 2, 2} \right), \bot \rangle \mathop \mapsto \limits^{{r_2}} \mathop \mapsto \limits^{{r_2}} \langle \left( {x - 2, 0, 4} \right), \bot \rangle \mathop \mapsto \limits^{{r_1}} \\\mathop \mapsto \limits^{{r_2}} \mathop \mapsto \limits^{{r_2}} \mathop \mapsto \limits^{{r_2}} \mathop \mapsto \limits^{{r_2}} \langle \left( {x - 3, 0, 8} \right), \bot \rangle \\ \mathop \mapsto \limits^{{r_1}} \underbrace {\mathop { \mapsto ...}\limits^{{r_2}} \mathop \mapsto \limits^{{r_2}} }_8\langle \left( {x - 4, 0, 16} \right), \bot \rangle \mathop \mapsto \limits^{{r_1}} \underbrace {\mathop { \mapsto ...}\limits^{{r_2}} \mathop \mapsto \limits^{{r_2}} }_{16}...\mathop \mapsto \limits^{{r_1}} \\\underbrace {\mathop { \mapsto ...}\limits^{{r_2}} \mathop \mapsto \limits^{{r_2}} }_{{2^{\left( {x - 1} \right)}}}\langle \left( {0, 0, 2 \times {2^{\left( {x - 1} \right)}}} \right), \bot \rangle = \langle \left( {0, 0, {2^x}} \right), \bot \rangle , \end{array} $ |
对应的tower(k+1)的值是
但是, 因为Mp的迁移规则具有单调性, 相比正确的格局迁移, 可能存在如下情况的错误的格局迁移, 造成数据丢失.
● 当n > 0, t > 0时, 用了r1而不是r2, 即x+t被认为是x进行后续计算.
● 当n > 0, t > 0时, 用了r3而不是r2, 即(x+t)×2n被认为是x进行后续计算.
● 当n=0, t > 0时, 用了r3而不是r2, 即x+t被认为是x进行后续计算.
● 当n > 0, t=0时, 用了r3而不是r1, 即x×2n被认为是x进行后续计算.
如果在格局迁移过程中没有任何的数据丢失, 则当格局处于〈(0, 0, x),
例5.1:利用引理5.1计算
$ \begin{array}{l} \langle \left( {1, 0, 2} \right), a \bot \rangle \mathop \mapsto \limits^{{r_1}} \langle \left( {0, 2, 2} \right), a \bot \rangle \mathop \mapsto \limits^{{r_2}} \mathop \mapsto \limits^{{r_2}} \langle \left( {0, 0, 4} \right), a \bot \rangle \mathop \mapsto \limits^{{r_3}} \langle \left( {3, 0, 2} \right), \bot \rangle \\ \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\mathop \mapsto \limits^{{r_1}} \langle \left( {2, 2, 2} \right), \bot \rangle \mathop \mapsto \limits^{{r_2}} \mathop \mapsto \limits^{{r_2}} \langle \left( {2, 0, 4} \right), \bot \rangle \mathop \mapsto \limits^{{r_1}} \langle \left( {1, 4, 4} \right), \bot \rangle \\ \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\mathop \mapsto \limits^{{r_2}} \mathop \mapsto \limits^{{r_2}} \mathop \mapsto \limits^{{r_2}} \mathop \mapsto \limits^{{r_2}} \langle \left( {1, 0, 8} \right), \bot \rangle \mathop \mapsto \limits^{{r_1}} \langle \left( {0, 8, 8} \right), \bot \rangle \underbrace {\mathop \mapsto \limits^{{r_2}} \mathop \mapsto \limits^{{r_2}} ...\mathop \mapsto \limits^{{r_2}} }_8\langle \left( {0, 0, 16} \right), \bot \rangle . \end{array} $ |
因此,
如果仅仅把Mp的迁移规则逆过来, 就构造了逆向弱计算
引理5.2.
定理5. 给定特定的良结构下推系统, 其状态集为三维的良拟序集, 栈字符集有限, 即三维的下推向量加法系统, 其可覆盖性问题的下界是TOWER难的.
证明:类似定理4的证明.因三维下推向量加法系统可以模拟Mb.所以, 由定理3可得, 其可覆盖性问题的下界是TOWER难的.证毕.
6 总结以及未来的工作本文基于良结构下推系统, 采用重置0操作, 提出了一种证明模型的下界的通用方法, 证明了n维的良结构下推系统的可覆盖性问题的下界是Hyper-Ackermann难的, 还将其与程序中的全局变量或局部变量的个数相对应, 表明了有n个局部变量的程序的可达性分析问题是很难的, 为分析含无限定义域的变量(如整数域)的程序时采取重置0操作持否定态度, 鼓励将无限定义域限制在有限定义域处理.本文还重新证明了下推向量加法系统在三维情况下其可覆盖性问题就可达到TOWER难.
未来希望能够推广这种证明模型可覆盖性难度下界的方法, 探索更多向量加法系统的拓展模型的下界或比已知下界更高的下界.同时, 寻求证明良结构下推系统的可覆盖性问题难度的上界, 形成证明上界的一般性方法并进行对其他模型的应用推广.再进一步探究良结构下推系统的可覆盖性问题的判定性.
[1] |
Derick WD. Theory of Computation:A Primer. Boston: Addison-Wesley Longman Publishing Co, 1987.
|
[2] |
Autebert JM, Berstel J, Boasson L. Context-Free languages and pushdown automata. Handbook of Formal Languages, 1997, 6(3): 111–174.
[doi:10.1007/978-3-642-59136-5_3] |
[3] |
Abdulla PA, Čerāns K, Jonsson B, Tsay YK. Algorithmic analysis of programs with well quasi-ordered domains. Information and Computation, 2000, 160(1-2): 109–127.
[doi:10.1006/inco.1999.2843] |
[4] |
Cai X, Ogawa M. Well-Structured pushdown systems. In: D'Argenio PR, Melgratti H, eds. Proc. of the Int'l Conf. on Concurrency Theory. Berlin: Springer-Verlag, 2013. 121-136.[doi: 10.1007/978-3-642-40184-8_10] |
[5] |
Jin Y, Cai XJ, Li GQ. Expressiveness of well-structured pushdown systems. Journal of Shanghai Jiaotong University, 2015, 49(8): 1084–1089.
[doi:10.16183/j.cnki.jsjtu.2015.08.002] |
[6] |
Leroux J, Praveen M, Sutre G. Hyper-Ackermannian bounds for pushdown vector addition systems. In: Henzinger T, Miller D, eds. Proc. of the Joint Meeting of the 23rd EACSL Annual Conf. on Computer Science Logic (CSL) and the 29th Annual ACM/IEEE Symp. on Logic in Computer Science (LICS). New York: ACM, 2014. Article 63.[doi: 10.1145/2603088.2603146] |
[7] |
Sen K, Viswanathan M. Model checking multithreaded programs with asynchronous atomic methods. In: Ball T, Jones RB, eds. Proc. of the Int'l Conf. on Computer Aided Verification. Berlin: Springer-Verlag, 2006. 300-314.[doi: 10.1007/11817963_29] |
[8] |
Kochems J, Luke Ong CH. Safety verification of asynchronous pushdown systems with shaped stacks. In: D'Argenio PR, Melgratti H, eds. Proc. of the Int'l Conf. on Concurrency Theory. Berlin: Springer-Verlag, 2013. 288-302.[doi: 10.1007/978-3-642-40184-8_21] |
[9] |
Bouajjani A, Emmi M. Analysis of recursively parallel programs. In: Field J, ed. Proc. of the 39th Annual ACM SIGPLANSIGACT Symp. on Principles of Programming Languages. New York: ACM, 2012. 203-214.[doi: 10.1145/2103621.2103681] |
[10] |
Lipton RJ. The reachability problem requires exponential space[Ph.D. Thesis]. Department of Computer Science, Yale University, 1976. |
[11] |
Lazic R. The reachability problem for vector addition systems with a stack is not elementary. Computer Science, 2013.
https://www.researchgate.net/publication/257410098_The_reachability_problem_for_vector_addition_systems_with_a_stack_is_not_elementary |
[12] |
Schnoebelen P. Revisiting Ackermann-Hardness for lossy counter machines and reset Petri nets. Lecture Notes in Computer Science, 2010, 6281: 616–628.
[doi:10.1007/978-3-642-15155-2_54] |
[13] |
Haddad S, Schmitz S, Schnoebelen P. The ordinal-recursive complexity of timed-arc Petri nets, data nets, and other enriched nets. In: Logic in Computer Science. IEEE, 2012. 355-364.[doi: 10.1109/LICS.2012.46] |
[14] |
Demri S, Jurdziński M, Lachish O, Lazić R. The covering and boundedness problems for branching vector addition systems. Journal of Computer and System Sciences, 2013, 79(1): 23–38.
[doi:10.1016/j.jcss.2012.04.002] |
[15] |
Lazić R. The reachability problem for branching vector addition systems requires doubly-exponential space. Information Processing Letters, 2010, 110(17): 740–745.
[doi:10.1016/j.ipl.2010.06.008] |
[16] |
Bonnet R. The reachability problem for vector addition system with one zero-test. In: Murlak F, Sankowski P, eds. Mathematical Foundations of Computer Science. Berlin: Springer-Verlag, 2011. 145-157.[doi: 10.1007/978-3-642-22993-0_16] |
[17] |
Lincoln P, Mitchell J, Scedrov A, Shankar N. Decision problems for propositional linear logic. Annals of Pure and Applied Logic, 1992, 56(1-3): 239–311.
[doi:10.1016/0168-0072(92)90075-B] |
[18] |
Kanovich MI. Petri nets, Horn programs, linear logic, and vector games. Annals of Pure and Applied Logic, 1995, 75(1-2): 107–135.
[doi:10.1016/0168-0072(94)00060-G] |
[19] |
Raskin JF, Samuelides M, Begin LV. Games for counting abstractions. Electronic Notes in Theoretical Computer Science, 2005, 128(6): 69–85.
[doi:10.1016/j.entcs.2005.04.005] |
[20] |
Urquhart A. The complexity of decision procedures in relevance logic Ⅱ. The Journal of Symbolic Logic, 1999, 64(4): 1774–1802.
[doi:10.2307/2586811] |
[21] |
Cantor G. Ueber unendliche, lineare Punktmannichfaltigkeiten. Mathematische Annalen, 1883, 21(4): 545–591.
[doi:10.1007/BF01446819] |
[22] |
Minsky ML. Computation:Finite and Infinite Machines. Prentice-Hall, Inc., 1967. |
[23] |
Schmitz S, Schnoebelen P. The power of well-structured systems. In: D'Argenio PR, Melgratti H, eds. Proc. of the Int'l Conf. on Concurrency Theory. Berlin: Springer-Verlag, 2013. 5-24.[doi: 10.1007/978-3-642-40184-8_2] |