李永明

（陜西師范大學(xué) 計(jì)算機(jī)科學(xué)學(xué)院，陜西 西安 710119）

模型檢測(cè)（Model Checking）［1］是一種重要的形式化驗(yàn)證方法，主要包括計(jì)算樹(shù)邏輯（CTL）模型檢測(cè)、時(shí)序邏輯（LTL）模型檢測(cè)、μ－演算模型檢測(cè)等.由于其可自動(dòng)實(shí)現(xiàn)，已在實(shí)際系統(tǒng)中得到成功應(yīng)用［1－2］.

經(jīng)典的模型檢測(cè)針對(duì)的系統(tǒng)模型是布爾的，驗(yàn)證的性質(zhì)也是布爾的.但現(xiàn)實(shí)的系統(tǒng)尤其是計(jì)算機(jī)硬件系統(tǒng)和軟件系統(tǒng)常處在不確定環(huán)境中，這勢(shì)必影響系統(tǒng)的建模及驗(yàn)證.為處理此類(lèi)系統(tǒng)的驗(yàn)證問(wèn)題，一類(lèi)定量的模型檢測(cè)算法被提出.這包括概率模型檢測(cè)［2］、多值模型檢測(cè)［3］等.針對(duì)信息的不完備性和模糊性對(duì)應(yīng)的描述不確定性的可能性理論，作者最近提出了可能模型檢測(cè)方法［4－7］，得到許多好的性質(zhì)與應(yīng)用.并在可能性理論下研究了定性的線性時(shí)序性質(zhì)的模型檢測(cè)問(wèn)題［4］.但可能性理論下定量的LTL模型檢測(cè)問(wèn)題并未展開(kāi)研究，本文擬在此方面開(kāi)展初步的工作.

1 GPoLTL及兩種模型檢測(cè)語(yǔ)義

本節(jié)介紹可能LTL模型檢測(cè)的兩種語(yǔ)義.首先給出可能LTL模型檢測(cè)的模型——廣義的可能Kripke結(jié)構(gòu)，如下:

定義1［7］廣義的可能Kripke結(jié)構(gòu)（簡(jiǎn)記為GPKS）是一個(gè)五元組M＝（S，P，I，AP，L），其中

（1）S為可數(shù)非空的狀態(tài)集；

（2）P:S×S→［0，1］是一個(gè)函數(shù)，稱(chēng)為可能轉(zhuǎn)移分布函數(shù)；

（3）I:S→［0，1］是一個(gè)函數(shù)，稱(chēng)為可能初始分布函數(shù)；

（4）AP為原子命題集合；

（5）L:S→［0，1］AP為可能加標(biāo)函數(shù)，將一個(gè)狀態(tài)s映射到原子命題AP上的模糊子集，其中［0，1］AP表示從集合AP到單位區(qū)間［0，1］上的函數(shù)全體構(gòu)成的集合，該集合上的元素即集合AP到單位區(qū)間［0，1］上的函數(shù)也稱(chēng)為集合AP上的模糊子集，表示原子命題在狀態(tài)s成立的可能性，即L（s）（a）表示原子命題a在狀態(tài)s成立的可能性或真度.

進(jìn)一步，若集合S和AP都是有限集，則稱(chēng)M＝（S，P，I，AP，L）為有限的.本文的 GPKS都是有限的.

（2）可能分布函數(shù)P:S×S→［0，1］可以用模糊矩陣表示.方便起見(jiàn)，該模糊矩陣記為P，即P＝（P（s，t））s，t∈S，P也稱(chēng)為M的模糊轉(zhuǎn)移矩陣.對(duì)模糊矩陣P，其傳遞閉包記為P＋.當(dāng)S為有限集，設(shè)集合S有N個(gè)元素，即，N＝｜S｜，則P＋＝P∨P2∨…∨PN，其中Pk＋1＝Pk?P.這里，用“?”表示模糊矩陣的max-min復(fù)合［8］.對(duì)一個(gè)模糊矩陣P，其反射傳遞閉包，記為P＊，定義為P＊＝P0∨P＋，其中P0表示恒等矩陣.

對(duì)一個(gè)廣義可能 Kripke結(jié)構(gòu)M＝（S，P，I，AP，L），利用P＋和P＊，可以得到兩個(gè)廣義可能Kripke結(jié)構(gòu)M＋＝（S，P＋，I，AP，L），M＊＝（S，P＊，I，AP，L）.

