可能LTL模型检测的两种方法

李永明

（陕西师范大学 计算机科学学院，陕西 西安 710119）

模型检测（Model Checking）［1］是一种重要的形式化验证方法，主要包括计算树逻辑（CTL）模型检测、时序逻辑（LTL）模型检测、μ－演算模型检测等.由于其可自动实现，已在实际系统中得到成功应用［1－2］.

经典的模型检测针对的系统模型是布尔的，验证的性质也是布尔的.但现实的系统尤其是计算机硬件系统和软件系统常处在不确定环境中，这势必影响系统的建模及验证.为处理此类系统的验证问题，一类定量的模型检测算法被提出.这包括概率模型检测［2］、多值模型检测［3］等.针对信息的不完备性和模糊性对应的描述不确定性的可能性理论，作者最近提出了可能模型检测方法［4－7］，得到许多好的性质与应用.并在可能性理论下研究了定性的线性时序性质的模型检测问题［4］.但可能性理论下定量的LTL模型检测问题并未展开研究，本文拟在此方面开展初步的工作.

1 GPoLTL及两种模型检测语义

本节介绍可能LTL模型检测的两种语义.首先给出可能LTL模型检测的模型——广义的可能Kripke结构，如下:

定义1［7］广义的可能Kripke结构（简记为GPKS）是一个五元组M＝（S，P，I，AP，L），其中

（1）S为可数非空的状态集；

（2）P:S×S→［0，1］是一个函数，称为可能转移分布函数；

（3）I:S→［0，1］是一个函数，称为可能初始分布函数；

（4）AP为原子命题集合；

（5）L:S→［0，1］AP为可能加标函数，将一个状态s映射到原子命题AP上的模糊子集，其中［0，1］AP表示从集合AP到单位区间［0，1］上的函数全体构成的集合，该集合上的元素即集合AP到单位区间［0，1］上的函数也称为集合AP上的模糊子集，表示原子命题在状态s成立的可能性，即L（s）（a）表示原子命题a在状态s成立的可能性或真度.

进一步，若集合S和AP都是有限集，则称M＝（S，P，I，AP，L）为有限的.本文的 GPKS都是有限的.

（2）可能分布函数P:S×S→［0，1］可以用模糊矩阵表示.方便起见，该模糊矩阵记为P，即P＝（P（s，t））s，t∈S，P也称为M的模糊转移矩阵.对模糊矩阵P，其传递闭包记为P＋.当S为有限集，设集合S有N个元素，即，N＝｜S｜，则P＋＝P∨P2∨…∨PN，其中Pk＋1＝Pk◦P.这里，用“◦”表示模糊矩阵的max-min复合［8］.对一个模糊矩阵P，其反射传递闭包，记为P＊，定义为P＊＝P0∨P＋，其中P0表示恒等矩阵.

对一个广义可能 Kripke结构M＝（S，P，I，AP，L），利用P＋和P＊，可以得到两个广义可能Kripke结构M＋＝（S，P＋，I，AP，L），M＊＝（S，P＊，I，AP，L）.

对一个GPKSM，其路径定义为无穷状态序列π＝s0s1s2…∈Sw，满足对任意的i，P（si，si＋1）＞0.令Paths（M）表示M中的所有路径构成的集合，而Pathsfin（M）表示M中的所有有穷路径的集合.用Paths（s）表示M中所有从状态s出发的无穷路径全体构成的集合.

定义2［7］对一个 GPKSM，定义函数PoM:Paths（M）→［0，1］如下:

其中π＝s0s1…∈Paths（M）.进一步，对于E⊆Paths（M），定义

则得到函数 PoM:2Paths（M）→［0，1］.PoM称为 Ω＝2Paths（M）上的广义可能性测度，因为其满足定理2.若M自明，则PoM简记为Po.

对一个广义可能Kripke结构M，定义本文常用的函数rP:S→［0，1］如下，其代表M中从s出发的路径的最大可能性，

下面是rP的计算公式.

定理1［7］对一个广义的Kripke结构M，状态s，有

用模糊矩阵表示为

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

