软件学报  2017, Vol. 28 Issue (4): 898-906   PDF    
NuTL2PFG:νTL公式的可满足性检查
刘尧1,2, 段振华1,2, 田聪1,2     
1. 西安电子科技大学 计算理论与技术研究所, 陕西 西安 710071;
2. 综合业务网理论及关键技术国家重点实验室 (西安电子科技大学), 陕西 西安 710071
摘要: 线性μ演算(linear time μ-calculus,简称νTL)语法简单,表达能力强,可用于验证并发程序的多种性质.然而,不动点操作符的嵌套使其判定问题难以有效解决.针对这一问题,开发了工具NuTL2PFG,用以判定νTL公式的可满足性.利用νTL公式的当前-未来范式(present future form,简称PF式),该工具能够为一个给定公式构造其当前-未来范式图(present future form graph,简称PFG),用以描述满足该公式的模型.通过在所得PFG中寻找一条ν-路径,即,不涉及最小不动点公式的无穷展开的路径,该工具便可判断出给定公式的可满足性.实验结果表明,NuTL2PFG的执行效率优于已有工具.
关键词: 线性μ演算     当前-未来范式     当前-未来范式图     可满足性    
NuTL2PFG: Checking Satisfiability of νTL Formulas
LIU Yao1,2, DUAN Zhen-Hua1,2, TIAN Cong1,2     
1. Institute of Computing Theory and Technology, Xidian University, Xi'an 710071, China;
2. State Key Laboratory of Integrated Service Networks (Xidian University), Xi'an 710071, China
Foundation item: National Natural Science Foundation of China (61322202, 61133001, 61420106004, 91418201)
Abstract: Linear time μ-calculus (νTL) is a formalism which has a strong expressive power with a succinct syntax. It is useful for specifying and verifying various properties of concurrent programs. However, the nesting of fix point operators makes its decision problem difficult to solve. To tackle the issue, a tool called NuTL2PFG for checking the satisfiability of νTL formulas is developed in this paper. Based on present future form (PF form) of νTL formulas, the tool is able to construct the present future form graph (PFG) for a given formula to specify the models that satisfy the formula. Further, the tool checks the satisfiability of a given formula by searching for a ν-path in its PFG free of infinite unfoldings of least fixpoints. Experimental results show that NuTL2PFG is more efficient than the existing tools.
Key words: linear time μ-calculus     present future form     present future form graph     satisfiability    

线性μ演算 (linear time μ-calculus, 简称νTL)[1]是模态μ演算[2]的时序版本, 它与线性时序逻辑 (linear temporal logic, 简称LTL)[3]最大的不同在于最小和最大不动点操作符的引入.νTL不仅语法简洁, 而且具有完全正则的表达能力[4, 5], 可用于表达和验证并发程序的多种正则性质, 这些性质是LTL无法表达的.因此, νTL在过去的几十年里受到了科学研究和工程技术领域的广泛关注.从实际应用的角度来看, 为νTL公式的可满足性提出一种有效的判定算法十分重要, 这对获得有效的νTL模型检测算法起着决定性作用.可满足性是指找出一种判定算法, 用以判断一个给定公式是否可满足, 它的复杂度是PSPACE-complete[6, 7], 即, 指数级时间和多项式空间复杂度.

针对νTL的判定问题, 目前主要存在两类方法:基于自动机的方法[6, 8]和基于Tableau的方法[9-11].基于自动机的方法主要用到αβ两个自动机, 其中, α用于检测预模型 (pre-model) 的一致性, β用于检测最小不动点的非良基性 (non-well-foundedness).通过对αβ的补的乘积自动机进行判空, 从而判断公式的可满足性, 时间复杂度为${2^{O({n^4})}}, $其中, n表示公式的长度 (下同).基于Tableau的方法主要利用相关推导规则来构造给定公式的Tableau, 通过检查所得Tableau中各分支成功与否, 进而判断公式的可满足性, 时间复杂度为${2^{O({n^2}\log n)}}.$此外, 文献[12]证明, 若一个公式可满足, 则该公式能够生成一个好的Hintikka结构, 进而将公式的可满足性问题转化为图的路径搜索问题.该方法的时间复杂度为${2^{O({n^4})}}$, 空间消耗为指数级.然而, 上述方法中涉及的判定过程较为复杂, 并且缺少相应的支持工具.文献[13]为νTL提出了一种简单的判定方法, 其时间复杂度为${2^{O({n^2}\log n)}}, $并且用OCAML实现了工具PS4NuTL.该工具是当前存在的针对νTL判定问题的唯一工具.

