广义可能性决策过程的计算树逻辑模型检测*

马占有，李永明

(1.陕西师范大学计算机科学学院，陕西 西安 710062；2.北方民族大学计算机科学与工程学院，宁夏 银川 750021)

广义可能性决策过程的计算树逻辑模型检测*

马占有1，2，李永明1

(1.陕西师范大学计算机科学学院，陕西 西安 710062；2.北方民族大学计算机科学与工程学院，宁夏 银川 750021)

模型检测作为一种形式化验证技术，已被广泛应用于各种并发系统的正确性验证。针对具有非确定性选择和广义可能性分布的并发系统，引入广义可能性决策过程作为此类系统的模型；给出描述其性质的规范语言广义可能性计算树逻辑的概念；研究此类系统的广义可能性计算树逻辑模型检测问题。结论表明，其模型检测算法的时间复杂度也为多项式时间。所获得的结果扩大了广义可能性测度在模型检测中的应用范围。

并发系统；广义可能性决策过程；广义可能性计算树逻辑；模型检测

1 引言

模型检测作为一种形式化的自动验证技术，自1981年由Clarke E等人[1]提出以来，在计算机软硬件设计、通信协议、安全协议、分布式算法的正确性和可靠性分析等方面取得了成功的应用[2～10]。

经典的模型检测技术主要用于验证系统的定性性质，近年来，许多学者开始关注系统的定量性质，提出了量化模型检测技术，而基于多值(模糊)逻辑的模型检测技术[8,9]是具有代表性的成果之一。李永明等[10～13]将模糊集合中可能性测度与模型检测技术相结合，提出了基于可能性测度的模型检测技术。可能性模型检测技术主要用于不完备信息的非确定性系统和非可加性系统的模型检测。在可能性模型检测技术中，广义可能性Kripke结构GPKS(Generalized Possibilistic Kriple Structure)[12]被用来描述系统的模型。GPKS的主要特点是Kripke结构图中状态到其后继状态是一个模糊值。在实际系统开发过程中，我们经常会遇到同时具有非确定性和模糊性的并发系统。为了对此类系统的性质进行分析，我们首先采用类似于马尔科夫决策过程[3]的广义可能性决策过程作为此类系统的模型。广义可能性决策过程中传递既有非确定性选择又有可能性分布，传递首先从当前状态开始非确定选择可能性分布；再选择到其后续状态可能性；然后引入广义可能性计算树逻辑作为此类系统的规范语言；最后给出广义可能性计算树逻辑模型检测的算法和相应的实例对全文内容进行说明。

2 广义可能性决策过程

基于文献[12]中的GPKS，本文提出广义可能性决策过程作为系统模型，该模型类似于马尔科夫决策过程模型。下面给出广义可能性决策过程的定义。

(1) S是一个可数非空的有限状态集合；

(2) Act是动作的集合；

(5) AP是一组原子命题集合；

(6) L:S→2AP是标签函数，即每个状态为真的原子命题的集合(AP的子集)。

Figure 1 Structure model of 4 states group organizations图1 四状态的GPKS

Figure 2 GPKS Mmax图2 GPKS Mmax

Figure 3 GPKS M+图3 GPKS M+

GPo可由Paths(M)扩张到2Paths(M)上，设GPo:2Paths(M)→[0,1]为在Ω=2Paths(M)上的广义可能性测度。对A⊆Paths(M)，有GPo(A)=∨{GPo(π)|π∈A}。

容易验证GPo满足如下性质:

s,si∈S,αi∈Act}

其中,rP(s)表示从M中状态s出发的路径的最大可能性，将用于定理1中的结果。下面通过以Pmax和P+为传递矩阵构造的GPKS，给出rP(s)的计算方法。

证明 对任意s∈S，

s,si∈S,αi∈Act}

由于S是有穷的，则M中存在路径π=s0α0s1α1…siαitβ0t1β1t2…βjt…；s0=s,si,t,tj∈S,αi,βj∈Act,使得:

另一方面，

因此，定理成立。

□

证明Cyl(s0α0s1α1…αn-1sn)=∪{π∈Paths(M)|s0α0s1α1…αn-1sn∈Pref(π)}，则有:

□

GPDP描述的是具有非确定性和模糊性的系统，则访问GPDP时，先确定状态间的可能性分布，然后再确定状态间的可能性，我们把确定状态间可能性分布的方法叫做策略，即调度表。下面给出调度表的定义。

上面由Pmax构造的GPKSMmax=(S,Pmax,I,AP,L)和由P+构造的GPKSM+=(S,P+,I,AP,L)实际上分别对应着GPDPM的一个调度表μ。

Mμ中状态s满足Pr的可能性为:

GPomax(s|=Pr)=maxμ{GPoμ(s|=Pr)}，

GPomin(s|=Pr)=minμ{GPoμ(s|=Pr)}

3 广义可能性计算树逻辑(GPoCTL)

定义4(GPoCTL语法) 原子命题集合AP上GPoCTL状态公式的语法定义如下:

路径公式的语法定义如下:

φ::=O

其中Φ,Φ1,Φ2是状态公式，n∈N。

用∪能够推导出◇和□，即：

◇：“最终”，◇Φ=true∪Φ，表示Φ最终在将来的某个时间为真。

□：“总是”，□Φ=◇Φ，表示从现在一直到永远Φ都为真。

对于GPDPM和GPKSMμ，用SatM(Φ)和SatMμ(Φ)分别表示M和Mμ满足公式Φ的状态集合，≡M和≡Mμ分别表示M和Mμ中两个状态公式等价，即对于状态公式Φ1和Φ2，Φ1≡MΦ2表示SatM(Φ1)=SatM(Φ2)；Φ1≡μΦ2表示SatMμ(Φ1)=SatMμ(Φ2)，我们可以得出如下结论：

4 GPoCTL模型检测

(1)

(2)

(2) 当φ=Φ1∪Φ2时，设C=Sat(Φ1)，B=Sat(Φ2)，对于任意的调度表μ,则有：

