文献类型：期刊文章

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

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

出　　处：《电子学报》

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

年　　份：2017

卷　　号：45

期　　号：11

起止页码：2641-2648

语　　种：中文

收录情况：BDHX、BDHX2014、CAS、CSCD、CSCD2017_2018、EI、IC、JST、RCCSE、SCOPUS、ZGKJHX、核心刊

摘　　要：本文首先分别给出了"约束可达","总是可达"这两个公式在广义可能性计算树逻辑(GPo CTL)中的另外两种等价形式;其次讨论了基于广义可能性测度的计算树逻辑的模型检测问题,将GPo CTL的模型检测问题规约为经典的CTL模型检测问题,利用截集的方法,给出了计算GPo CTL的模型检测问题的算法及其复杂度,并通过实例分析说明了这种算法的可行性;最后,研究了具有公平性假设的GPo CTL模型检测问题的计算复杂度,得到了与上面相似的结论.

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

分 类 号：TP301.2]