本文展示了原型工具NuTL2PFG, 用以检查νTL公式的可满足性.NuTL2PFG能够将νTL公式转化为当前-未来范式 (present future form, 简称PF式)[14, 15].当前部分是原子命题或它们的非的合取式, 未来部分是给定公式的闭包中元素的合取式.基于PF式, NuTL2PFG能够构造出一个公式的当前-未来范式图 (present future form graph, 简称PFG), 用以描述该公式的模型.在构造PFG的过程中, 需要对某些边添加记号, 用于记录不动点公式的展开情况.一个记号就是公式中出现的变量的一个子集.通过记号, 能够找出PFG中的ν-路径, 即, 不存在最小不动点公式的无穷展开的路径.这样, 对于一个给定的公式, NuTL2PFG通过构造其PFG并在该PFG中寻找一条ν-路径, 便可判断该公式的可满足性.基于PFG的判定方法的时间复杂度为2O(n), 空间消耗为指数级[15].实验结果显示, NuTL2PFG的表现优于文献[13]中的工具PS4NuTL.需要注意的是:本文方法的复杂度仅适用于受卫公式, 而已有方法的复杂度适用于任意公式.

PF式和PFG的概念受命题投影时序逻辑 (propositional projection temporal logic, 简称PPTL) 的范式 (normal form) 和范式图 (normal form graph)[16, 17]的启发.范式和范式图能够用于判定PPTL公式的可满足性[18-20].

本文第1节给出νTL的语法、语义和其他基本概念.第2节介绍νTL公式的PF式、PFG以及PFG中的ν-路径.第3节详细描述工具NuTL2PFG的架构.第4节给出相关实验结果与分析.第5节对本文进行总结, 并进一步指出今后的研究方向.

1 基础概念 1.1 νTL语法

$\mathcal{P}$为一个原子命题集合, $\mathcal{V}$为一个变量集合.νTL公式可根据以下语法进行构造:

$\phi :: = p\left| {\neg p} \right|X\left| {\phi \vee \phi } \right|\phi \wedge \phi \left| {{\bigcirc}\phi } \right|\mu X.\phi \left| {\nu X.\phi, } \right.$

其中, p$\mathcal{P}$, X$\mathcal{V}$.

通常用σ来表示μν.σX表示变量Xσ绑定.在一个公式中, 如果变量X的出现位于σX的辖域之内, 则称X为约束变量 (bound variable); 否则, 称为自由变量 (free variable).如果一个公式中不包含自由变量, 则称该公式是封闭的 (closed).通常以ϕ[φ/X]表示将公式ϕ中所有变量X的自由出现替换为公式φ.假定在一个公式中每个变量至多可被绑定1次, 那么按照上述语法构造出的公式都是正则式 (positive normal form)[21].

对于公式φ中出现的任意约束变量X, 都存在一个形如sX.φXφ的子公式, 称该公式为Xφ中的绑定式, 记作Γφ(X).给定φ中的两个约束变量XY, 如果Γφ(Y) 是Γφ(X) 的子公式, 则称X高于Y.如果X高于Y并且在Γφ(Y) 中自由出现, 则称Y依赖于X, 记作XY.在一个公式中, 变量间的依赖关系具有可传递性.

例如, 对于公式νX. μY.(p∧◯XνZ.◯(YqZr)), 可得XYZ.

一个公式是受卫的 (guarded) 当且仅当该公式中任意约束变量均处于◯操作符的辖域之内.任何公式都能转化为与之等价的受卫公式[22].对公式进行受卫转换时, 在最坏情况下, 可能导致公式长度的指数级增长[23].

对于一个给定的公式φ, 基于文献[24], 归纳定义其闭包CL(φ) 如下.

(1) φ, true∈CL(φ);

(2) 若ϕψCL(φ) 或ϕψCL(φ), 则ϕ, ψCL(φ);

(3) 若◯ϕCL(φ), 则ϕCL(φ);

(4) 若σX.ϕCL(φ), 则ϕ[σX.ϕ/X]∈CL(φ).

对于任意公式φ, CL(φ) 中的公式个数为O(|φ|)[24].这里, |φ|表示φ的长度.

1.2 νTL语义

νTL公式的语义需要通过线性结构进行解释.一个关于$\mathcal{P}$的线性结构是一个函数$\mathcal{K}$:$\mathbb{N} \to {2^{\cal P}}$, 这里, $\mathbb{N}$表示自然数集.给定一个环境e:$\mathcal{V} \to {2^\mathbb{N}}$, 公式ϕ关于$\mathcal{K}$e的语义定义如下:

