扩展命题区间时序逻辑公式可满足性判定算法

朱维军 ，邓淼磊，周清雷，张海宾

(1. 郑州大学信息工程学院 郑州 450001；2. 西安电子科技大学计算机学院 西安 710071；3. 河南工业大学信息科学与工程学院 郑州 450001)

模型检测技术是近年来研究的热点，已经在硬件与网络协议领域取得了大量的重要应用。其基本思想是，自动验证有穷状态空间是否满足需求的性质，经常采用自动机、Petri网或进程代数建立动态模型，静态性质则使用时序逻辑来表达。普通时序逻辑只能表达孤立点之间的时序性质，而区间时序逻辑(interval temporal logic，ITL)及其规范可执行子集Tempura语言[1]，则可通过chop算子实现对数字电路区间内状态之间以及区间之间时序关系性质的描述。ITL逻辑命题部分PITL公式的可有穷满足的判定算法[2]直到2003年才完成，然而由于非终止并发系统大多具无穷模型，因而很难在该判定算法基础上开发相应的模型检测工具。

针对该问题，扩展区间时序逻辑(extended interval temporal logic，EITL)[3-7]把区间从有穷扩展到无穷，与同类扩展ITL模型至无穷区间[8]相比，前者由于只允许最后区间具无穷模型，因而更适合真实的非终止并发系统。而EITL的规范可执行子集扩展Tempura语言[3,5]更使得规范可以通过执行的方式得到结果。然而，目前EITL满足性判定的方法问题仍未解决，本文对此进行研究。由于一阶部分不可判定，因此只考查命题部分(EPITL)。

1 扩展命题区间时序逻辑EPITL

1.1 语法

1.2 语义

1.3 导出公式

比较EPITL与命题投影时序逻辑(propositional projection temporal logic，PPTL)[9]的语法和语义，不难发现两种区间逻辑的区别：前者拥有两种区间算子chop(即“;”)和chop star(即“ϕ*”)；后者也有两种描述区间语义的算子chop和prj。由于chop star与prj无法互相表示，因而两种逻辑表达能力是相交非包含关系。为了得到EPITL判定算法，应考虑如何在PPTL判定算法[9]的基础上，去掉prj，加上chop star。而PITL判定算法[2]也未实现对chop star的判定。

2 EPITL正则形算法

3 EPITL可满足性的判定

3.1 EPITL正则图(NFG)

图1 NFG图

修改PPTL正则图算法[9]，根据正则形公式构造EPITL正则图的算法(算法2)如下：

3.2 EPITL公式可满足性的判定

定理 4 对公式R的正则图G，R有穷可满足当且仅当G中存在有穷路径。

定理 5 对公式R的正则图G，R无穷可满足当且仅当G中存在无穷路径。

定理4、定理5的证明是对正则形公式每个next推进步数归纳构造集合，对有穷情况做数学归纳，对无穷的情况构造不动点，这种证明与公式R的结构无关，因而可以直接把对PPTL的证明[9]用来证明EPITL的结论。

下面的算法CHECK在正则图上判定EPITL公式的可满足性。其中函数SIMPLIFY删除没有后继节点的非终止于ε的节点(这样的节点不在有穷模型上也不在无穷模型上)。定理4、定理5保证了判定算法的有效性和正确性。EPITL公式可满足性判定算法(算法3)如下：

例2 在图1中，以ε节点为终点的任一路径，均为公式的有穷模型，图中任一无穷路径，均为公式的无穷模型。路径与模型一一对应。

4 复杂度分析

定理 6 算法3最坏情况下的时间复杂度为非初等。

证明 文献[10]证明了对在字母表{0,1}上运行的具“+”“i”“¬”算子的任意正则表达式的判空问题的时间复杂度下限是非初等时间[10]。文献[1]将上述表达式用PITL公式表示，从而证明了PITL满足性判定问题的时间复杂度是非初等时间[1]。从表达能力上讲，EPITL⊇PITL，且本文给出了EPITL 满足性判定算法，因此EPITL满足性判定问题固有时间复杂度仍为非初等时间，即为算法3的时间复杂度。

定理 7 非初等时间复杂度算法的空间复杂度必为非初等。

推论 1 算法3最坏情况下的空间复杂度为非初等。

5 相关工作比较

在算法1和算法2的基础上，如果对正则图加上接受条件，就可以直接得到自动机，从而得到逻辑与自动机的转换算法。按照模型检测技术的一般原理，结合已经发展成熟的自动机求积算法与自动机语言判空算法[11]，就可直接得到EPITL模型检测算法。

由于EPITL的表达能力高于LTL，因而新算法对模型的验证能力高于已被广泛使用的SPIN等LTL验证工具。由于EPITL与PPTL的表达能力相交非包含，因而与已有的PPTL判定算法相比，本文的NFG算法具有验证chop star区间性质的能力。而这样的性质在表达程序循环结构时特别有效。为了证明新算法对可判定规范程序循环结构描述性质的验证能力，本文分别使用4种不同方法针对4类不同的有穷或无穷循环结构进行仿真验证，实验结果如表1和表2所示。

表1 4种方法对有穷循环结构的描述公式及验证结果

表2 4种方法对无穷循环结构的描述公式及验证结果

6 结 论

本文工作给出了EPITL逻辑公式可满足性的判定算法，从而为该逻辑的模型检测提供了核心方法。

区间逻辑具非初等复杂度的判定问题仍可在验证实践中被使用[1]。下一步将在EPITL验证算法的基础上，开发基于EPITL的SPIN验证工具，为著名的模型检测器SPIN提高验证能力。

[1] MOSZKOWSKI B. Reasoning about digital circuits[D].Palo Alto, California, USA: Department of Computer Science, Stanford University, 1983.

[2] BOWMAN H, THOMPSON S. A decision procedure and complete axiomatization of finite interval temporal logic with projection[J]. Journal of Logic and Computation, 2003,13(2):195-239.

[3] DUAN Z. Temporal logic and temporal logic programming[M]. Beijing: Science Press, 2005.

[4] DUAN Z, KOUTNY M, HOLT C. Projection in temporal logic programming[C]//Proceedings of 5th International Conference on Logic Programming and Automated Reasoning. London, UK: Springer, 1994, 333-344.

[5] DUAN Z. An extended interval temporal logic and a framing technique for temporal logic programming[D]. Tyne and Wear, UK: Department of Computing Science,University of Newcastle Upon Tyne, 1996.

[6] DUAN Z, YANG X, KOUTNY M. Framed temporal logic programming[J]. Science of Computer Programming, 2008,70(1): 31-61.

[7] DUAN Z, KOUTNY M A. Framed temporal logic programming language[J]. Journal of Computer Science and Technology, 2004, 19(3): 341-351,

[8] MOSZKOWSKI B. Compositional reasoning about projected and infinite time[C]//Proceedings of the First IEEE International Conference on Engineering of Complex Computer Systems (ICECCS’95). Fort Lauderdale, Florida,USA: IEEE Computer Society Press, 1995.

[9] DUAN Z, TIAN C, ZHANG L. A decision procedure for propositional projection temporal logic with infinite models[J]. Acta Informatica, 2008, 45(1): 43-78.

[10] STOCKMEYER L. The complexity of decision problems in automata theory and logic[D]. Cambridge,Massachusetts, USA: MIT, 1974.

[11] CLARKE E M, GRUMBERG O, PELED D A. Model checking [M]. Massachusetts: MIT Press, 1999.