朱維軍 ，鄧淼磊，周清雷，張海賓

(1. 鄭州大學(xué)信息工程學(xué)院 鄭州 450001；2. 西安電子科技大學(xué)計(jì)算機(jī)學(xué)院 西安 710071；3. 河南工業(yè)大學(xué)信息科學(xué)與工程學(xué)院 鄭州 450001)

模型檢測技術(shù)是近年來研究的熱點(diǎn)，已經(jīng)在硬件與網(wǎng)絡(luò)協(xié)議領(lǐng)域取得了大量的重要應(yīng)用。其基本思想是，自動(dòng)驗(yàn)證有窮狀態(tài)空間是否滿足需求的性質(zhì)，經(jīng)常采用自動(dòng)機(jī)、Petri網(wǎng)或進(jìn)程代數(shù)建立動(dòng)態(tài)模型，靜態(tài)性質(zhì)則使用時(shí)序邏輯來表達(dá)。普通時(shí)序邏輯只能表達(dá)孤立點(diǎn)之間的時(shí)序性質(zhì)，而區(qū)間時(shí)序邏輯(interval temporal logic，ITL)及其規(guī)范可執(zhí)行子集Tempura語言[1]，則可通過chop算子實(shí)現(xiàn)對(duì)數(shù)字電路區(qū)間內(nèi)狀態(tài)之間以及區(qū)間之間時(shí)序關(guān)系性質(zhì)的描述。ITL邏輯命題部分PITL公式的可有窮滿足的判定算法[2]直到2003年才完成，然而由于非終止并發(fā)系統(tǒng)大多具無窮模型，因而很難在該判定算法基礎(chǔ)上開發(fā)相應(yīng)的模型檢測工具。

針對(duì)該問題，擴(kuò)展區(qū)間時(shí)序邏輯(extended interval temporal logic，EITL)[3-7]把區(qū)間從有窮擴(kuò)展到無窮，與同類擴(kuò)展ITL模型至無窮區(qū)間[8]相比，前者由于只允許最后區(qū)間具無窮模型，因而更適合真實(shí)的非終止并發(fā)系統(tǒng)。而EITL的規(guī)范可執(zhí)行子集擴(kuò)展Tempura語言[3,5]更使得規(guī)范可以通過執(zhí)行的方式得到結(jié)果。然而，目前EITL滿足性判定的方法問題仍未解決，本文對(duì)此進(jìn)行研究。由于一階部分不可判定，因此只考查命題部分(EPITL)。

1 擴(kuò)展命題區(qū)間時(shí)序邏輯EPITL

1.1 語法

1.2 語義

1.3 導(dǎo)出公式

比較EPITL與命題投影時(shí)序邏輯(propositional projection temporal logic，PPTL)[9]的語法和語義，不難發(fā)現(xiàn)兩種區(qū)間邏輯的區(qū)別：前者擁有兩種區(qū)間算子chop(即“;”)和chop star(即“?*”)；后者也有兩種描述區(qū)間語義的算子chop和prj。由于chop star與prj無法互相表示，因而兩種邏輯表達(dá)能力是相交非包含關(guān)系。為了得到EPITL判定算法，應(yīng)考慮如何在PPTL判定算法[9]的基礎(chǔ)上，去掉prj，加上chop star。而PITL判定算法[2]也未實(shí)現(xiàn)對(duì)chop star的判定。

2 EPITL正則形算法

3 EPITL可滿足性的判定

3.1 EPITL正則圖(NFG)

圖1 NFG圖

修改PPTL正則圖算法[9]，根據(jù)正則形公式構(gòu)造EPITL正則圖的算法(算法2)如下：

3.2 EPITL公式可滿足性的判定

定理 4 對(duì)公式R的正則圖G，R有窮可滿足當(dāng)且僅當(dāng)G中存在有窮路徑。

定理 5 對(duì)公式R的正則圖G，R無窮可滿足當(dāng)且僅當(dāng)G中存在無窮路徑。

