廣義可能性計算樹邏輯的兩種范式*

趙　杰，李永明

陜西師范大學 計算機科學學院，西安 710019

廣義可能性計算樹邏輯的兩種范式*

趙杰，李永明+

陜西師范大學 計算機科學學院，西安 710019

計算樹邏輯（computation tree logic，CTL）的范式在模型檢測方法中具有重要意義，但基于廣義可能性測度的計算樹邏輯的范式尚未有系統(tǒng)研究。為了進一步完善廣義可能性計算樹（generalized possibilistic computation tree logic，GPoCTL）理論，在現有的廣義可能性計算樹邏輯理論的基礎上，參考經典計算樹邏輯的范式，給出了廣義可能性計算樹邏輯的兩種不同的范式——正態(tài)范式（positive normal form，PNF）和存在范式（existential normal form，ENF），及其對應的語構和語義解釋。最后利用歸納假設法證明了任意的廣義可能性計算樹邏輯公式都有與之等價的PNF公式和ENF公式。

廣義可能性測度；計算樹邏輯；范式；模型檢測

1　引言

1981年由Clarke、Emerson等人提出了模型檢測方法，其作為一種形式化的自動驗證技術，已被廣泛應用于計算機軟硬件系統(tǒng)、通信協(xié)議、控制系統(tǒng)、安全認證協(xié)議中[1-4]。它的基本思想是：通過對系統(tǒng)狀態(tài)空間進行窮舉搜索來驗證系統(tǒng)是否滿足設計規(guī)范。模型檢測的一般步驟為：（1）抽象出系統(tǒng)的數學模型；（2）給出需要驗證的性質的語言描述；（3）通過模型檢測算法來計算系統(tǒng)是否滿足該性質，如果不滿足，則給出反例。

由于計算機軟硬件系統(tǒng)復雜性的不斷增加，模型中狀態(tài)存在很多需要量化的信息。基于此，一些學者提出了狀態(tài)遷移模型的量化擴展，如在狀態(tài)中加入時間[1]，或者在模型中考慮概率[1]、可能性[5]、多值[6-7]或者統(tǒng)計信息[8]。1965年控制論學者Zadeh提出了模糊集理論[9-12]。進一步，為了處理含有可能性測度量化信息的模型檢測，李永明等人提出了基于廣義可能性測度的模型檢測，形成了基于廣義可能性Kripke結構的模型檢測理論[13-15]。

在經典計算樹邏輯（computation tree logic，CTL）模型檢測中，不同的范式扮演著不同但十分重要的角色。一方面，在處理狀態(tài)爆炸時，可以使用符號模型檢測，其基本原理是將系統(tǒng)的狀態(tài)轉換關系用邏輯公式表示。二叉圖（binary decision diagram，BDD）是用以表示邏輯公式的重要手段，有序二插圖（order binary decision diagram，OBDD）作為布爾公式的一個規(guī)范的表示形式，比一般的傳統(tǒng)公式如析取公式及合取公式能夠更加緊湊地表示狀態(tài)轉換關系，以降低系統(tǒng)模型所需的內存空間[1-16]。而正態(tài)范式（positive normal form，PNF）可以有效地運用于OBDD的簡化過程。另一方面，在CTL模型檢測算法中，對于CTL公式的要求則為存在范式（existential normal form，ENF）公式[1]，這是由于ENF通過只處理邏輯詞?而不考慮邏輯詞?就可以計算出任意的CTL公式的結果，有效簡化了模型檢測算法，高效地得到結果。因此，GPoCTL（generalized possibilistic computation tree logic）范式對于GPoCTL模型檢測的研究也有著極其重要的價值與意義。然而，目前對于GPoCTL范式并沒有系統(tǒng)研究，文獻[14]給出了GPoCTL公式的語構及其語義，并討論了GPoCTL公式的一些基本性質，為GPoCTL理論奠定了基礎。本文在上述工作的基礎上，給出了GPoCTL公式的PNF和ENF的描述。