GPoμ{π∈Paths(s)|∃j≥0,π[j]∈B,

∀

(3)

(4)

对s∈S?的状态s，有:

(3) 当φ=Φ1∪≤nΦ2，设C=Sat(Φ1)，B=Sat(Φ2)，对于任意的μ,我们有:

GPoμ({π∈Paths(s)|∃j≤n,π[j]∈B,

∀

5 实例分析

从而得(xs max)s∈S=(0.9,1,1,1)，

同理向量(xs min)s∈S的值迭代过程如下：

因此，poor|=GPo[0.7,0.9](◇{excellent})，说明病人通过治疗后恢复的最大可能性为0.9，最小可能性为0.7。

(3) 计算公式GPo(s|={poor,fair}∪≤6{excellent})。

此时S0={good}，Sr={excellent}，S?={poor,fair}，从而得(xs max)s∈S=(0.9,0.9,0,1)，(xs min)s∈S=(0.7,0.7,0,1)。

因此，poor|=GPo[0.7,0.9]({poor,fair}∪≤6{excellent})，说明了病人通过六天的治疗恢复的最大可能性和最小可能性分别为0.9和0.7。

6 结束语

本文引入了GPDP来描述系统的模型，给出了描述系统的性质的规范语言GPoCTL，探讨了系统的GPoCTL模型检测问题，提出了解决GPoCTL模型检测问题的算法，拓展了可能性测度在模型检测中的应用范围。

[1]ClarkeE,GrumbergO,PeledD.ModelChecking[M].Massachusetts:TheMITPress,1999.

[2]LinHM,ZhangWH.Modelchecking:Theories,techniquesandapplications[J].ChineseJournalofElectronics,2002,30(12A): 1907-1912. (inChinese)

[3]BaierC,KatoenJP.Principlesofmodelchecking[M].Massachusetts:TheMITPress, 2007.

[4]CranenS,GrooteJF,ReniersM.AlineartranslationfromCTL*tothefirst-ordermodalμ-calculus[J].TheoreticalComputerScience, 2011,412(28): 3129-3139.

[5]RozierKY.Lineartemporallogicsymbolicmodelchecking[J].ComputerScienceReview, 2011,5(2):163-203.

[6]CleavelandR,PurushothamanS,NarasimhaIM.Probabilistictemporallogicsviathemodalmu-calculus[J].TheoreticalComputerScience, 2005,342(2-3): 316-350.

[7]BentaharJ,YahyaouiH,KovaM,etal.Symbolicmodelcheckingcompositewebservicesusingoperationalandcontrolbehaviors[J]．ExpertSystemswithApplications, 2013,40(2)：508-522．

[8]FischerD,GradelE,KaiserL.Modelcheckinggamesforthequantitativeμ-calculus[J].TheoryofComputingSystems, 2010,47(3): 696-719．

[9]ChechikM,DevereuxB,EasterbrookS,etal.Multi-valuedsymbolicmodel-checking[J].ACMTransactionsonSoftwareEngineeringandMethodology,2003,12(4):1-38．

[10]LiYM,LiLJ.Modelcheckingoflinear-timepropertiesbasedonpossibilitymeasure[J].IEEETransactionsinFuzzySystems, 2013,21(5)：842-854.

[11]LiYM,LiYL,MaZY.Computationtreelogicmodelcheckingbasedonpossibilitymeasure[J].FuzzySetsandSystems, 2015,262(5): 44-59.

[12]LiYM,MaZY.Quantitativecomputationtreelogicmodelcheckingbasedongeneralizedpossibilitymeasures[J].IEEETransactionsonFuzzySystems,2014(09),doi:10.1109/TFUZZ.2015.2396537.

[13]ZhangXX,DengNY,MaZY,etal.Possibilisticbisimulationbasedongeneralizedpossibilitymeasuresanditslogicalcharacterizations[J].ComputerEngineering&Science, 2015,37(5)：951-957. (inChinese)

[14]GarmendiaL,GonzálezR,delCampoV,etal.Analgorithmtocomputethetransitiveclosure,atransitiveapproximationandatransitiveopeningofafuzzyproximity[J].MathwareandSoftComputing, 2009,16(2)：175-191.

[15]XingHY,ZhangQS,HuangKS.Analysisandcontroloffuzzydiscreteeventsystemsusingbisimulationequivalence[J].TheoreticalComputerScience, 2012,456(19)：100-111.

附中文参考文献：

[2] 林惠民,张文辉.模型检测:理论 方法与应用[J].电子学报, 2002,36(12A)：1907-1012.

[13] 张兴兴, 邓楠轶, 马占有, 等. 广义可能性互模拟及其逻辑刻画[J]. 计算机工程与科学, 2015,37(5)：951-957.

马占有(1979-),男，宁夏固原人，博士生，副教授，研究方向为多值模型检测。E-mail:mazhany@126.com

MA Zhan-you,born in 1979,PhD candidate,associate professor,his research interest includes multi-valued model checking.

Computation tree logic model checking for generalized possibilistic decision processes

MA Zhan-you1，2，LI Yong-ming1

(1.College of Computer Science,Shaanxi Normal University,Xi’an 710062;2.College of Computer Science and Engineering,Beifang University of Nationalities,Yinchuan 750021,China)

Model checking is a widespread formal technique for verifying the correctness of concurrent systems. We introduce the generalized possibilistic decision process as the model of the systems, which have non-deterministic choices and generalized possibility distributions.To describe its attributes, we define the concept of generalized possibilistic computation tree logic (GPCTL) specification language and study the GPCTL model checking problems.The time complexity of the computation tree logic model checking algorithm shows to be polynomial time. The results obtained in this paper extend the application scope of model checking based on generalized possibility measurement.

concurrent systems；generalized possibilistic decision process；generalized possibilistic computation tree logic (GPCTL)；model checking

1007-130X(2015)11-2162-07

2015-08-13;

2015-10-11

国家自然科学基金资助项目(11271237,61228305,61462001);北方民族大学资助项目(2014XB213)

TP301

A

10.3969/j.issn.1007-130X.2015.11.025

通信地址：750021 宁夏银川市北方民族大学计算机科学与工程学院

Address:College of Computer Science and Engineering,Beifang University of Nationalities,Yinchuan 750021,Ningxia,P.R.Chin