$\begin{array}{l} [\kern-0.15em[p]\kern-0.15em] _e^\mathcal{K}: = \{ i \in \mathbb{N}\:|\:p \in \mathcal{K}(i)\}, [\kern-0.15em[\neg p]\kern-0.15em] _e^\mathcal{K}: = \{ i \in \mathbb{N}\:|\:p \notin \mathcal{K}(i)\}, [\kern-0.15em[X]\kern-0.15em] _e^\mathcal{K}: = e(X), \hfill \\ [\kern-0.15em[\varphi \vee \psi]\kern-0.15em] _e^\mathcal{K}: = [\kern-0.15em[\varphi]\kern-0.15em] _e^\mathcal{K} \cup [\kern-0.15em[\psi]\kern-0.15em] _e^\mathcal{K}, [\kern-0.15em[\varphi \wedge \psi]\kern-0.15em] _e^\mathcal{K}: = [\kern-0.15em[\varphi]\kern-0.15em] _e^\mathcal{K} \cap [\kern-0.15em[\psi]\kern-0.15em] _e^\mathcal{K}, [\kern-0.15em[\bigcirc \varphi]\kern-0.15em] _e^\mathcal{K}: = \{ i \in \mathbb{N}\:|\:i + 1 \in [\kern-0.15em[\varphi]\kern-0.15em] _e^\mathcal{K}\}, \hfill \\ [\kern-0.15em[\mu X.\varphi]\kern-0.15em] _e^\mathcal{K}: = \bigcap {\{ W \subseteq \mathbb{N}\:|\: [\kern-0.15em[\varphi]\kern-0.15em] _{e[X \mapsto W]}^\mathcal{K} \subseteq W\} }, [\kern-0.15em[\nu X.\varphi]\kern-0.15em] _e^\mathcal{K}: = \bigcup {\{ W \subseteq \mathbb{N}\:|\:W \subseteq [\kern-0.15em[\varphi]\kern-0.15em] _{e[X \mapsto W]}^\mathcal{K}\} }, \hfill \\ \end{array} $

其中, e[XW]表示一个新的环境e'.除e'(X)=W之外, e'对其他变量的赋值与e相同.环境e用于对自由变量进行赋值, 当ϕ封闭时可省略.

对于一个给定的公式φ, 其在线性结构$\mathcal{K}$的状态i下为真, 记作$\mathcal{K}$, iφ, 当且仅当$i \in [\kern-0.15em[\varphi]\kern-0.15em] _e^\mathcal{K}$.称φ是有效的, 记作╞φ, 当且仅当对于任意线性结构$\mathcal{K}$以及$\mathcal{K}$中的任意状态j, 均有$\mathcal{K}$, jφ; 称φ是可满足的, 当且仅当存在一个线性结构$\mathcal{K}$以及$\mathcal{K}$中的一个状态j, 使得$\mathcal{K}$, jφ.

2 PF式和PFG

从本节开始, 只考虑封闭的受卫公式.同时, ∨操作符不得作为◯操作符辖域下的主操作符 (可由等价性◯(φ1φ2)≡◯φ1∨◯j2进行相关转换).

2.1 PF式

定义1(PF式).给定一个公式j, 令$\mathcal{Q}$表示φ中出现的原子命题集合.φ的PF式定义为

$\varphi \equiv \vee _{i = 1}^n({\varphi _{{p_i}}} \wedge \bigcirc {\varphi _{{f_i}}}), $

其中, ${\varphi _{{p_i}}} \equiv \wedge _{j = 1}^h{\dot p_{ij}}, {\varphi _{{f_i}}} \equiv \wedge _{k = 1}^m{\varphi _{ik}}$.对于任意j, 有pij$\mathcal{Q}$(对于任意r$\mathcal{Q}$, $\dot r$表示r或﹁r); 对于任意k, 有φikCL(φ).

利用PF式可以将一个公式φ分解为当前和未来两部分, 其中, 当前部分${\varphi _{{p_i}}}$φ中的原子命题或它们的非的合取式, 未来部分${\varphi _{{f_i}}}$CL(φ) 中的元素的合取式.这样, 为了满足φ, 当前状态需要满足当前部分, 下一状态需要满足未来部分.通过把未来部分的公式分别转化为PF式, 并且不断重复该转化过程, 就能构造出描述φ的模型的图, 即PFG.

2.2 PFG

给定一个公式ϕ.它的PFG, 记作Gϕ, 是一个三元组 (Nϕ, Eϕ, n0), 其中, Nϕ是节点集, Eϕ是边集, n0是根节点.Nϕ中的每个节点都是CL(ϕ) 中公式的合取式.Eϕ中的每条边都是一个三元组 (ϕi, ϕe, ϕj), 其中, ϕi, ϕjNϕ, ϕe是边上的标签.此外, 边上可能伴有记号.一个记号就是ϕ中出现的变量的一个子集.

定义2(PFG).给定公式ϕ.NϕEϕ归纳定义如下.

(1) n0=ϕNϕ;