本文組織結構如下：第2章是預備知識；第3章引入PNF、ENF范式的語構和語義；第4章證明了任意的GPoCTL公式都有一個等價的PNF公式，以及任意的GPoCTL公式都有一個等價的ENF公式。

2　預備知識

本章給出一些基于廣義可能性測度的計算樹邏輯的概念，包括廣義可能性Kripke結構（generalized possibilistic Kripke structure，GPKS）、廣義可能性測度和GPoCTL等。詳見參考文獻[13-15]。

2.1廣義可能性Kripke結構

定義1[14]一個GPKS是一個五元組M=(S,P,I, AP,L)，其中：

（1）S是非空可數的狀態(tài)集合；

（2）P:S×S→[0,1]是可能性轉移函數，并且滿足對任意狀態(tài)s，存在狀態(tài)t，使得P(s,t)>0；

（3）I:S→[0,1]是可能性初始分布，滿足存在狀態(tài)s∈S，使I(s)>0；

（4）AP是一組原子命題的集合；

（5）L:S×AP→[0,1]是可能性標簽函數，?a∈AP,s∈S，有L(s,a)∈[0,1]，即為每個狀態(tài)賦一個AP的模糊集合。

如果S和AP都是有窮的集合，則稱M是有窮的GPKS。

（2）可能性轉移函數P:S×S→[0,1]可表示成一個模糊矩陣P=(P(s,t))s,t∈S，并稱P為M的模糊轉移矩陣。

上式中的“∨”表示上確界，“∧”表示下確界[13]。特別的P*定義為：P*=P0∨P+，其中P0表示單位矩陣。

（4）令Paths(M)表示M中所有狀態(tài)路徑π= s0s1s2…,滿足?i≥0,P(si,si+1)>0所構成的集合，用Paths(s)表示M中所有從狀態(tài)s出發(fā)的無窮路徑全體構成的集合。

2.2廣義可能性測度

2.3GPoCTL

3　GPoCTL的PNF范式和ENF范式

文獻[14]已對GPoCTL的語義做了詳細的解釋，下面給出其在PNF范式和ENF范式下的語構和語義解釋。

3.1GPoCTL的PNF范式的語法

3.2GPoCTL的ENF范式的語法

4　GPoCTL公式在PNF和ENF范式下的等價

5　結論

本文給出了廣義可能性測度下計算樹邏輯的兩種范式及其對應的語構和語義解釋，并證明了任意的GPoCTL公式都存在這兩種范式下與之等價的公式，為處理GPoCTL公式的轉換、GPoCTL模型檢測算法的實現以及狀態(tài)爆炸等問題打下了基礎，同時進一步完善了現有的廣義可能性模型檢測理論。

[1]Baier C,Katoen J P.Principles of model checking[M].Cambridge,USA:MIT Press,2008.

[2]Clark E,Grumberg O,Peled D.Model checking[M].Cambridge,USA:MIT Press,1999.

[3]Rozier K Y.Linear temporal logic symbolic model checking[J]. Computer Science Review,2011,5(2):163-203.

[4]Lin Huimin,Zhang Wenhui.Model checking:theories,techniques and applications[J].Chinese Journal of Electronics, 2002,30(12A):1907-1912.

[5]Li Yongming,Li Lijun.Model checking of linear-time properties based on possibility measure[J].IEEE Transactions on Fuzzy Systems,2013,21(5):842-854.

[6]Lei Lihui,Duan Zhenhua.An extended deterministic finite automata based on possibility measure[J].Journal of Software,2007,18(12):2980-2990.

[7]Chechik M,Devereux B,Easterbrook S,et al.Multi-valued symbolic model-checking[J].ACM Transactions on Software Engineering and Methodology,2003,12(4):371-408.

[8]Fischer D,Gradel E,Kaiser L.Model checking games for the quantitativeμ-calculus[J].Theory of Computing Systems, 2010,47(3):696-719.

[9]Kwiatkowska M,Norman G,Parker D.Stochastic model checking[M]//Formal Methods for Performance Evaluation. Berlin,Heidelberg:Springer,2007:220-270.