定理2［7］对一个广义的Kripke结构M，Po是Ω＝2Paths（M）上的广义可能性测度，其满足如下条件:

下面给出用于描述系统性质的广义可能LTL语构与语义定义.

定义3 （GPoLTL的语构定义）广义可能LTL公式（简记为GPoLTL）的语构按如下的BNF范式来定义:

其中a∈AP.

其他路径公式可以如下方式诱导:

从上述定义可见，GPoLTL的语构和LTL的语构是完全一致的，他们的区别主要表现在其语义上.

定义4 （GPoLTL的路径语义）设M＝（S，P，I，AP，L）是一个广义可能Kripke结构，φ为GPoLTL公式，其在M上的语义是Paths（M）的模糊子集，即‖φ‖M:Paths（M）→［0，1］，归纳定义如下:对π∈Paths（M），令π＝s0s1s2…，πj＝sjsj＋1…，则

定义5 （GPoLTL的语言语义）设φ为GPoLTL公式，l为单位区间［0，1］的有限子集.则φ的语言语义为字符集lAP上的ω－语言的模糊子集，即‖φ‖:（lAP）ω→［0，1］，其归纳定义如下:令σ＝A0A1…∈（lAP）ω，σj＝AjAj＋1…，则

这两种语义的明显区别是，路径语义与模型有关，而语言语义与模型无关.但本文将要证明，实际上这两种语义是有关联的.

利用这两种语义，可以定义一个广义可能Kripke结构M满足可能LTL路径公式φ的程度如下.

按路径语义，M满足φ的程度，记做MCP（M，φ），定义为

为定义语言语义下的模型检测问题，需要定义一个广义可能Kripke结构M的迹函数，其可以定义为一个模糊 Büchi自动机［9－10］接受的语言，该模糊自动机记为AM，构造如下.

设M＝（S，AP，P，I，L），令l＝∪s∈SIm（L（s）），这里Im（L（s））表示函数L（s）的像集，即Im（L（s））＝｛L（s）（a）｜a∈AP｝，则l是有限集.定义字符集lAP上的模糊自动机为 AM＝（S∪｛i｝，δ，｛i｝，S∪｛i｝），其中i∉S.状态转移函数定义为，若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公式的等价性及对应模型检测算法

从GPoLTL模型检测问题的定义看，对于一个GPKSM，和一个GPoLTL公式φ，关键是计算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‖（σ）.为此，构造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的正规范型）对a∈AP，GPoLTL的release正规范型（PNF）如下定义:

定理5 对任意GPoLTL公式φ，存在正规范型公式ψ，使得ψ≡φ，此构造的时间复杂性为O（｜φ｜）.

这是由于如下公式成立，从而总可以把非运算只作用在原子公式.

由于以上的规范型，以及定理4，对一个广义可能Kripke结构，只需要计算针对GPoLTL的正规范型公式φ的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（φ）为函数f（Z）＝Po（φ2）∨（Po（φ1）∧P◦Z））的最小不动点.

实现上述计算的算法如下:

算法1:计算不动点

输入:从状态集合S上的可能性分布全体构成的集合到其自身的映射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）.

从以上算法及其对应的计算易知如下定理成立.

定理6 （GPoLTL模型检测时间复杂性）对一个广义的Kripke结构M，及GPoLTL公式φ，GPoLTL模型检测MCP（M，φ）时间复杂性为O（poly（｜S｜），exp（｜φ｜），其中｜φ｜表示φ的子公式个数，poly（N）表示N的多项式函数.

3 结论

本文给出了广义可能性测度下的LTL公式，并给出了其基于路径和语言的两种语义.在这两种语义下，给出了LTL模型检测问题，并证明了其一致性.利用GPoLTL的正规范型，给出了GPoLTL模型检测的算法和时间复杂性.

进一步的工作包括GPoLTL模型检测的基于自动机的模型检测算法以及一些有意义的应用.

［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］李亚丽，李永明.可能性测度下的计算树逻辑的若干性质［J］.陕西师范大学学报:自然科学版，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］李永明.模糊系统分析［M］.北京:科学出版社，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］.陕西师范大学学报:自然科学版，2003，31（4）:1-6.