對(duì)一個(gè)GPKSM，其路徑定義為無(wú)窮狀態(tài)序列π＝s0s1s2…∈Sw，滿(mǎn)足對(duì)任意的i，P（si，si＋1）＞0.令Paths（M）表示M中的所有路徑構(gòu)成的集合，而Pathsfin（M）表示M中的所有有窮路徑的集合.用Paths（s）表示M中所有從狀態(tài)s出發(fā)的無(wú)窮路徑全體構(gòu)成的集合.

定義2［7］對(duì)一個(gè) GPKSM，定義函數(shù)PoM:Paths（M）→［0，1］如下:

其中π＝s0s1…∈Paths（M）.進(jìn)一步，對(duì)于E?Paths（M），定義

則得到函數(shù) PoM:2Paths（M）→［0，1］.PoM稱(chēng)為 Ω＝2Paths（M）上的廣義可能性測(cè)度，因?yàn)槠錆M(mǎn)足定理2.若M自明，則PoM簡(jiǎn)記為Po.

對(duì)一個(gè)廣義可能Kripke結(jié)構(gòu)M，定義本文常用的函數(shù)rP:S→［0，1］如下，其代表M中從s出發(fā)的路徑的最大可能性，

下面是rP的計(jì)算公式.

定理1［7］對(duì)一個(gè)廣義的Kripke結(jié)構(gòu)M，狀態(tài)s，有

用模糊矩陣表示為

其中D＝（P＋（t，t））t∈S.

定理2［7］對(duì)一個(gè)廣義的Kripke結(jié)構(gòu)M，Po是Ω＝2Paths（M）上的廣義可能性測(cè)度，其滿(mǎn)足如下條件:

下面給出用于描述系統(tǒng)性質(zhì)的廣義可能LTL語(yǔ)構(gòu)與語(yǔ)義定義.

定義3 （GPoLTL的語(yǔ)構(gòu)定義）廣義可能LTL公式（簡(jiǎn)記為GPoLTL）的語(yǔ)構(gòu)按如下的BNF范式來(lái)定義:

其中a∈AP.

其他路徑公式可以如下方式誘導(dǎo):

從上述定義可見(jiàn)，GPoLTL的語(yǔ)構(gòu)和LTL的語(yǔ)構(gòu)是完全一致的，他們的區(qū)別主要表現(xiàn)在其語(yǔ)義上.

定義4 （GPoLTL的路徑語(yǔ)義）設(shè)M＝（S，P，I，AP，L）是一個(gè)廣義可能Kripke結(jié)構(gòu)，φ為GPoLTL公式，其在M上的語(yǔ)義是Paths（M）的模糊子集，即‖φ‖M:Paths（M）→［0，1］，歸納定義如下:對(duì)π∈Paths（M），令π＝s0s1s2…，πj＝sjsj＋1…，則

定義5 （GPoLTL的語(yǔ)言語(yǔ)義）設(shè)φ為GPoLTL公式，l為單位區(qū)間［0，1］的有限子集.則φ的語(yǔ)言語(yǔ)義為字符集lAP上的ω－語(yǔ)言的模糊子集，即‖φ‖:（lAP）ω→［0，1］，其歸納定義如下:令σ＝A0A1…∈（lAP）ω，σj＝AjAj＋1…，則

這兩種語(yǔ)義的明顯區(qū)別是，路徑語(yǔ)義與模型有關(guān)，而語(yǔ)言語(yǔ)義與模型無(wú)關(guān).但本文將要證明，實(shí)際上這兩種語(yǔ)義是有關(guān)聯(lián)的.

利用這兩種語(yǔ)義，可以定義一個(gè)廣義可能Kripke結(jié)構(gòu)M滿(mǎn)足可能LTL路徑公式φ的程度如下.

按路徑語(yǔ)義，M滿(mǎn)足φ的程度，記做MCP（M，φ），定義為

為定義語(yǔ)言語(yǔ)義下的模型檢測(cè)問(wèn)題，需要定義一個(gè)廣義可能Kripke結(jié)構(gòu)M的跡函數(shù)，其可以定義為一個(gè)模糊 Büchi自動(dòng)機(jī)［9－10］接受的語(yǔ)言，該模糊自動(dòng)機(jī)記為AM，構(gòu)造如下.

