随着大规模复杂计算机系统的广泛使用, 并发程序得到了越来越多的应用.编写一段正确高效的并发程序十分困难, 而验证一段并发程序则更加困难.近年来, 许多学者提出了针对并发程序的验证技术^[1-5].其中, Petri网(Petri net)^[6]是一种简明且自然的用于描述和分析并发程序的模型, 它可以模拟具有无穷进程的程序.具体地说, 我们可以使用Petri网的库所p(place)表示程序的位置l(location), 用p的令牌(token)数表示当前运行至l的进程数量.然而, 传统的并发程序验证使用Petri网建模, 会使验证的复杂性太高.例如, 在并发程序的验证中, 活性(liveness)是一类值得关注的性质, 其表示“好事情最终总会发生”, 例如程序最终会终止、如果事件X发生则事件Y最终也会发生等等.如果我们用递归时序逻辑(recursive temporal logic)^[7]表达活性, 那么异步程序的活性问题被归约为Petri网的可达性(reachability)问题上^[8].然而Petri网的可达性问题最近被证明是Tower难的^[9], 因此不可能存在高效的验证工具.我们发现, 一些异步并发程序可以通过使用Petri网的一个子类——基本并行进程(basic parallel process, 简称BPP)^[10]进行建模, 使得对并发程序验证的复杂性大为降低.例如, BPP的可达性问题是NP完备的^[11], 因此我们可以对一类并发程序的活性问题进行验证.BPP是一个由Søren Christensen提出的针对并发的无穷状态模型, 在BPP中, 一个进程被建模为一个符号, 程序的状态被建模为符号的并行组合, 而规则表示着进程的迁移方式.一个符号能够通过迁移产生更多的符号, 因此BPP生成的是一个无穷状态系统.由于BPP的迁移语义是异步的, 因此BPP可被视为非交互式Petri网(communication-free Petri net), 即Petri网的一个子类.事实上, BPP的进程符号X对应着Petri网的库所p, 一个BPP表达式α对应着Petri网的标记M(marking), 而α中X出现的次数对应着库所p内令牌的数目.

我们用一个程序的例子说明如何使用BPP为并发程序建模.表 1程序中的cobegin和coend表示创建多个进程, 其中, 主程序在等待请求, 如果没有收到请求, 则创建两个进程用于打印信息和等待; 否则, 同样创建两个进程, 一个进程根据请求的内容向文件写进相关信息, 而另一个进程用于继续检测请求.我们可以用符号集为{S, T, P, W}的BPP来表示该程序, 其包含以下规则.

$ \begin{array}{*{20}{l}} {S\mathop \to \limits^v T, }\\ {T\mathop \to \limits^u PT, }\\ {T\mathop \to \limits^u WS.} \end{array} $

其中, ${S\mathop \to \limits^v T}$表示程序由detect()进入wait(), 而${T\mathop \to \limits^u PT}$和${T\mathop \to \limits^u WS}$分别对应程序根据请求数目的不同行为.符号T有两种迁移方式, 分别对应着请求数量为0和不为0的情况.若没有收到请求, 则迁移到含有PT的状态; 否则, 迁移到包含进程WS的状态.

并发程序验证的一个重要的手段是对并发模型进行模型检测.一个模型检测问题是指在一个模型下, 给定一个模型中的状态s以及一个逻辑公式φ, 要求检测状态s是否满足公式φ, 其形式化的表示为s⊨φ.若给定的模型是BPP, 则状态空间为BPP表达式构成的集合.逻辑公式φ则表示待验证的性质.根据需要验证的性质, 我们选取合适的逻辑进行模型检测.对于分支时间时序逻辑, 我们常用算子AF来表示活性.逻辑公式AFφ表达的是从当前的状态出发, 性质φ最终会被满足.在本文, 我们研究的逻辑是EG逻辑^[12].EG逻辑由Esparza提出, 是一种在Hennessy-Milner Logic(HML)的基础上增加EG算子的分支时间时序逻辑, 其包含了常见的命题逻辑公式以及时序逻辑公式E < a > φ和EGφ, 其中, E < a > φ表示的是存在通过动作a可以到达的满足性质φ的状态; 而EG是AF的对偶算子, 即AF可以用﹁EG﹁表示.因此, EG逻辑是一种能够表达活性的逻辑.例如, s⊨AF(X≥1)表示从BPP状态s出发, 最终会到达一个进程X数量至少为1的状态.

在文献[12]中, Esparza证明了基于BPP的EG逻辑的模型检测问题是不可判定的.因此在标准语义下, 我们无法对BPP的活性进行模型检测.值得注意的是, 一个BPP和一个作为初始状态的BPP表达式生成的标签迁移系统可能会含有无穷长但不包含循环的路径, 这导致了BPP状态的进程符号数量会不断增加.然而在现实中, 大部分的程序都会在有穷步内终止, 因此状态的进程数量不会出现趋于无穷的情况, 而进程的迁移行为也会在一定步数内停止.

基于上述观察, 本文给出了基于BPP的EG逻辑的限界模型检测方法, 将BPP上EG逻辑的限界模型检测问题转化为线性整数算术公式的可满足性问题.本文的思路如下.

●  我们首先给出基于BPP的EG逻辑的k步限界语义s⊨_kφ.

●  接着, 根据BPP(V, Δ)的模型结构、初始的BPP状态s以及表示特定性质的EG逻辑公式φ, 给出对应的基于线性整数算术公式的刻画.具体地说, 定义了原子约束、迁移约束和路径约束等相应的约束, 并根据k步限界语义的定义给出了生成线性整数算术公式的算法.由于BPP从某个状态出发, 其路径可能有无限条, 因此我们并不能使用主流的具有门限定理的限界模型检测编码来给BPP上的EG进行编码.同时, 由于路径长度是作为参数进行输入, 并且BPP具有以上所说的特性而并非如Kripke结构的有穷模型, 因此在对公式EGφ进行SMT编码时, 不含有检测loop的相应约束条件.

●  最后, 将编码的线性整数算术公式作为SMT求解器的输入进行求解.若求解的结果为公式可满足, 则说明性质在k步内成立; 若不可满足, 则说明性质在k步内不成立.

例如, 对于表 1程序对应的BPP, 如果我们希望检测, 在2步之内, 从只包含detect()的进程的状态出发, 是否存在一条路径, 对于该路径上的每一个状态, 若写文件的进程数至少为1则用于detect()的进程数也至少为1, 那么我们可以用BPP状态s=S, 步长k=2, EG逻辑公式φ=EG(W≥1→S≥1)作为输入, 构造出对应的线性整数算术公式.用SMT求解器进行求解, 得到的结果是可满足, 因此待检测性质成立.

本文第1节介绍用到的一些基础知识, 包括用到的一些基础符号、标签迁移系统、基本并行进程、EG逻辑和线性整数算术的严格定义以及对SMT求解技术的简介.第2节对BPP上EG逻辑的模型检测问题的不可判定性进行分析, 并给出了EG逻辑的限界语义.第3节给出了BPP上EG逻辑限界模型检测问题的基于线性整数算术公式的刻画.第4节展示工具的实现及实验结果的分析.第5节介绍基本并行进程研究的一些相关工作.第6节是对全文的总结和未来工作的展望.

