广义可能性计算树逻辑的模型检测问题  

The Model Checking Problem of Computing Tree Logic Based on Generalized Possibility Measures

作　　者：梁常建[1,2] 李永明 

机构地区：[1]陕西师范大学数学与信息科学学院,陕西西安710119 [2]商丘师范学院数学与统计学院,河南商丘476000

出　　处：《电子学报》2017年第11期2641-2648,共8页Acta Electronica Sinica

基　　金：国家自然科学基金(No.11271237;No.11671244;No.11401363;No.11501345);高等学校博士学科点专项科研基金(No.20130202110001)

摘　　要：本文首先分别给出了"约束可达","总是可达"这两个公式在广义可能性计算树逻辑(GPo CTL)中的另外两种等价形式;其次讨论了基于广义可能性测度的计算树逻辑的模型检测问题,将GPo CTL的模型检测问题规约为经典的CTL模型检测问题,利用截集的方法,给出了计算GPo CTL的模型检测问题的算法及其复杂度,并通过实例分析说明了这种算法的可行性;最后,研究了具有公平性假设的GPo CTL模型检测问题的计算复杂度,得到了与上面相似的结论.Firstly,two alternative equivalent forms of GPoCTL state formulas,"until","always",are given respectively.Secondly,it shows that the model checking problem of GPoCTL can be reduced to which of CTL,its algorithm is given through the method of cut set,and whose availability is explained with an example analysis,as a result,the time complexity of the algorithm is obtained.Finally,the properties of the GPoCTL model checking problem with fairness assumptions,which are similar to the GPoCTL,are studied by the similar method with GPoCTL.

关 键 词：可能性理论 计算树逻辑 模型检测 时间复杂性 规约 

分 类 号：TP301.2[自动化与计算机技术—计算机系统结构]