設(shè)M＝（S，AP，P，I，L），令l＝∪s∈SIm（L（s）），這里Im（L（s））表示函數(shù)L（s）的像集，即Im（L（s））＝｛L（s）（a）｜a∈AP｝，則l是有限集.定義字符集lAP上的模糊自動(dòng)機(jī)為 AM＝（S∪｛i｝，δ，｛i｝，S∪｛i｝），其中i?S.狀態(tài)轉(zhuǎn)移函數(shù)定義為，若A＝L（s2），則δ（s1，A，s2）＝P（s1，s2）；若A＝L（s），則δ（i，A，s）＝I（s）；其他情況下δ取值為0.AM接受的語(yǔ)言，記為‖AM‖，稱(chēng)為M的跡，記為 Traces（M）.這時(shí)，對(duì)σ＝A0A1A2…，Traces（M）（σ）＝ ‖AM‖ （σ）＝∨｛I（s）∧PoMs（π）｜L（π）＝σ｝.

按語(yǔ)言語(yǔ)義，M滿(mǎn)足φ的程度，記為MCL（M，φ），定義為

定理3MCP（M，φ）＝MCL（M，φ）.

2 GPoLTL公式的等價(jià)性及對(duì)應(yīng)模型檢測(cè)算法

從GPoLTL模型檢測(cè)問(wèn)題的定義看，對(duì)于一個(gè)GPKSM，和一個(gè)GPoLTL公式φ，關(guān)鍵是計(jì)算PoM（φ）.為此，先給出GPoLTL公式的范式.

定義6 對(duì)兩個(gè)GPoLTL公式φ1與φ2，定義φ1＝φ2當(dāng)且僅當(dāng)他們的語(yǔ)言語(yǔ)義一致，即對(duì)任意的有限集合l?［0，1］，‖φ1‖＝‖φ2‖:（lAP）ω→［0，1］.

定理4φ1≡φ2，當(dāng)且僅當(dāng)對(duì)任意的GPKSM，‖φ1‖M＝‖φ2‖M.

反之，若對(duì)任意GPKSM，‖φ1‖M＝‖φ2‖M，要證φ1≡φ2.對(duì)任意的有限集合l?［0，1］，取σ＝A0A1A2…∈（lAP）ω，要證‖φ1‖（σ）＝‖φ2‖（σ）.為此，構(gòu)造GPKSM＝（S，AP，P，I，L）如下:S＝lAP，P（Ai，Ai＋1）＝1，其他情況P（s，t）＝0；I任意定義；L（A）＝A.這時(shí)，對(duì)π＝σ＝A0A1…∈Paths（M）有L（π）＝σ.從而由‖φ1‖M＝‖φ2‖M知，‖φ1‖M（π）＝‖φ2‖M（π），由 此 可 知 ‖φ1‖ （L（π））＝‖φ2‖（L（π）），從而‖φ1‖（σ）＝‖φ2‖（σ）.則證φ1≡φ2.證畢.

定義7 （GPoLTL的正規(guī)范型）對(duì)a∈AP，GPoLTL的release正規(guī)范型（PNF）如下定義:

定理5 對(duì)任意GPoLTL公式φ，存在正規(guī)范型公式ψ，使得ψ≡φ，此構(gòu)造的時(shí)間復(fù)雜性為O（｜φ｜）.

這是由于如下公式成立，從而總可以把非運(yùn)算只作用在原子公式.

由于以上的規(guī)范型，以及定理4，對(duì)一個(gè)廣義可能Kripke結(jié)構(gòu)，只需要計(jì)算針對(duì)GPoLTL的正規(guī)范型公式φ的PoM（φ）（簡(jiǎn)記為Po（φ））的計(jì)算公式.針對(duì)φ的長(zhǎng)度｜φ｜遞歸計(jì)算如下:

當(dāng)φ＝false時(shí)，Po（φ）（s）＝0.