1 预备知识

令Var={X, Y, Z, …}为一个可数符号集, Act={a, b, c, …}为一个可数动作集.

令S为一集合, ⊗为一个二元运算S×S→S.如果以下3个条件成立.

1)   封闭性:若a∈S且b∈S则a⊗b∈S.

2)   结合律:对任意a, b, c∈S, (a⊗b)⊗c=a⊗(b⊗c)成立.

3)   存在单位元:存在e∈S, 使得对任意a∈S, a⊗e=e⊗a成立.

则称(S, ⊗)是一个幺半群(monoid).一般我们也直接称S为一个幺半群.令C为一集合, 则由C中元素构成的一个有穷序列称为C上的一个字(word).由集合C生成的自由幺半群(free monoid)指的是幺半群(C^*, concat), 其中, C^*是由C上的字组成的集合, 二元运算concat是字的串接(concatenation)操作.空字ε为自由幺半群的单位元.若我们规定串接运算满足交换律, 即对任意字x, y∈C^*, xy=yx成立, 则由集合C生成的自由幺半群称为自由交换幺半群(free communicative monoid), 记作C^⊕.

1.1 标签迁移系统

定义 1(标签迁移系统).一个标签迁移系统(labelled transition system)可以用一个四元组(S, A, →, r)表示, 其中, S是状态的集合, A是动作(action)的集合, →⊆S×A×S表示迁移关系, r表示初始状态.一般我们将关系集→中的元素(s, a, t)写作${s\mathop \to \limits^a t}$, 表示系统中状态间通过动作的迁移.标签迁移系统的一个路径(path)指的是一个无穷序列s₀, s₁, s₂, …, 使得${{s_0}\mathop \to \limits^{{a_0}} {s_1}\mathop \to \limits^{{a_1}} {s_2} \cdots }$, 或者是一个有穷序列s₀, s₁, …, s_n, 使得${{s_0}\mathop \to \limits^{{a_0}} \ldots \mathop \to \limits^{{a_{n - 1}}} {s_n}}$且s_n没有后继状态.在本文, 若不加说明, 则π表示一条路径, π(i)(其中, i≥0)表示路径的第i个状态.

1.2 Petri网

由于BPP是Petri网的一个子类, 因此我们首先引入Petri网的定义.

定义 2(Petri网).一个网N是一个三元组(S, T, W), 其中, S和T是不相交的有穷集合, W:(S×T)∪(T×S)→$\mathbb{N}$是权值函数.集合S和T中的元素分别称为库所和迁移.网N的一个标记是一个映射M:S→$\mathbb{N}$.一个Petri网是一个二元组(N, M₀), 其中, N是一个网, M₀是N的一个标记.

定义 3(非交互式Petri网).给定一个网N=(S, T, W).对于x∈S∪T, 记^●x为集合{y|W(y, x) > 0}, x^●为集合{y| W(x, y) > 0}.如果对于任意t∈T, |^●t|=1, 且对于任意s∈S, t∈T, W(s, t)≤1, 则称网N为非交互式网.给定一个Petri网(N, M₀), 如果N为非交互式网, 则称该Petri网为非交互式Petri网.

1.3 基本并行进程

在原始的定义中, 一个BPP表达式由进程变量通过动作前缀(action prefix)、选择(choice)和结合(merge)运算构成, 这些运算分别表示进程的迁移、进程对迁移的选择和进程的并行组合.BPP则定义为一族递归等式{X_i=E_i|1≤i≤n}, 其中, X_i为进程变量, E_i是只包含变量{X₁, …, X_n}的BPP表达式.在本文, 我们采用如下更为简洁的等价定义^[13], 这种定义实际上是将BPP视为交换上下文无关语法(commutative context-free grammar).

定义 4(基本并行进程).一个基本并行进程BPP是一个二元组(V, Δ), 其中V⊆Var是一个有穷符号集, Δ是一个由规则组成的有穷集合.Δ中的规则的形式为

$ {X\mathop \to \limits^a \alpha }, $

其中, X∈V, a∈Act, α∈V^⊕.其中, V^⊕是由V生成的自由交换幺半群.在本文, 我们称V^⊕中的元素为BPP表达式, 用小写希腊字母α, β, γ等表示.

由一个BPP(V, Δ)和一个BPP表达式α, 我们可以定义标签迁移系统(V^⊕, Act, →, α), 即状态空间为V^⊕, 初始状态为α.其中, 迁移关系→由以下规则生成.

$ {\frac{{X\mathop \to \limits^a \alpha \in \varDelta }}{{\beta X\gamma \mathop \to \limits^a \beta \alpha \gamma }}.} $

我们记→^*为一步迁移关系${{{\{ \mathop \to \limits^a \} }_{a \in Act}}}$的自反传递闭包(reflexive transitive closure), 则α→^*β表示状态α经过若干(可能为0)次迁移后到达状态β.

因为V^⊕是由V生成的自由交换幺半群, 因此BPP表达式具有模交换性(modulo commutativity), 即表达式中的符号元素可以交换位置.例如, XYZ, XZY, YXZ, YZX, ZXY和ZYX这6个表达式都被视为同一个表达式.从直观上看, BPP表达式由符号并行地组合而成, 每个符号都能根据相应的迁移规则各自独立地完成迁移.

BPP限定了每次迁移由单个进程触发, 其对应非交互式Petri网.给定一个BPP(V, Δ)和一个BPP表达式β, 其可以转换为一个与其同构的非交互式Petri网.我们用α(X)表示符号X在BPP表达式α中出现的次数.符号集V中的每个符号转换为Petri网的一个库所, 即符号集转换为Petri网的库所集.对于Δ中的每条规则${X\mathop \to \limits^a \alpha }$, 动作a转换为Petri网的一个迁移, 并添加一条从X到a的权值为1的边; 而对于每个α中的符号Y, 添加一条从a到Y的权值为α(Y)的边.非交互式Petri网中的标记M₀则定义为M₀(X)=β(X).图 1展示了从BPP({X, Y}, Δ)转换到对应的非交互式网的例子.

如果初始状态β为X, 则对应的非交互式Petri网中的标记M₀:{X, Y}→$\mathbb{N}$定义为:M₀(X)=1, M₀(Y)=0.

1.4 EG逻辑

定义 5(EG逻辑的语法). EG逻辑的语法如下.

$ {\varphi : = {\rm{true}} |\neg \varphi |\varphi \wedge \varphi |E\langle a\rangle \varphi |EG\varphi , } $

其中a∈Act.

定义 6(EG逻辑的语义).令s为状态空间V^⊕中的一个状态(即一个BPP表达式), φ是一个EG逻辑公式, 则基于BPP的EG逻辑的语义可以如下归纳定义.

●  s⊨true永远成立;

●  s⊨﹁φ当且仅当s⊨φ不成立;

●  s⊨φ₁∧φ₂当且仅当s⊨φ₁且s⊨φ₂;

●  s⊨E < a > φ当且仅当存在状态t, 使得${s\mathop \to \limits^a t}$且t⊨φ;