(2) 对于任意φNϕ\{false}, 若$\varphi \equiv \vee _{i = 1}^k({\varphi _{{p_i}}} \wedge \bigcirc {\varphi _{{f_i}}}), $则对任意i, 均有${\varphi _{{f_i}}} \in {N_\phi }, (\varphi, {\varphi _{{p_i}}}, {\varphi _{{f_i}}}) \in {E_\phi }.$

在一个PFG中, 根节点用双圆形表示, 其他节点用单圆形表示.每条边由一条有向弧表示, 弧上伴有标签.此外, 还可能伴有记号.为了表述方便, 在节点中通常用变量来表示相应的不动点公式.

图 1中展示了公式μX.(p∨◯◯X) 的PFG.该PFG共有3个节点, 其中, n0为根节点.(n0, p, n1) 是一条不带记号的边, 其标签为p.(n0, true, n2) 是一条带有记号{X}的边, 其标签为true.

Fig. 1 An example of PFG 图 1 PFG实例

PFG中的路径Π是指始于根节点的节点和边的无穷交替序列.每条路径均对应一个线性结构.

$Atom( \wedge _{i = 1}^m{\dot q_i})$表示公式$ \wedge _{i = 1}^m{\dot q_i}$中的原子命题或它们的非的集合.对于一条路径Π=ϕ0, ϕe0, ϕ1, ϕe1, …, 可以得到

一个对应的线性结构Atom(ϕe0), Atom(ϕe1), Atom(ϕe2), …例如, 与图 1中路径n0, p, (n1, true)ω相对应的线性结构为{p}, {true}ω.

2.3 记号

图 1可以看出:PFG中的路径, 例如 (n0, true, n2, true)ω, 可能产生于最小不动点公式的无穷展开.因此, 在构造PFG的过程中, 需要添加记号用以追踪不动点的展开情况.

定义3(记号).给定一个PFG Gϕ以及Gϕ中的一个节点φ, 其中, $\varphi \equiv \vee _{i = 1}^k({\varphi _{{p_i}}} \wedge \bigcirc {\varphi _{{f_i}}}), $$(\varphi, {\varphi _{{p_i}}}, {\varphi _{{f_i}}})$(1≤ik) 的

记号是一个变量集M, 并且满足以下两个条件.

(a) 对于M中的任意变量X, 与之对应的不动点公式σX.φXCL(ϕ) 是${\varphi _{{f_i}}}$的子公式;

(b) 在PF式的转化过程中, σX.φX在未来部分的出现不是源于公式νY.φY(Y高于X) 的展开.

2.4 ν-路径

给定一个公式ϕ.实际上, Gϕ中的节点的每一条出边均对应于选择函数[6]的一种可能的选择.由于一个节点不能同时拥有多个选择, 因此在Gϕ中, 只需考虑结束于简单环的路径.令ΠGϕ中的一条路径.为方便起见, 用LES(Π) 来表示出现在Π中环的部分的边集, 用Mark(e) 表示边e上的记号, 用LMS(Π) 表示LES(Π) 中的边上的记号里所有μ型变量的集合.

定义4(ν-路径).给定一个PFG以及该PFG中的一条路径Π.称Π是一条ν-路径当且仅当对于任意XLMS(Π), 均能找到一条边eLES(Π), 使得XMark(e), 并且对于任意变量X'(XX'), X'∉Mark(e).

由文献[15]中的定理4可知, 一个公式是可满足的当且仅当其PFG中存在一条ν-路径.因此, νTL公式的可满足性问题得以转化为PFG中的ν-路径搜索问题.本文已用C++开发了基于PFG的νTL公式可满足性判定工具NuTL2PFG, 该工具的工作原理将在下一节进行介绍.

3 原型工具 3.1 工具架构

基于PFG的概念, 我们开发了用于判定nTL公式可满足性的原型工具NuTL2PFG, 其架构如图 2所示.

Fig. 2 Architecture of NuTL2PFG 图 2 NuTL2PFG架构

NuTL2PFG主要包括4个模块, 分别是语法树构造模块、PF式转化模块、PFG构造模块以及n-路径搜索模块.该工具以一个公式φ作为输入, 格式为文本文件.在该文件中, 公式各操作符的表示方法如下:~表示﹁; |和 & 分别表示∨和∧;next表示◯;munu分别表示μν.例如, 公式νX.(dXμY.(p∨﹁q∧dY)) 可表示为

$nu\;X\left( {{\text{next}}\;\;X\;\& \;mu\;Y.\left( {p\left| { \sim q\& \;{\text{next}}\;Y} \right.} \right)} \right).$