定理4、定理5的證明是對(duì)正則形公式每個(gè)next推進(jìn)步數(shù)歸納構(gòu)造集合，對(duì)有窮情況做數(shù)學(xué)歸納，對(duì)無窮的情況構(gòu)造不動(dòng)點(diǎn)，這種證明與公式R的結(jié)構(gòu)無關(guān)，因而可以直接把對(duì)PPTL的證明[9]用來證明EPITL的結(jié)論。

下面的算法CHECK在正則圖上判定EPITL公式的可滿足性。其中函數(shù)SIMPLIFY刪除沒有后繼節(jié)點(diǎn)的非終止于ε的節(jié)點(diǎn)(這樣的節(jié)點(diǎn)不在有窮模型上也不在無窮模型上)。定理4、定理5保證了判定算法的有效性和正確性。EPITL公式可滿足性判定算法(算法3)如下：

例2 在圖1中，以ε節(jié)點(diǎn)為終點(diǎn)的任一路徑，均為公式的有窮模型，圖中任一無窮路徑，均為公式的無窮模型。路徑與模型一一對(duì)應(yīng)。

4 復(fù)雜度分析

定理 6 算法3最壞情況下的時(shí)間復(fù)雜度為非初等。

證明 文獻(xiàn)[10]證明了對(duì)在字母表{0,1}上運(yùn)行的具“+”“i”“?”算子的任意正則表達(dá)式的判空問題的時(shí)間復(fù)雜度下限是非初等時(shí)間[10]。文獻(xiàn)[1]將上述表達(dá)式用PITL公式表示，從而證明了PITL滿足性判定問題的時(shí)間復(fù)雜度是非初等時(shí)間[1]。從表達(dá)能力上講，EPITL?PITL，且本文給出了EPITL 滿足性判定算法，因此EPITL滿足性判定問題固有時(shí)間復(fù)雜度仍為非初等時(shí)間，即為算法3的時(shí)間復(fù)雜度。

定理 7 非初等時(shí)間復(fù)雜度算法的空間復(fù)雜度必為非初等。

推論 1 算法3最壞情況下的空間復(fù)雜度為非初等。

5 相關(guān)工作比較

在算法1和算法2的基礎(chǔ)上，如果對(duì)正則圖加上接受條件，就可以直接得到自動(dòng)機(jī)，從而得到邏輯與自動(dòng)機(jī)的轉(zhuǎn)換算法。按照模型檢測技術(shù)的一般原理，結(jié)合已經(jīng)發(fā)展成熟的自動(dòng)機(jī)求積算法與自動(dòng)機(jī)語言判空算法[11]，就可直接得到EPITL模型檢測算法。

由于EPITL的表達(dá)能力高于LTL，因而新算法對(duì)模型的驗(yàn)證能力高于已被廣泛使用的SPIN等LTL驗(yàn)證工具。由于EPITL與PPTL的表達(dá)能力相交非包含，因而與已有的PPTL判定算法相比，本文的NFG算法具有驗(yàn)證chop star區(qū)間性質(zhì)的能力。而這樣的性質(zhì)在表達(dá)程序循環(huán)結(jié)構(gòu)時(shí)特別有效。為了證明新算法對(duì)可判定規(guī)范程序循環(huán)結(jié)構(gòu)描述性質(zhì)的驗(yàn)證能力，本文分別使用4種不同方法針對(duì)4類不同的有窮或無窮循環(huán)結(jié)構(gòu)進(jìn)行仿真驗(yàn)證，實(shí)驗(yàn)結(jié)果如表1和表2所示。

表1 4種方法對(duì)有窮循環(huán)結(jié)構(gòu)的描述公式及驗(yàn)證結(jié)果

表2 4種方法對(duì)無窮循環(huán)結(jié)構(gòu)的描述公式及驗(yàn)證結(jié)果

6 結(jié) 論

本文工作給出了EPITL邏輯公式可滿足性的判定算法，從而為該邏輯的模型檢測提供了核心方法。

區(qū)間邏輯具非初等復(fù)雜度的判定問題仍可在驗(yàn)證實(shí)踐中被使用[1]。下一步將在EPITL驗(yàn)證算法的基礎(chǔ)上，開發(fā)基于EPITL的SPIN驗(yàn)證工具，為著名的模型檢測器SPIN提高驗(yàn)證能力。

[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.