●  s⊨EGφ当且仅当存在路径π, 使得π(0)=s且∀i≥0, π(i)⊨φ.

我们定义如下对偶算子.

●  φ₁∨φ₂=﹁(﹁φ₁∧﹁φ₂);

●  A < a > =﹁E < a > ﹁;

●  AF=﹁EG﹁.

由定义, 我们可以得到这3个算子的语义.

●  s⊨φ₁∨φ₂当且仅当s⊨φ₁或s⊨φ₂;

●  s⊨A < a > φ当且仅当对于任意状态t, 如果${s\mathop \to \limits^a t}$, 则t⊨φ;

●  s⊨AFφ当且仅当对于任意路径π, 如果π(0)=s, 则∃i≥0, π(i)⊨φ.

基于BPP的EG逻辑的模型检测问题为:给定BPP(V, Δ), BPP表达式α以及EG逻辑公式φ, 判断α⊨φ是否成立.由文献[12]我们可以得到以下结论.

定理 1.基于BPP的EG逻辑的模型检测问题是不可判定的.

1.5 线性整数算术

线性整数算术(linear integer arithmetic)是一种一阶理论, 线性整数算术公式的语法可以如下表示.

定义 7(线性整数算术的语法).

$ {\psi : = {a_0} + {a_1}{x_1} + \ldots + {a_n}{x_n} \triangleleft |\neg \psi |\psi \wedge \psi |\exists x.\psi , } $

其中, ${{a_0}, {a_1}, \ldots , {a_n} \in {\mathbb{Z}}, \triangleleft \in \{ > , = \} .}$

1.6 SMT求解

SAT问题是计算机科学和人工智能领域中的一个重要问题.然而在SAT求解中, 求解的对象是表达能力相对较弱的命题逻辑公式, 在试图求解特定背景领域的问题时, 其难以表达各种约束.可满足性模理论(SMT)^[14]是SAT的扩展, 指的是在特定背景理论下, 判定一阶逻辑公式的可满足性问题.目前的SMT求解器能处理的理论主要包括未解释函数(uninterpreted function)、整数演算(integer arithmetic)、实数演算(real arithmetic)、数组(array)以及位向量(bit vector).直观上, 一个SMT公式可以被视为其命题变元代表着理论公式的逻辑公式, 因此具备比SAT公式更强的表达能力.SMT求解在模型检测、静态分析、线性规划和调度以及测试用例生成等领域中发挥着重要作用.由于SMT求解技术具有广阔应用前景, 因此目前, 其在工业界和学术界都得到了不少的重视.许多研究团队相继开发了SMT求解器, 目前主要的SMT求解器包括Yices^[15]、Z3^[16]、CVC4^[17]和MathSAT^[18]等.其中, 微软公司开发的SMT求解器Z3是目前综合求解能力最强的SMT求解器, 因此在本文作为我们的求解工具.

2 EG逻辑的模型检测及k步限界语义

本节主要对基于基本并行进程的EG逻辑模型检测问题的不可判定定理进行分析, 并基于此提出了EG逻辑在BPP模型上的k步限界语义.

2.1 不可判定性分析

文献[12]实际上证明了VBPP, 一个比BPP更弱的模型, 其针对EG逻辑的模型检测问题是不可判定的, 因此对于BPP而言也是不可判定的.VBPP是限定了规则集Δ中不能同时存在不同的规则$X\mathop \to \limits^a \alpha $和$X\mathop \to \limits^b \beta $的BPP, 即每个进程最多只能选择一种迁移方式.证明的思路是, 将不可判定的计数器机停机问题^[19]归约到该模型检测问题上.

一个计数器机M可以用一个三元组({q₀, …, q_n+1}, {c₁, …, c_m}, {t₀, …, t_n})表示, 其中, c_i表示计数器; q_i表示状态, 而q₀是初始态, q_n+1是终止态; t_i表示q_i的转移规则.状态分为两类.

●  类型1状态的转移规则的形式是

$ {{c_j}: = {c_j} + 1;{\rm{ goto}}{\kern 1pt} {\kern 1pt} {q_k}:} $

●  而类型2状态的转移规则的形式是

$ {{\rm{if}}{\kern 1pt} {\kern 1pt} {c_j}{\rm{ = 0}}{\kern 1pt} {\kern 1pt} {\rm{then}}{\kern 1pt} {\kern 1pt} {\rm{goto}}{\kern 1pt} {\kern 1pt} {\kern 1pt} {q_k}{\kern 1pt} {\rm{else}}({c_j}: = {c_j} - 1;{\rm{ goto}}{\kern 1pt} {\kern 1pt} {q_l})} $

M的一个配置是一个元组(q_i, j₁, …, j_m), 其中, j₁, …, j_m是计数器c₁, …, c_m记录的数值.我们说M停机是指:如果从初始配置(q₀, 0, …, 0)出发, M能够根据转移规则到达终止配置, 即状态为q_n+1的配置.计数器机的计算是确定性的, 因为每个状态最多只有一条转移规则.给定一个计数器机M, 通过归约可以构造出一个VBPP, VBPP表达式m(作为初始状态)以及EG逻辑公式Halt使得M停机当且仅当m满足Halt.

标签迁移系统的一个趟(run)是一条从初始状态出发的路径.与计数器机不同, VBPP/BPP的计算是非确定性的, 一个状态可以迁移到多个不同的状态, 因此不是所有的趟都会正确地模拟计数器机M的计算.我们称VBPP/BPP的一个趟是诚实的(honest), 是指这个趟正确地模拟了M的计算; 否则称其是不诚实的.通过EG逻辑公式的表达力, 我们可以区分诚实和不诚实的趟.构造Halt的要点是先构造公式φ, 使得φ满足两个性质:(1)存在一个趟, 使得这个趟上的所有状态都满足φ; (2)一个趟上的所有状态都满足φ, 当且仅当这个趟是诚实的.实际上, φ表示了M的计算过程中所需要满足的约束.接着, 公式Halt定义为

$ {Halt = AF(\neg \varphi \vee EN (halt)), } $

其中, EN(a)=E < a > true表示a被触发(enable).在构造VBPP的时候, 终止状态q_n+1被建模为进程Q_n+1, 相应的迁移规则为${Q_{n + 1}}\mathop \to \limits^{halt} {Q_{n - 1}}$.

由此, 我们可以得知M停机当且仅当m满足Halt.如果m满足Halt, 那么每个状态都满足φ的趟肯定存在一个状态满足EN(halt), 且由上述两个性质可知, 这样的趟肯定存在且诚实, 因此M停机.反之, 假设M停机.对于一个趟, 如果它是诚实的, 则因为M停机, 这个趟会包含一个满足EN(halt)的状态; 如果是不诚实的, 则由性质(2)可知, 这个趟上会由一个状态不满足φ, 即满足﹁φ.因此m满足AF(﹁φ∨EN(halt)).