首先, 语法树构造模块创建φ的语法树, 在PFG中的所有相关操作都是在语法树上进行的; 然后, PFG构造模块开始创建φ的PFG, 在此过程中, 需要不断调用PF式转化模块将节点转化为PF式, 并据此生成新的节点和边, 直至所有节点均已被处理; 最后, ν-路径搜索模块检测所得PFG中是否存在ν-路径, 以此来判定φ的可满足性.

3.2 语法树构造

PFG中所有关于节点和边的操作都是在语法树的概念上进行的.νTL公式的语法树结构如图 3所示.

Fig. 3 Syntax trees of νTL formulas 图 3 νTL公式的语法树

图 3可以看出, 语法树的根节点能够表示相应的节点类型.true、false、原子命题或它们的非以及变量的语法树均不含子节点.在公式φψ(或φψ) 的语法树中, 左右孩子分别对应该公式的左右析取项 (或合取项).公式◯φ的语法树只有一个孩子φ.在不动点公式σX.φ的语法树中, 左孩子为变量X, 右孩子为公式φ.

3.3 PF式转化

在构造PFG的过程中, PF式转化模块不断被PFG构造模块调用, 进而将PFG中的节点转化为PF式并返回给PFG构造模块.将一个公式φ转化为PF式的算法PFTran可递归描述如下.

(1) 当φ为true时, 返回true∧◯true;

(2) 当φ为false时, 返回false;

(3) 当φφp时, 其中, ${\varphi _p} \equiv \wedge _{k = 1}^m{\dot p_k}$, 返回φp∧◯true;

(4) 当φφp∧◯ψ时, 返回∨i(φp∧◯ψi);

(5) 当φ为◯ψ时, 返回∨i(true∧◯ψi);

(6) 当φφ1φ2时, 返回PFTran(φ1)∨PFTran(φ2);

(7) 当φφ1φ2时, 返回AND(PFTran(φ1), PFTran(φ2));

(8) 当φσX.ψ时, 返回PFTran(ψ[σX.ψ/X]).

算法AND用于处理∧操作符.令ϕψ为该算法的输入参数.由算法PFTran可以看出, ϕψ均为PF式.若ϕ形如∨i(ϕi∧◯χi), ψ形如∨k(ψk∧◯gk), 那么算法AND返回∨ik(ϕiψk∧◯(χiγk)).接下来给出用算法PFTran将公式Ψ:νZ.(p∧◯Z)∧ μX.(q∨◯X)∨νY.(r∧◯◯Y) 转化为PF式的过程.

$\begin{array}{l} PFTran(\nu Z.(p \wedge \bigcirc Z) \wedge \mu X.(q \vee \bigcirc X) \vee \nu Y.(r \wedge \bigcirc \bigcirc Y)) \equiv \hfill \\ PFTran(\nu Z.(p \wedge \bigcirc Z) \wedge \mu X.(q \vee \bigcirc X)) \vee PFTran \\(\nu Y.(r \wedge \bigcirc \bigcirc Y)) \equiv \hfill \\ AND(PFTran(\nu Z.(p \wedge \bigcirc Z)), PFTran(\mu X.(q \vee \bigcirc X))) \vee PFTran \\(r \wedge \bigcirc \bigcirc \nu Y.(r \wedge \bigcirc \bigcirc Y)) \equiv \hfill \\ AND(PFTran(p \wedge \bigcirc \nu Z.(p \wedge \bigcirc Z)), PFTran(q \vee \bigcirc \mu X.(q \vee \bigcirc X))) \\ \vee r \wedge \bigcirc \bigcirc \nu Y.(r \wedge \bigcirc \bigcirc Y) \equiv \hfill \\ AND(p \wedge \bigcirc \nu Z.(p \wedge \bigcirc Z), PFTran(q) \vee PFTran(\bigcirc \mu X.(q \vee \bigcirc X))) \\ \vee r \wedge \bigcirc \bigcirc \nu Y.(r \wedge \bigcirc \bigcirc Y) \equiv \hfill \\ AND(p \wedge \bigcirc \nu Z.(p \wedge \bigcirc Z), q \wedge \bigcirc true \vee true \wedge \bigcirc \mu X. \\(q \vee \bigcirc X)) \vee r \wedge \bigcirc \bigcirc \nu Y.(r \wedge \bigcirc \bigcirc Y) \equiv \hfill \\ p \wedge q \wedge \bigcirc \nu Z.(p \wedge \bigcirc Z) \vee p \wedge \bigcirc (\nu Z.(p \wedge \bigcirc Z) \\ \wedge \mu X.(q \vee \bigcirc X)) \vee r \wedge \bigcirc \bigcirc \nu Y.(r \wedge \bigcirc \bigcirc Y). \hfill \\ \end{array} $
3.4 PFG构造