當(dāng)φ＝φ1φ2時(shí)，‖Po（φ1φ2）‖（s）＝（π）∧ ‖φ1φ2）‖ （π）＝P（s，s1）∧ … ∧P（sj－2，sj－1）∧（πj－1）∧‖φ1‖（πj－1）∧P（sj－1，sj）∧PoMsj（πj）∧‖φ2‖（πj）＝（Dφ1?P）＊?Po（φ2））（s）.其中Dφ1＝diag（Po（φ1）（s））s∈S.另外，簡(jiǎn)單計(jì)算可以證明 Po（φ）＝μZ.（Po（φ2）∨（Po（φ1）∧P?Z）），即，Po（φ）為函數(shù)f（Z）＝Po（φ2）∨（Po（φ1）∧P?Z））的最小不動(dòng)點(diǎn).

實(shí)現(xiàn)上述計(jì)算的算法如下:

算法1:計(jì)算不動(dòng)點(diǎn)

輸入:從狀態(tài)集合S上的可能性分布全體構(gòu)成的集合到其自身的映射f

輸出:不動(dòng)點(diǎn)f

算法2:GPoLTL模型檢測(cè)

輸入:一個(gè)GPKSM與GPoLTL公式φ

輸出:Po（φ）

這里，P＝ （P（s，t））s，t∈S，Dφ＝Diag（Po（φ）（s））s∈S，rP＝P＋?D，P＋＝P∨P2∨ … ∨PN，D＝（P＋（s，s））s∈S，P＊＝P0∨P＋，其中N＝｜S｜，P0表示N×N階恒等矩陣，fφ（Z）＝Po（φ2）∨（Po（φ1）∧P?Z），gφ（Z）＝Po（φ2）∧（Po（φ1）∨P?Z）.

從以上算法及其對(duì)應(yīng)的計(jì)算易知如下定理成立.

定理6 （GPoLTL模型檢測(cè)時(shí)間復(fù)雜性）對(duì)一個(gè)廣義的Kripke結(jié)構(gòu)M，及GPoLTL公式φ，GPoLTL模型檢測(cè)MCP（M，φ）時(shí)間復(fù)雜性為O（poly（｜S｜），exp（｜φ｜），其中｜φ｜表示φ的子公式個(gè)數(shù)，poly（N）表示N的多項(xiàng)式函數(shù).

3 結(jié)論

本文給出了廣義可能性測(cè)度下的LTL公式，并給出了其基于路徑和語(yǔ)言的兩種語(yǔ)義.在這兩種語(yǔ)義下，給出了LTL模型檢測(cè)問(wèn)題，并證明了其一致性.利用GPoLTL的正規(guī)范型，給出了GPoLTL模型檢測(cè)的算法和時(shí)間復(fù)雜性.

進(jìn)一步的工作包括GPoLTL模型檢測(cè)的基于自動(dòng)機(jī)的模型檢測(cè)算法以及一些有意義的應(yīng)用.

［1］Edmund E，Grumberg O，Peled D.Model checking［M］.Cambridge:The MIT Press，1999.

［2］Baier C，Katoen J P.Principles of model checking［M］.Cambridge:The MIT Press，2008.

［3］Chechik M，Devereux B，Gurfinkel A.Multi-valued symbolic model-checking［J］.ACM Transactions on Software Engineering and Methodology，2003，12（4）:371-408.

［4］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.

［5］Li Yongming，Li Yali，Ma Zhanyou.Computation tree logic model checking based on possibility measures［EB/OL］.［2014-09-15］.http://dx.doi.org/10.1016/j.fss.2014.03.009.

［6］李亞麗，李永明.可能性測(cè)度下的計(jì)算樹(shù)邏輯的若干性質(zhì)［J］.陜西師范大學(xué)學(xué)報(bào):自然科學(xué)版，2013，41（6）:6-11.

［7］Li Yongming，Ma Zhanyou.Quantitative computation tree logic model checking based on generalized possibility measures［EB/OL］.［2014-09-15］.http:∥arxiv.org/abs/1409.6466.

［8］李永明.模糊系統(tǒng)分析［M］.北京:科學(xué)出版社，2005.

［9］Kupferman O，Lustig Y.Lattice automata［C］∥Cook B，Podelski A.Proceedings of VMCAI2007，Lecture Notes in Computer Science，Berlin:Springer，2007:199-213.

［10］李永明.格值自動(dòng)機(jī)與語(yǔ)言［J］.陜西師范大學(xué)學(xué)報(bào):自然科學(xué)版，2003，31（4）:1-6.