直观上, 计数器机M中类型1状态的转移规则对应着VBPP/BPP的迁移序列X→^*α, 其中, α(X) > 1;而类型2状态的转移规则对应着迁移序列X→^*ε.第1种迁移序列会使得VBPP/BPP中状态的符号逐渐增加, 从而产生无穷长且不带循环的趟.这种特性对应着M的一种不停机的情况:计数器的数值不断增加而终止配置永远不会达到.我们通过下面的例子进行说明.假设M为

$ {(\{ {q_0}, {q_1}, {q_2}\} , \{ {c_1}, {c_2}\} , \{ {t_0}, {t_1}\} ), } $

其中, t₀为c₁:=c₁+1; goto q₁, t₁为c₂:=c₂+1; goto q₀, 则从初始配置出发, c₁, c₂中的数值持续增加但M不停机.构造的VBPP具有以下规则(进程符号用||分割).

$ \begin{array}{l} {C_j}\mathop \to \limits^{de{c_j}} \varepsilon , {\rm{ for}}{\kern 1pt} {\rm{ }}j = 1, 2, \\ {Q_0}\mathop \to \limits^{ou{t_0}} \left. {{Q_1}} \right\|{C_1}, \\ {Q_1}\mathop \to \limits^{ou{t_1}} \left. {{Q_0}} \right\|{C_2}, \\ {Q_2}\mathop \to \limits^{halt} {Q_2}. \end{array} $

初始配置表示为Q₀, 同时也作为初始状态m.不难发现, 存在以下诚实的趟模拟了M的不停机行为

$ {{Q_0}\mathop \to \limits^{ou{t_0}} {Q_1}\left\| {{C_1}\mathop \to \limits^{ou{t_1}} {Q_0}} \right\|{C_1}\left\| {{C_2}\mathop \to \limits^{ou{t_0}} {Q_1}} \right\|C_1^2\left\| {{C_2}\mathop \to \limits^{ou{t_1}} {Q_0}} \right\|C_1^2\left\| {C_2^2\mathop \to \limits^{ou{t_0}} } \right....} $

因此, 从m出发存在上述路径, 由于它诚实地模拟了M, 因此该路径上所有状态都满足φ.同时, 因为它始终没有进入终止状态Q₂, 所以动作halt没有被触发, 即路径上每一个状态都不满足EN(halt).根据EG逻辑的语义, 我们可以得到m⊨EG(φ∧﹁EN(halt)), 即﹁Halt.在给定的逻辑为EG逻辑的前提下, BPP上的模型检测问题不可判定的原因在于其会产生长度无穷但不含循环的路径.基于这个观察, 我们下面将路径限制在k步内进行模型检测.

2.2 k步限界语义

在EG逻辑的定义中, 原子命题被限定为true.为了表达进程的一些基础性质, 我们对原子命题的形式进行扩展.具体地说, 假设给定的BPP的有穷符号集V={X₁, …, X_n}, 我们规定原子命题为如下形式.

$ {A \cdot M \ge B.} $

其中, A是一个m×n维的整数矩阵, M是由BPP中进程符号组成的向量(X₁, …, X_n)^T, B是一个m维整数向量.例如, 下面的公式.

$ {AF(X + Y = 3 \to E\langle a\rangle (Z > 1))} $

表达的是:“如果一个状态中的进程X和Y的数量之和为3, 那么该状态存在一个经过动作a的后继状态, 其进程Z的个数大于1”这个性质在未来的某个时刻终将会被满足.

一个BPP表达式α可以很自然地表示为一个多重集合(multiset).例如, X₁X₂X₂X₃可以用集合{X₁, X₂, X₂, X₃}表示.在本文中, 我们将α表示为n维向量.严格地说, 定义Parikh映射(Parikh mapping)P:${{V^ \oplus } \to {{\mathbb{N}}^n}}$为

$ {P(\alpha ) = {{(\alpha ({X_1}), \ldots , \alpha ({X_n}))}^T}, } $

其中, α(X)表示X在中α出现的次数.注意:表示α的n维向量中的每个分量都必须满足非负的要求, 因为一个进程符号在BPP表达式中出现的次数不能为负数.在下文, 我们用Parikh映射来表示一个BPP状态.例如, 若V={X₁, X₂, X₃}, α=X₁X₂X₂, 则α可以用(1, 2, 0)^T表示.对于两个n维向量x=(x₁, …, x_n)^T, y=(y₁, …, y_n)^T, 定义x≤y当且仅当

$ {{x_1} \le {y_1}, \ldots , {x_n} \le {y_n}.} $

现在我们可以如下定义EG逻辑的k步限界语义.

定义 8(EG逻辑的k步限界语义).假设给定的BPP的有穷符号集V={X₁, …, X_n}.令M为由给定的BPP中进程符号组成的向量(X₁, …, X_n)^T, s为一个BPP表达式, φ为一个EG逻辑公式, k≥0.k步限界语义s⊨_kφ归纳定义如下.

●  s⊨_kA·M≥B当且仅当A·s≥B;

●  s⊨_k﹁φ当且仅当s⊨_kφ不成立;

●  s⊨_kφ₁∧φ₂当且仅当s⊨_kφ₁且s⊨_kφ₂;

●  s⊨_kE < a > φ当且仅当k≥1, 且存在状态t, 使得$s\mathop \to \limits^a t$且t⊨_kφ;

●  s⊨_kEGφ当且仅当存在路径π, 使得π(0)=s且∀0≤i≤k, π(i)⊨_kφ.

上述的k步限界语义表达了在从s出发的k步内的状态空间中φ在s上满足.注意:对于s⊨_kE < a > φ, 由于E < a > φ在s上成立必须经过一次迁移, 因此需要限制步数至少为1, 即k≥1.

3 线性整数算术公式刻画

本节主要根据上文给出的EG逻辑的k步限界语义, 构造对应的线性整数算术公式.我们首先定义一些基本约束来表示BPP的状态迁移等行为, 接着给出构造线性整数算术公式的算法并证明其正确性.在本节, 我们假设给定的BPP为(V={X₁, …, X_n}, Δ).

3.1 基本约束

首先定义一些约束, 包括原子约束、迁移约束和路径约束.

定义 9(原子约束).给定m×n维的整数矩阵A={a_ij}_m×n, n维向量s=(s₁, …, s_n)^T, m维整数向量b=(b₁, …, b_m)^T, 原子约束如下定义.

$ { \wedge _{i = 1}^m\left( {\sum\limits_{j = 1}^n {{a_{ij}}} \cdot {s_j} \ge {b_i}} \right).} $

原子约束表示了原子命题A·M≥B的语义A·s≥B, 即对于矩阵A的每个行向量A_i, A_i·s≥b_i都必须成立.

接着我们定义迁移约束, 即$s\mathop \to \limits^a t$对应的约束条件.我们首先定义一些基础符号和映射.对于每个规则r∈Δ, 我们用^●r表示箭头左边的符号, r^●表示箭头右边的BPP表达式, r^act表示迁移动作.例如若r为$X\mathop \to \limits^a \alpha $, 则^●r=X, r^●=α, r^act=a.

定义映射${P:V \times {V^ \oplus } \to {{\mathbb{N}} ^n}}$如下.

$ {P^ - }(X, \alpha ) = {({c^ - }(X, \alpha , {X_1}), \ldots , {c^ - }(X, \alpha , {X_n}))^T}, $