对于一个给定的输入ϕ, PFG构造模块首先调用PF式转化模块, 将ϕ转化为PF式, 并据此生成新的节点和边.此后, 继续调用PF式转化模块, 将新生成的节点再分别转化为PF式, 并重复上述过程, 直至没有新的节点产生.此外, 在向PFG中添加边时, 通过检查PF式中未来部分的各个合取项, 还需添加相应的记号, 用以追踪不动点的展开情况.

值得注意的是:在构造PFG的过程中, 可能会产生false节点, 例如p∧﹁p.这些节点对应公式闭包的不一致性子集, 公式的模型无法由这些节点产生.因此, 在PFG构造过程的最后, 还需删除这些节点以及相关的边.接下来给出构造公式Ψ:νZ.(p∧◯Z)∧ μX.(q∨◯X)∨νY.(r∧◯◯Y) 的PFG (如图 4所示) 的过程.

Fig. 4 PFG of formula Ψ 图 4 公式Ψ的PFG

●  首先创建根节点νZ.(p∧◯Z)∧ μX.(q∨◯X)∨νY.(r∧◯◯Y), 记作n0;

●  然后, 将根节点转化为PF式:n0pq∧◯nZ.(p∧◯Z)∨p∧◯(νZ.(p∧◯Z)∧ μX.(q∨◯X))∨r∧◯◯νY.(r∧◯◯Y), 并据此生成新的节点:νZ.(p∧◯Z), νZ.(p∧◯Z)∧ μX.(q∨◯X) 和◯nY.(r∧◯◯Y), 分别记作n1, n2n3.与此同时, 还要生成相应的边:(n0, pq, n1), (n0, p, n2) 和 (n0, r, n3), 它们的记号分别为{Z}, {Z, X}和{Y};

●  之后, 将节点n1转化为PF式:n1p∧◯nZ.(p∧◯Z), 并据此创建边 (n1, p, n1), 记号为{Z}.需要注意的是, 此时没有新节点产生.类似地, 对于节点n2, 可生成边 (n2, p, n2) 和 (n2, pq, n1), 它们的记号分别为{Z, X}和{Z};

●  在此之后, 将节点n3转化为PF式:n3≡true∧◯nY.(r∧◯◯Y), 并据此生成节点n4:νY.(r∧◯◯Y) 以及边 (n3, true, n4), 记号为{Y};

●  最后, 对于节点n4, 可生成边 (n4, r, n3), 记号为{Y}.此时无新节点产生.

至此, 所有节点均已被处理, 整个构造过程结束.

3.5 ν-路径搜索

为了判断在一个PFG中是否存在ν-路径, 需要储存一个边序列.在实际中, 为节省空间消耗, 通常先对该PFG用Tarjan算法[25]进行强连通分量分解, 然后再从某个强连通分量中找出一个对应于ν-路径的环.

给定一个PFG.令scc为该PFG中的一个强连通分量, uscc中一个任意节点.ν-路径搜索模块能够构造一条始于节点u的潜在ν-路径.在此过程中, 需要使用全局变量ES, 用于存储scc中的一个边序列.该模块首先将scc中一条以u为源节点且未被访问过的边e加入至ES.接着, 按深度优先搜索方式继续向ES中添加其他未被访问的边.每当向ES中添加一条边后, 都需要判断当前ES中是否存在一个环:若存在, 且该环对应于一条n-路径, 则搜索过程结束; 否则, 需要删除ES中的最后一条边, 然后搜索其他路径.当scc中的所有边都被访问过时, 搜索过程结束.若一个PFG中的所有强连通分量里均不存在对应于ν-路径的环, 则说明给定公式是不可满足的.

在由工具NuTL2PFG生成的PFG中, 若在某个强连通分量里找到了一个对应于ν-路径的环, 那么, 任意终止于该环的路径 (即ν-路径) 均描述一个满足给定公式的模型.如果生成的PFG中不存在上述环, 则表明给定公式是不可满足的.

对于公式Ψ:νZ.(p∧◯Z)∧ μX.(q∨◯X)∨νY.(r∧◯◯Y), 由NuTL2PFG为其生成的PFG如图 4所示.环 (n1, p)ω为对

应于ν-路径的环, 因此, 该公式是可满足的.公式Ψ表示原子命题p总是成立且q最终成立, 或r在偶数时刻成立.图 4中任意终止于环 (n1, p)ω的路径均对应满足公式Ψ的模型.例如, 路径n0, pq, (n1, p)ω对应的模型为{p, q}, {p}ω.由此可见:通过PFG, 能够更直观地反映出为什么一个公式是可满足的.

4 实验与分析

