擴展命題區(qū)間時序邏輯公式可滿足性判定算法

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

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

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

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

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

1.1 語法

1.2 語義

1.3 導出公式

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

2 EPITL正則形算法

3 EPITL可滿足性的判定

3.1 EPITL正則圖(NFG)

圖1 NFG圖

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

3.2 EPITL公式可滿足性的判定

定理 4 對公式R的正則圖G，R有窮可滿足當且僅當G中存在有窮路徑。

定理 5 對公式R的正則圖G，R無窮可滿足當且僅當G中存在無窮路徑。

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

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

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

4 復雜度分析

定理 6 算法3最壞情況下的時間復雜度為非初等。

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

定理 7 非初等時間復雜度算法的空間復雜度必為非初等。

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

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

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

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

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

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

6 結(jié) 論

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

區(qū)間邏輯具非初等復雜度的判定問題仍可在驗證實踐中被使用[1]。下一步將在EPITL驗證算法的基礎(chǔ)上，開發(fā)基于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.