[10]Zadeh L A.Fuzzy sets[J].Information and control,1965,8 (3):338-353.

[11]Li Yongming.Analysis of fuzzy systems[M].Beijing:Science Press,2005.

[12]Wang Xizhao.Fuzzy measures and fuzzy integral and its application in the classification technique[M].Beijing:Science Press,2008.

[13]Li Yongming,Li Yali,Ma Zhanyou.Computation tree logic model checking based on possibility measures[J].Fuzzy Sets and Systems,2015,262:44-59.

[14]Li Yongming,Ma Zhanyou.Quantitative computation tree logic model checking based on generalized possibility measures[J].IEEE Transactions on Fuzzy Systems,2015,23 (6):2034-2047.

[15]Li Yali,Li Yongming.Some properties of computation tree logic under possibility measure[J].Journal of Shanxi Normal University:Natural Science Edition,2013,41(6):6-12. [16]Gu Tianlong,Xu Zhoubo.Ordered binary decision diagram and application[M].Beijing:Science Press,2009.

附中文參考文獻：

[4]林惠民,張文輝.模型檢測:理論,方法與應用[J].電子學報,2002,30(12A):1907-1912.

[6]雷麗暉,段振華.一種基于擴展有限自動機驗證組合Web服務的方法[J].軟件學報,2007,18(12):2980-2990.

[11]李永明.模糊系統(tǒng)分析[M].北京:科學出版社,2005.

[12]王熙照.模糊測度和模糊積分及在分類技術中的應用[M].北京:科學出版社,2008.

[15]李亞利,李永明.可能性測度下計算樹邏輯的若干性質[J].陜西師范大學學報:自然科學版,2013,41(6):6-12.

[16]古天龍,徐周波.有序二叉決策圖及應用[M].北京:科學出版社,2009.

ZHAO Jie was born in 1990.He is an M.S.candidate at Shaanxi Normal University.His research interest is model checking.

趙杰（1990—），男，陜西寶雞人，陜西師范大學碩士研究生，主要研究領域為模型檢測。

LI Yongming was born in 1966.He received the Ph.D.degree from Sichuan University in 1996.Now he is a professor and Ph.D.supervisor at Shaanxi Normal University.His research interests include intelligent computing,fuzzy system analysis,quantum logic and quantum information,etc.

李永明（1966—），男，陜西大荔人，1996年于四川大學獲得博士學位，1999年于西北工業(yè)大學博士后流動站出站，現為陜西師范大學教授、博士生導師，陜西師范大學圖書館館長，主要研究領域為計算智能，模糊系統(tǒng)分析，量子計算與量子邏輯等。

Two Normal Forms Based on Generalized Possibilistic Computation Tree Logic?

ZHAO Jie,LI Yongming+
College of Computer Science,Shaanxi Normal University,Xi’an 710019,China

E-mail:liyongm@snnu.edu.cn

Normal form of computation tree logic(CTL)plays an important role in model checking.But the normal forms of computation tree logic based on generalized possibilistic measure have not been researched systematically. For improving the generalized possibilistic computation tree logic(GPoCTL)theory,according to existing generalized possibilistic computation tree logic theory and normal forms of classical computation tree logic,this paper defines two normal forms—positive normal form(PNF)and existential normal form(ENF)based on generalized possibilistic computation tree logic,and gives the corresponding language structure and semantic interpretation.Finally,using inductive method,this paper proves that any GPoCTL formula can write into a normal form in PNF or ENF respectively.

generalized possibility measure;computation tree logic;normal form;model checking

2015-06,Accepted 2015-08.

10.3778/j.issn.1673-9418.1507053

A

TP301.2

*The National Natural Science Foundation of China under Grant Nos.11271237,61228305(國家自然科學基金).

CNKI網絡優(yōu)先出版:2015-08-13,http://www.cnki.net/kcms/detail/11.5602.TP.20150813.1653.006.html

ZHAO Jie,LI Yongming.Two normal forms based on generalized possibilistic computation tree logic.Journal of Frontiers of Computer Science and Technology,2016,10(10)：1475-1481.