文献[13]中给出了针对νTL判定问题的当前唯一可用的工具PS4NuTL.在该文献中, 共对以下3类公式进行了有效性验证 (实验环境为1G内存PC):Includen, NesternCountern.

$\begin{array}{l} Includ{e_n} \equiv \nu X.(\underbrace {q \wedge \bigcirc (q \wedge \bigcirc (...\bigcirc (q}_{2n{\text{ }}times} \wedge \bigcirc (\neg q \wedge \bigcirc X))...))) \to \nu Z.\mu Y.\\(\neg q \wedge \bigcirc Z \vee q \wedge \bigcirc (q \wedge \bigcirc Y)), \hfill \\ Neste{r_n} \equiv \psi \vee \neg \psi, 其中, \psi \equiv \mu {X_1}.\nu {X_2}.\mu {X_3}....\sigma {X_n}.\\({q_1} \vee \bigcirc ({X_1} \wedge ({q_2} \vee \bigcirc ({X_2} \wedge ...({q_n} \vee \bigcirc {X_n})...)))), \hfill \\ Counte{r_n} \equiv \vee _{i = 0}^n\neg {c_i} \vee \mu X.(\bigcirc X \vee ({c_0} \nleftrightarrow \bigcirc \neg {c_0}) \vee \vee _{i = 1}^n(\bigcirc {c_i} \nleftrightarrow {c_i} \wedge \neg {c_{i - 1}} \vee {c_{i - 1}} \wedge (\bigcirc {c_{i - 1}} \leftrightarrow {c_i}))). \hfill \\ \end{array} $

为了与文献[13]中的实验结果进行对比, 我们用工具NuTL2PFG分别检查﹁Includen, ﹁Nestern和﹁Countern的可满足性.实验环境为1.73GHz, Genuine Intel (R) CPU T2080, 1G内存PC.实验结果见表 1.在表 1中, 第1列表示公式中下标n的大小; 节点数和边数所在列分别表示生成的相应公式的PFG中的节点数和边数, 单位为个; 时间所在列表示判断公式可满足性所需时间, 单位为ms.

Table 1 Experimental result 表 1 实验结果

文献[13]指出, 用PS4NuTL检测各个公式有效性的运行时间均为几分钟.此外, 在处理公式Nester4, Nester5Counter5时还遇到了内存溢出问题.这是因为, 在文献[13]所用的方法中, 除了需要构造公式的证明树之外, 还要通过构造自动机来检测最小不动点的非良基性.然而, 本文方法仅需为公式构造PFG, 并根据PFG中的记号便可检测最小不动点的非良基性.因此, NuTL2PFG比PS4NuTL的执行效率更高.

5 结束语

作为一种语法简洁表达能力强的逻辑, νTL在程序验证领域具有举足轻重的地位.然而, 不动点操作符的嵌套使其判定问题难以得到有效解决, 妨碍了其在实际中的进一步应用.针对这一问题, 本文开发了νTL公式的可满足性判定工具NuTL2PFG.利用νTL公式的PF式、PFG以及PFG中的ν-路径等概念, NuTL2PFG通过为一个给定公式构造PFG并从该PFG中找出一条ν-路径, 进而判定该公式的可满足性.此外, 本文通过实验证明了NuTL2PFG在实践中的可用性和高效性.未来有两方面的工作有待进一步研究:一方面, 我们可以通过比较节点的所有出边的记号, 从而更快地构造出ν-路径, 以此提升NuTL2PFG的性能; 另一方面, 我们将在NuTL2PFG的基础上开发基于PFG的νTL模型检测工具.