其中,

$ {{c^ - }({X^\prime }, \alpha , X) = \left\{ {\begin{array}{*{20}{l}} {\alpha (X) - 1, {\rm{ if}}{\kern 1pt} {\kern 1pt} X = {X^\prime }}\\ {\alpha (X), \quad {\rm{ otherwise }}} \end{array}.} \right.} $

映射P^-与Parikh映射P类似, 区别在于P^-(X, α)中X对应的整数值会比其在α中出现的次数α(X)少1.例如对于符号集只包含符号X₁, X₂, X₃的BPP, P(X₁X₂X₂X₃X₃)=(1, 2, 2)^T, P^-(X₂, X₁X₂X₂X₃X₃)=(1, 1, 2)^T.

给定r∈Δ, n维向量s=(s₁, …, s_n)^T和t=(t₁, …, t_n)^T.定义约束T^-(s, t, r)如下.

$ {{T^ - }(s, t, r) = \wedge _{i = 1}^n({s_i} + {P^ - }{{{(^ \bullet }r, {r^ \bullet })}_i} = {t_i}).} $

约束T^-实际上刻画了s和t中各个进程符号数量的关系, 表示s通过迁移规则r到达t.例如假设符号集V={X₁, X₂, X₃}, r为${X_1}\mathop \to \limits^a {X_2}$, 则^●r=X₁, r^●=X₂, P^-(^●r, r^●)=P^-(X₁, X₂)=(-1, 1, 0)^T, 此时, T^-(s, t, r)=(s₁-1=t₁)∧(s₂+1=t₂)∧(s₃=t₃).注意, 约束T^-(s, t, r)没有对t进行非负的限定, 因此t可能不是一个合法的BPP表达式.通过约束T^-, 我们现在可以定义迁移约束来表示$s\mathop \to \limits^a t$.

定义 10(迁移约束).给定两个n维向量s=(s₁, …, s_n)^T和t=(t₁, …, t_n)^T, 迁移动作a∈Act, 则s通过动作a到达t可以通过以下约束T(s, t, a)表示.

$ T(s, t, a) = {v_{r \in \varDelta }}({r^{act}} = a \wedge s{(^ \bullet }r) \ge 1 \wedge {T^ - }(s, t, r)). $

注意:在迁移约束中, 条件s(^●r)≥1是迁移被触发的必要条件, 其能够保证BPP的基本要求, 即BPP表达式中每个进程符号出现的次数不能为负数.例如, 对于(V={X, Y, Z}, Δ), 其中, Δ由下列规则组成.

$ \begin{array}{l} X\mathop \to \limits^a Y, \\ Y\mathop \to \limits^b XZZ. \end{array} $

令${p_1} = {(2, 0, 0)^T}\mathop \to \limits^a {(1, 1, 0)^T}\mathop \to \limits^b {(2, 0, 2)^T}, {p_2} = {(2, 0, 0)^T}\mathop \to \limits^b {(3, - 1, 2)^T}\mathop \to \limits^a {(2, 0, 2)^T}$.p₁和p₂都是从XX出发的长度k=2且最终到达XXZZ的序列, 但由于(3, -1, 2)^T中Y对应的整数值为-1, 因此该状态是不合法的.而s(^●r)≥1确保了${(2, 0, 0)^T}\mathop \to \limits^b {(3, - 1, 2)^T}$不会发生, 因为对于规则$Y\mathop \to \limits^b XZZ{;^ \bullet }r = Y$, 而Y在XX出现的次数为0.

我们如下定义路径约束, 即表示向量构成路径的约束.

定义 11(路径约束).令k≥0, u(0), u(1), …, u(k)为k+1个n维向量, 则这些向量构成一条路径可以通过以下约束Path(u(0), …, u(k))表示.

$ Path (u(0), \ldots , u(k)) = \wedge _{j = 1}^k[{ \vee _{r \in \varDelta }}(u(j - 1){(^ \bullet }r) \ge 1 \wedge {T^ - }(u(j - 1), u(j), r))]. $

路径约束Path(u(0), …, u(k))表示的是:对于每个1≤j≤k, u(j-1)可以根据规则集Δ中的一条迁移规则r到达u(j).与迁移约束中的条件s(^●r)≥1类似, 路径约束中必须包含条件u(j-1)(^●r)≥1.

3.2 构造线性整数算术公式

令k≥0, s是一个n维向量, φ是一个EG逻辑公式.构造线性整数算术公式的算法Trans(φ, s, k), 如图 2所示.

算法1接收一个EG逻辑公式φ、一个n维向量s以及一个非负整数k作为输入, 而输出是一个线性整数算术公式.该递归算法根据EG逻辑公式φ的结构进行递归.若φ为原子公式, 则生成原子约束.若φ的最外层算子是命题逻辑算子, 则根据否定和合取的语义进行构造.若φ形如E < a > φ₁或EGφ₁, 则通过迁移约束和路径约束结合限界语义生成相应的线性整数算术公式.注意, 算法返回的线性整数算术公式是一个闭合公式(closed formula).

下面我们证明:如果输入的向量s中所有分量都满足大于0的条件, 且同时算法生成的线性整数算术公式ψ成立, 则ψ中任意变量x都满足非负条件, 即x≥0.为了证明这个结论, 我们首先证明以下引理.

引理 1.给定r∈Δ, n维向量s=(s₁, …, s_n)^T和t=(t₁, …, t_n)^T, 如果$ \wedge _{i = 1}^n{s_i} \ge 0, s{(^ \bullet }r) \ge 1$和T^-(s, t, r)同时成立, 则$ \wedge _{i = 1}^n{t_i} \ge 0$成立.

证明:因为T^-(s, t, r)成立, 故对于任意1≤i≤n, 由映射P^-的定义, 可得t_i=s_i+P^-(^●r, r^●)_i=s_i+c^-(^●r, r^●, X_i).注意:对于任意r∈Δ, r^●(X_i)≥0.我们分以下两种情况讨论.

●  如果X_i≠^●r, 则t_i=s_i+r^●(X_i)≥s_i≥0;

●  如果X_i=^●r, 则t_i=s_i+r^●(X_i)-1=r^●(X_i)+s(X_i)-1=r^●(X_i)+s(^●r)-1≥r^●(X_i)≥0.

综上, $ \wedge _{i = 1}^n{t_i} \ge 0$成立.

借助引理1, 我们可以证明以下定理.

定理 2.给定EG逻辑公式φ、n维向量s=(s₁, …, s_n)^T和非负整数k.令π=E < a > φ或EGφ.若$ \wedge _{i = 1}^n{s_i} \ge 0 \wedge Trans (\pi , s, k)$成立, 则对于任意在构造线性整数公式Trans(π, s, k)的过程中新增的变量x都满足非负条件, 即x≥0.

证明:我们分别对π=E < a > φ和π=EGφ两种情况讨论.

●  假设π=E < a > φ.在Trans(E < a > φ, s, k)中, 新增的变量为t₁, …, t_n, 因为T(s, (t₁, …, t_n), a)成立, 由引理1可知:对于任意1≤i≤n, t_i≥0为真;

●  假设π=EGφ₁.在Trans(EGφ, s, k)中, 新增的变量为u(0)₁, …, u(0)_n, …, u(k)₁, …, u(k)_n.我们对步长k进行归纳证明.当k=0时, 由于$ \wedge _{i = 1}^nu{(0)_i} = {s_i}$和$ \wedge _{i = 1}^n{s_i} \ge 0$成立, 因此变量u(0)₁, …, u(0)_n非负.对于1≤j≤k, 由于存在r∈Δ使得u(j-1)(^●r)≥1∧T^-(u(j-1), u(j), r)为真, 且由归纳假设, 变量u(j-1)₁, …, u(j-1)_n非负, 因此由引理1可知, 变量u(j)₁, …, u(j)_n非负.综上, 变量u(0)₁, …, u(0)_n, …, u(k)₁, …, u(k)_n都为非负.

根据算法1, 在构造线性整数算术公式Trans(φ, s, k)时, 只有遇到E < a > 算子和EG算子时才会增加新的变量.因此由定理2我们可知:只要输入的n维向量s是一个合法的BPP状态, 即向量中的每个分量非负, 且同时算法1生成的线性整数算术公式Trans(φ, s, k)成立, 则基于算法1的编码不会出现到达不合法的BPP状态的情况.

3.3 算法的正确性

下面我们对EG逻辑公式进行结构归纳证明算法1的正确性.

定理 3(算法的正确性).给定EG逻辑公式φ, n维向量s=(s₁, …, s_n)^T和非负整数k, 则算法1是正确的, 即下列命题成立.

●  终止性:算法会终止.

●  可靠性:如果s⊨_kφ成立, 则Trans(φ, s, k)可满足.

●  完备性:如果Trans(φ, s, k)可满足, 则s⊨_kφ成立.

证明:由于算法1是根据EG逻辑公式φ的结构进行递归构造线性整数算术公式的, 因此可知算法1是终止的.对于可靠性和完备性, 我们如下对φ进行结构归纳证明.

●  假设φ是原子命题公式, 即φ=A·M≥B, 则根据原子约束$ \wedge _{i = 1}^m\left( {\sum\limits_{j = 1}^n {{a_{ij}}} \cdot {s_j} \ge {b_i}} \right)$以及s⊨_kA·M≥B当且仅当A·s≥B, 显然可得可靠性和完备性成立.

●  假设φ=﹁φ₁.对于可靠性, 假设Trans(﹁φ₁, s, k)不可满足, 则根据算法1, ﹁Trans(φ₁, s, k)不可满足, 因此Trans(φ₁, s, k)正确.由归纳假设, s⊨_kφ₁成立, 故s⊨_k﹁φ₁不成立.反之, 对于完备性, 假设Trans(﹁φ₁, s, k)正确, 则根据算法1, Trans(φ₁, s, k)不可满足, 由归纳假设, s⊨_kφ₁不成立, 故s⊨_k﹁φ₁成立.

●  假设φ=φ₁∧φ₂.对于可靠性, 假设Trans(φ₁∧φ₂, s, k)不可满足, 则根据算法1的构造, Trans(φ₁, s, k)∧Trans(φ₂, s, k)不可满足, 因此Trans(φ₁, s, k)不可满足或Trans(φ₂, s, k)不可满足.由归纳假设, s⊨_kφ₁或s⊨_kφ₂不成立, 因此s⊨_kφ₁∧φ₂不成立.反之, 对于完备性, 假设Trans(φ₁∧φ₂, s, k)正确, 则根据算法1, ﹁Trans(φ₁, s, k)不可满足且﹁Trans(φ₂, s, k)不可满足.由归纳假设, s⊨_k﹁φ₁且s⊨_k﹁φ₂不成立, 因此s⊨_kφ₁∧φ₂成立.

●  假设φ=E < a > φ₁.对于可靠性, 假设Trans(E < a > φ₁, s, k)可满足, 则k=0或者对于任意t₁, …, t_n, 如果T(s, (t₁, …, t_n), a), 则﹁Trans(E < a > φ₁, (t₁, …, t_n), k).若k=0, 则显然s⊨_kA < a > ﹁φ₁成立.若后者, 假设T(s, (t₁, …, t_n), a)正确, 则﹁Trans(φ₁, (t₁, …, t_n), k)正确, 因此Trans(φ₁, (t₁, …, t_n), k)不可满足.由归纳假设, (t₁, …, t_n)⊨_kφ₁不成立, 因此s⊨_kA < a > ﹁φ₁成立.综上, s⊨_kE < a > φ₁不成立.反之, 对于完备性, 假设Trans(E < a > φ₁, s, k)正确, 则k≥1且存在t₁, …, t_n, 使得T(s, (t₁, …, t_n), a)∧Trans(φ₁, (t₁, …, t_n), k), 因此﹁Trans(E < a > φ₁, (t₁, …, t_n), k)不可满足.由归纳假设, (t₁, …, t_n)⊨_k﹁φ₁不成立, 因此(t₁, …, t_n)⊨_kφ₁成立, 所以s⊨_kE < a > φ₁成立.

●  假设φ=EGφ₁.对于可靠性, 假设Trans(EGφ₁, s, k)不可满足, 则对于任意u(0)₁, …, u(0)_n, …, u(k)₁, …, u(k)_n, 如果$\alpha = path ((u{(0)_1}, \ldots , u{(0)_n}), \ldots , (u{(k)_1}, \ldots , u{(k)_n})) \wedge \wedge _{i = 1}^nu{(0)_i} = {s_i}$, 则$\neg \wedge _{j = 0}^k Trans ({\varphi _1}, (u{(j)_1}, \ldots , u{(j)_n}), k)$.假设α正确, 则存在0≤j≤k, 使得﹁Trans(φ₁, u(j), k)正确, 因此Trans(φ₁, u(j), k)不可满足.由归纳假设, u(j)⊨_kφ₁不成立, 因此s⊨_kAF﹁φ₁成立, 即s⊨_kEGφ₁不成立.反之, 对于完备性, 假设Trans(EGφ₁, s, k)正确, 则存在u(0)₁, …, u(0)_n, …, u(k)₁, …, u(k)_n, 使得$\alpha \wedge \wedge _{j = 0}^k Trans ({\varphi _1}, (u{(j)_1}, \ldots , u{(j)_n}), k)$.因此对于任意0≤j≤k, ﹁Trans(φ₁, u(j), k)不可满足.由归纳假设, u(j)⊨_k﹁φ₁不成立, 即u(j)⊨_kφ₁成立, 所以s⊨_kEGφ₁成立.

3.4 线性整数算术公式构造示例

为了更加直观地认识上述算法, 下面我们举例说明如何构建一个线性整数算术公式.

我们考虑BPP(V, Δ), 其中, V={X₁, X₂, X₃}, Δ包含以下规则.

$ \begin{array}{*{20}{l}} {{r_1}:{X_1}\mathop \to \limits^a {X_2}{X_3}, }\\ {{r_2}:{X_2}\mathop \to \limits^a {X_1}{X_2}, }\\ {{r_3}:{X_3}\mathop \to \limits^b {X_1}.} \end{array} $

我们令初始状态s=X₁, 令k=2, 则相应的标签迁移系统如图 3所示.

待检测的EG逻辑公式φ为EG(E < a > (X₂+X₃≥2)), 则Trans(φ, s, 2)为

$ \exists u{(0)_1}\exists u{(0)_2}\exists u{(0)_3}\exists u{(1)_1}\exists u{(1)_2}\exists u{(1)_3}\exists u{(2)_1}\exists u{(2)_2}\exists u{(2)_3}.\theta , $

其中,

$ \begin{array}{l} \theta : = Path((u{(0)_1}, u{(0)_2}, u{(0)_3}), (u{(1)_1}, u{(1)_2}, u{(1)_3}), (u{(2)_1}, u{(2)_2}, u{(2)_3})) \wedge (u{(0)_1} = 1 \wedge u{(0)_2} = 0 \wedge u{(0)_3} = 0) \wedge \\ {\rm{ }} \wedge _{j = 0}^2Trans(E\langle a\rangle ({X_2} + {X_3} \ge 2), (u{(j)_1}, u{(j)_2}, u{(j)_3}), 2){\rm{.}} \end{array} $

我们首先展开θ的第1个合取支即路径约束.根据映射P^-的定义, 可知:

$ {P^ - }({}^ \bullet {r_1}, r_1^ \bullet ) = {( - 1, 1, 1)^T}, {P^ - }({}^ \bullet {r_2}, r_2^ \bullet ) = {(1, 0, 0)^T}, {P^ - }({}^ \bullet {r_3}, r_3^ \bullet ) = {(1, 0, - 1)^T}. $

因此, 路径约束中的每个合取支(j=1, 2)为

$ \begin{array}{l} {\psi _{trans}}(j): = [u{(j - 1)_1} \ge 1 \wedge (u{(j - 1)_1} - 1 = u{(j)_1} \wedge u{(j - 1)_2} + 1 = u{(j)_2} \wedge u{(j - 1)_3} + 1 = u{(j)_3})] \vee \\ \ \ \ \ \ \ \ \ [u{(j - 1)_2} \ge 1 \wedge (u{(j - 1)_1} + 1 = u{(j)_1} \wedge u{(j - 1)_2} + 0 = u{(j)_2} \wedge u{(j - 1)_3} + 0 = u{(j)_3})] \vee \\ \ \ \ \ \ \ \ \ [u{(j - 1)_3} \ge 1 \wedge (u{(j - 1)_1} + 1 = u{(j)_1} \wedge u{(j - 1)_2} + 0 = u{(j)_2} \wedge u{(j - 1)_3} - 1 = u{(j)_3})]. \end{array} $

所以路径约束为ψ_trans(1)∧ψ_trans(2).

接着, 我们展开θ的第3个合取支.对于j=0, 1, 2, 考虑Trans(E < a > (X₂+X₃≥2), (u(j)₁, u(j)₂, u(j)₃), 2), 该约束对应着子公式E < a > (X₂+X₃≥2)在(u(j)₁, u(j)₂, u(j)₃)上2步内成立的情形, 展开为

$ \begin{array}{l} {\psi _{sub}}(j): = 2 \ge 1 \wedge \exists {t_1}\exists {t_2}\exists {t_3}.(([a = a \wedge u{(j)_1} \ge 1 \wedge (u{(j)_1} - 1 = {t_1} \wedge u{(j)_2} + 1 = {t_2} \wedge u{(j)_3} + 1 = {t_3})] \vee \\ \ \ \ \ \ \ \ \ \ \ [a = a \wedge u{(j)_2} \ge 1 \wedge (u{(j)_1} + 1 = {t_1} \wedge u{(j)_2} + 0 = {t_2} \wedge u{(j)_3} + 0 = {t_3})] \vee \\ \ \ \ \ \ \ \ \ \ \ [b = a \wedge u{(j)_3} \ge 1 \wedge (u{(j)_1} + 1 = {t_1} \wedge u{(j)_2} + 0 = {t_2} \wedge u{(j)_3} - 1 = {t_3})]) \wedge {t_2} + {t_3} \ge 2). \end{array} $

因此, 第3个合取支为ψ_sub(0)∧ψ_sub(1)∧ψ_sub(2).注意:对于上述公式中的迁移动作, 我们在实际中可以用整数进行编码.

综上, 根据算法生成的公式Trans(φ, s, 2)为

$ \begin{array}{l} \psi : = \exists u{(0)_1}\exists u{(0)_2}\exists u{(0)_3}\exists u{(1)_1}\exists u{(1)_2}\exists u{(1)_3}\exists u{(2)_1}\exists u{(2)_2}\exists u{(2)_3}\\ \ \ \ \ \ \ ({\psi _{trans}}(1) \wedge {\psi _{trans}}(2) \wedge (u{(0)_1} = 1 \wedge u{(0)_2} = 0 \wedge u{(0)_3} = 0) \wedge {\psi _{sub}}(0) \wedge {\psi _{sub}}(1) \wedge {\psi _{sub}}(2)) \end{array} $

4 工具实现及实验结果 4.1 技术架构

基于线性整数算术公式刻画, 我们采用基于约束的方法实现了工具, 其架构如图 4所示.

工具接受3个输入, 分别是BPP模型(V, Δ)、待检测的EG逻辑公式φ以及步长k.工具从这些输入获取BPP中符号集V和规则集Δ的信息, 并根据EG逻辑公式φ的结构以及步长k的大小, 生成原子约束、迁移约束和路径约束等约束条件, 进而构造出相应的线性整数算术公式, 保存为约束文件作为SMT求解器Z3的输入.如果Z3的求解结果为sat, 则说明在限界语义下EG逻辑公式φ在k步内满足; 若求解的返回结果为unsat, 则说明在k步内不满足.

4.2 实验结果

我们在实验部分首先讨论第3.4节中的BPP的例子(如图 3所示), 该BPP包含3个进程符号以及3条规则.我们对以下4个EG逻辑公式在限制步长k分别为1, 5, 10, 20, 50和100的条件下进行限界模型检测.

$ \begin{array}{l} {\varphi _1} = {X_1} + {X_2} \ge 1 \wedge {X_3} \ge 0, \\ {\varphi _2} = EG(E\langle a\rangle ({X_2} + {X_3} \ge 2)), \\ {\varphi _3} = EG({X_1} + {X_2} \ge 2 \to E\langle a\rangle ({X_1} \ge 2 \wedge {X_3} \ge 1)), \\ {\varphi _4} = EG(AF({X_1} + {X_2} \ge 2)). \end{array} $

实验结果见表 2, 实验结果的单位为s.

从表 2可以看出, 对于φ₁, 步长k不影响求解时间.这是因为φ₁是两个原子命题公式的合取式, 根据算法1, 对于原子命题公式, 作为参数的k不参与线性整数算术公式的构造, 因此求解φ₁的时间总体趋于一致.而对于φ₂, φ₃, φ₄, 求解时间总体上随着步长k的增大而增加.公式φ₃的嵌套深度比φ₂的和φ₄的均要小, 然而求解φ₃的时间只比求解φ₂的稍多, 而求解φ₄的时间相对于求解φ₂, φ₃的时间较多, 这在步长k较大, 如k=50, 100时尤为明显.这是因为限制求解速度的原因在于变量的数量.对于EG算子, 根据算法1, 生成的线性整数算术公式需要引入(k+1)·n个变量, 其中, n为BPP中进程符号的数量.而φ₄实际上等价于公式EG(﹁EG﹁(X₁+X₂≥2)), 因此对于φ₄, 生成的线性整数算术公式中含有的变量数目为(k+1)²·n², 因此在k较大时, 求解器在较长时间后返回结果.

因为已有的程序验证基准案例并不能证明其全部可以BPP可解, 所以这些案例并不能直接使用.同时, 现有的与Petri网相关的验证工具都是针对传统Petri网, 它们所使用的标准测试集也不再适用.因此, 我们随机生成了测试用例, 对不同规模的BPP在多个步长下进行实验.BPP的规模主要体现在其进程符号的数量以及迁移规则的数目.我们实验的对象是进程符号数分别是20, 50和100的BPP.对于具有相同进程符号数的BPP, 我们将迁移规则数分别设置为10, 20和30进行实验.对于EG逻辑公式, 我们选取了上述的φ₂, φ₃, φ₄.表 3~表 5分别对应k分别为15, 20, 25的实验结果, 单位为s.

从实验结果可以看出, 求解时间随着进程符号数量和迁移规则数目的增加以及k的增大而增加.进程符号数量影响了线性整数算术公式中引入的量词和变量的数目.此外, 对于一个BPP状态s, 因为我们要保证经过一次迁移后得到的状态t, s和t中每一个进程符号的数量关系要与相应的规则一致, 因此BPP进程符号数的增多会导致对应约束数量的增加, 从而影响求解时间.在迁移约束和路径约束中, 由于要在BPP规则集中寻找使得迁移和路径成立的规则, 因此规则集的大小影响了迁移约束和路径约束中析取式的公式大小.而步长k决定了最外层算子为EG的公式对应的线性整数算术公式的路径约束中合取式的大小, 即子约束的数目, 同时, k也对引入的变量数目产生影响.

5 相关工作

在基于BPP和Petri网的模型检测问题上, 对于线性时间逻辑, Petri网上的线性时间mu-演算的模型检测问题是可判定的^[20].然而, 对于一些表达力比较弱的逻辑, 如原子命题为EN(a)且只包含Fφ作为模态算子的线性时间逻辑, 在VBPP上的模型检测却是不可判定的^[12].对于分支时间逻辑, 除了上文提及的不可判定性结果, 对于EF逻辑, 即在Hennessy-Milner Logic的基础上增加EF算子的逻辑, Esparza还在文献[12]中证明了以下结论:

(1) 基于Petri网的模型检测问题是不可判定的, 然而对于BPP, 即使给定的BPP是有穷状态的, 该问题是PSPACE难的; (2)在BPP上, 对于长度固定的公式(fixed formula), 模型检测问题是$\varSigma _d^p$难的, 其中, d是模态算子的嵌套深度.在这个结论的基础上, Mayr证明了若给定的模型为BPP, 则EF逻辑的模型检测问题实际上分别是PSPACE完备和$\varSigma _d^p$完备的^[21].EGF是CTL*的一个算子, 其表达的是:“存在一条路径, 使得某个特定的性质被满足无穷次”.在正则模型检测(regular model checking)中, EGF代表了活性和反复可达性(recurrent reachability).在EF逻辑的基础上加上EGF算子, 我们可以得到EGF逻辑.文献[22]证明了BPP上对EGF逻辑的模型检测问题是可判定的.而Fu证明了该问题的复杂度是PSPACE完备且对于长度固定的公式是$\varSigma _d^p$完备的^[13], 也就是说, 增加EGF算子并没有提高模型检测的复杂度.证明的关键思路是使用一种称为半片段(semisegment)的结构, 而该结构也被用于处理基于Petri网模型检测的状态爆炸问题^[23].

在安全性问题上, Petri网的可达性问题是可判定的^[24], 且最早被证明是EXPSPACE难的^[25], 然而该问题的复杂度仍然是学术界的一个开问题.最近, 文献[26]证明了该问题的一个新的Ackermannian上界, 而文献[9]证明了该问题的一个新的Tower难下界.Petri网的可覆盖性问题是EXPSPACE完备的^{[27, 28]}, 对于Petri网的可覆盖性, 目前检测工具主要分为两类:一类基于完备算法, 对状态空间进行搜索, 判断可达的状态集是否覆盖了指定状态, 这类工具包括BFC^[1], IIC^[29]和MIST; 而另一类工具如Petrinizer^[30]将给定的Petri网的结构和状态以及可覆盖性条件转换为约束, 然后交给求解器进行求解.然而, Petrinizer在理论上是不完备的, 其无法判定不安全的测试用例.以上这些工具由于Petri网的可覆盖性问题复杂度过高, 因此都无法处理规模较大的测试用例.而BPP的可达性以及可覆盖性问题是NP完备问题^[11].针对BPP, 文献[31]实现了工具CFPCV, 在Petri网可覆盖性检测的安全性方法的基础上, 额外增加了基于BPP的子网可标记方法, 并以此来验证状态是否可达, 保证了算法在理论上是完备的.

在限界模型检测上, 模型检测问题一般被规约为SAT问题.该方法最先被运用到检测LTL性质上^[32], 接着在ACTL性质检测上也具有应用^[33].但是这两类研究只关注时序逻辑的存在片段(existential fragment), 其限界语义不能适用于如本文提及的活性AFφ等表示全称(universal)性质的公式.文献[34]就此问题提出了CTL的限界语义, 并将CTL公式编码为QBF公式.以上研究讨论的模型都是有穷状态系统, 对于无穷状态系统, 文献[35]提出了将性质分别用LTL_-X和ECTL_-X表示, 并在分布式时间Petri网上进行限界模型检测的方法, 该方法仍是将模型检测问题编码为命题逻辑公式.不同于直接处理时序逻辑公式的方法, 文献[36]首先将时序逻辑公式转换为对应的ω自动机, 其接受条件为安全性或活性等性质条件, 然后将ω自动机编码为Presburger算术, 而该方法适用于无穷状态系统.

6 总结及未来的工作

本文关注基本并行进程上EG逻辑的限界模型检测问题, 并将该问题转化为线性整数算术公式的可满足性问题.首先, 我们根据基于基本并行进程的限定步长为k的EG逻辑限界语义, 以及基本并行进程的模型结构和表示特定性质的EG逻辑公式, 定义相应的约束, 并给出了对应的基于线性整数算术公式的刻画, 然后将线性整数算术公式作为SMT求解器的输入进行求解.

我们未来的工作主要包括两个方面:一是对并发程序的一些性质如动态更新(dynamic updating)进行分析, 使用基本并行进程对并发程序进行建模并验证这些性质; 二是尝试寻找描述并发程序的其他模型, 并比较和分析其在安全性和活性的验证上与基本并行进程的异同.