可能LTL模型檢測的兩種方法

李永明

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

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

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

1 GPoLTL及兩種模型檢測語義

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

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

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

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

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

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

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

進一步，若集合S和AP都是有限集，則稱M＝（S，P，I，AP，L）為有限的.本文的 GPKS都是有限的.

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

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

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

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

其中π＝s0s1…∈Paths（M）.進一步，對于E?Paths（M），定義

則得到函數(shù) PoM:2Paths（M）→［0，1］.PoM稱為 Ω＝2Paths（M）上的廣義可能性測度，因為其滿足定理2.若M自明，則PoM簡記為Po.

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

下面是rP的計算公式.

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

用模糊矩陣表示為

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

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

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

定義3 （GPoLTL的語構(gòu)定義）廣義可能LTL公式（簡記為GPoLTL）的語構(gòu)按如下的BNF范式來定義:

其中a∈AP.

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

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

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

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

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

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

按路徑語義，M滿足φ的程度，記做MCP（M，φ），定義為

為定義語言語義下的模型檢測問題，需要定義一個廣義可能Kripke結(jié)構(gòu)M的跡函數(shù)，其可以定義為一個模糊 Büchi自動機［9－10］接受的語言，該模糊自動機記為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上的模糊自動機為 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接受的語言，記為‖AM‖，稱為M的跡，記為 Traces（M）.這時，對σ＝A0A1A2…，Traces（M）（σ）＝ ‖AM‖ （σ）＝∨｛I（s）∧PoMs（π）｜L（π）＝σ｝.

按語言語義，M滿足φ的程度，記為MCL（M，φ），定義為

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

2 GPoLTL公式的等價性及對應(yīng)模型檢測算法

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

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

定理4φ1≡φ2，當且僅當對任意的GPKSM，‖φ1‖M＝‖φ2‖M.

反之，若對任意GPKSM，‖φ1‖M＝‖φ2‖M，要證φ1≡φ2.對任意的有限集合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.這時，對π＝σ＝A0A1…∈Paths（M）有L（π）＝σ.從而由‖φ1‖M＝‖φ2‖M知，‖φ1‖M（π）＝‖φ2‖M（π），由 此 可 知 ‖φ1‖ （L（π））＝‖φ2‖（L（π）），從而‖φ1‖（σ）＝‖φ2‖（σ）.則證φ1≡φ2.證畢.

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

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

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

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

當φ＝false時，Po（φ）（s）＝0.

當φ＝φ1φ2時，‖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.另外，簡單計算可以證明 Po（φ）＝μZ.（Po（φ2）∨（Po（φ1）∧P?Z）），即，Po（φ）為函數(shù)f（Z）＝Po（φ2）∨（Po（φ1）∧P?Z））的最小不動點.

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

算法1:計算不動點

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

輸出:不動點f

算法2:GPoLTL模型檢測

輸入:一個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）.

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

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

3 結(jié)論

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

進一步的工作包括GPoLTL模型檢測的基于自動機的模型檢測算法以及一些有意義的應(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］李亞麗，李永明.可能性測度下的計算樹邏輯的若干性質(zhì)［J］.陜西師范大學(xué)學(xué)報:自然科學(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］李永明.格值自動機與語言［J］.陜西師范大學(xué)學(xué)報:自然科學(xué)版，2003，31（4）:1-6.