参考文献
[1] Barringer H, Kuiper R, Pnueli A. A really abstract concurrent model and its temporal logic. In:Proc. of the POPL'86. New York:ACM Press, 1986. 173-183.[doi:10.1145/512644.512660]
[2] Kozen D. Results on the propositional μ-calculus. Theoretical Computer Science, 1983, 27(3): 333–354. [doi:10.1016/0304-3975(82)90125-6]
[3] Pnueli A. The temporal logic of programs. In:Proc. of the FOCS'77. New York:IEEE Computer Society, 1977. 46-57.[doi:10.1109/SFCS.1977.32]
[4] Barringer H, Kuiper R, Pnueli A. Now you may compose temporal logic specifications. In:DeMillo RA, ed. Proc. of the STOC'84. New York:ACM Press, 1984. 51-63.[doi:10.1145/800057.808665]
[5] Emerson EA, Clarke EM. Characterizing correctness properties of parallel programs using fixpoints. In:de Bakker JW, van Leeuwen J, eds. Proc. of the ICALP'80. LNCS 85, Heidelberg:Springer-Verlag, 1980. 169-181.[doi:10.1007/3-540-10003-2_69]
[6] Vardi MY. A temporal fixpoint calculus. In:Ferrante J, Mager P, eds. Proc. of the POPL'88. New York:ACM Press, 1988. 250-259.[doi:10.1145/73560.73582]
[7] Sistla AP, Clarke EM. The complexity of propositional linear temporal logics. Journal of the Association for Computing Machinery, 1985, 32(3): 733–749. [doi:10.1145/3828.3837]
[8] Streett RS, Emerson EA. An automata theoretic decision procedure for the propositional mu-calculus. Information and Computation, 1989, 81(3): 249–264. [doi:10.1016/0890-5401(89)90031-X]
[9] Stirling C, Walker D. CCS, liveness, and local model checking in the linear time mu-calculus. In:Sifakis J, ed. Proc. of the AVMFSS'89. LNCS 407, Heidelberg:Springer-Verlag, 1990. 166-178.[doi:10.1007/3-540-52148-8_14]
[10] Kaivola R. A simple decision method for the linear time mu-calculus. In:Desel J Dr. rer. nat, ed. Proc. of the STRICT'95. London:Springer-Verlag, 1995. 190-204.[doi:10.1007/978-1-4471-3078-9_13]
[11] Bradfield J, Esparza J, Mader A. An effective tableau system for the linear time mu-calculus. In:Meyer F, Monien B, eds. Proc. of the ICALP'96. LNCS 1099, Heidelberg:Springer-Verlag, 1996. 98-109.[doi:10.1007/3-540-61440-0_120]
[12] Banieqbal B, Barringer H. Temporal logic with fixed points. In:Banieqbal B, Barringer H, Pnueli A, eds. Proc. of the Temporal Logic in Specification'87. LNCS 398, Heidelberg:Springer-Verlag, 1989. 62-74.[doi:10.1007/3-540-51803-7_22]
[13] Dax C, Hofmann M, Lange M. A proof system for the linear time mu-calculus. In:Arun-Kumar S, Garg N, eds. Proc. of the FSTTCS 2006. LNCS 4337, Heidelberg:Springer-Verlag, 2006. 274-285.[doi:10.1007/11944836_26]
[14] Liu Y, Duan ZH, Tian C, Liu B. Present-Future form of linear time mu-calculus. In:Liu SY, Duan ZH, eds. Proc. of the SOFL+ MSVL 2013. LNCS 8332, Switzerland:Springer Int'l Publishing, 2014. 76-85.[doi:10.1007/978-3-319-04915-1_6]
[15] Liu Y, Duan ZH, Tian C. An improved decision procedure for linear time mu-calculus. arXiv preprint arXiv:1507.05513, 2015.
[16] Duan ZH. An extended interval temporal logic and a framing technique for temporal logic programming[Ph.D. Thesis]. Newcastle upon Tyne:University of Newcastle upon Tyne, 1996.
[17] Duan ZH. Temporal Logic and Temporal Logic Programming. Beijing: Science Press, 2005.
[18] Duan ZH, Tian C. Decidability of propositional projection temporal logic with infinite models. In:Cai JY, Cooper SB, Zhu H, eds. Proc. of the TAMC 2007. LNCS 4484, Heidelberg:Springer-Verlag, 2007. 521-532.[doi:10.1007/978-3-540-72504-6_47]
[19] Duan ZH, Tian C. An improved decision procedure for propositional projection temporal logic. In:Dong JS, Zhu HB, eds. Proc. of the ICFEM 2010. LNCS 6447, Heidelberg:Springer-Verlag, 2010. 90-105.[doi:10.1007/978-3-642-16901-4_8]
[20] Duan ZH, Tian C. A practical decision procedure for propositional projection temporal logic with infinite models. Theoretical Computer Science, 2014, 554: 169–190. [doi:10.1016/j.tcs.2014.02.011]
[21] Stirling C. Modal and temporal logics. Technical Report, ECS-LFCS-91-157, University of Edinburgh, Department of Computer Science, Laboratory for Foundations of Computer Science, 1991.
[22] Walukiewicz I. Completeness of Kozen's axiomatisation of the propositional μ-calculus. Information and Computation, 2000, 157(1): 142–182. [doi:10.1006/inco.1999.2836]
[23] Bruse F, Friedmann O, Lange M. On guarded transformation in the modal μ-calculus. Logic Journal of the IGPL, 2015, 23(2): 194–216. [doi:10.1093/jigpal/jzu030]
[24] Fischer MJ, Ladner RE. Propositional dynamic logic of regular programs. Journal of Computer and System Sciences, 1979, 18(2): 194–211. [doi:10.1016/0022-0000(79)90046-1]
[25] Tarjan R. Depth-First search and linear graph algorithms. SIAM Journal on Computing, 1972, 1(2): 146–160. [doi:10.1137/0201010]