电子学报 ›› 2017, Vol. 45 ›› Issue (11): 2641-2648.DOI: 10.3969/j.issn.0372-2112.2017.11.010

• 学术论文 • 上一篇    下一篇

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

梁常建1,2, 李永明1   

  1. 1. 陕西师范大学数学与信息科学学院, 陕西西安 710119;
    2. 商丘师范学院数学与统计学院, 河南商丘 476000
  • 收稿日期:2016-04-11 修回日期:2017-04-25 出版日期:2017-11-25 发布日期:2017-11-25
  • 作者简介:梁常建,男,1981年出生于河南鹿邑,博士研究生,讲师,主要研究领域为定量模型检测.E-mail:liangcj37@snnu.edu.cn;李永明,男,1966年出生于陕西大荔,博士,教授,博士生导师,研究方向为计算智能、量子逻辑、量子计算、模型检测.E-mail:liyongm@snnu.edu.cn
  • 基金资助:
    国家自然科学基金(No.11271237,No.11671244,No.11401363,No.11501345);高等学校博士学科点专项科研基金(No.20130202110001)

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

LIANG Chang-jian1,2, LI Yong-ming1   

  1. 1. School of Mathematics and Information Science, Shaanxi Normal University, Xi'an, Shaanxi 710119, China;
    2. School of Mathematics and Statistics, Shangqiu Normal University, Shangqiu, Henan, 476000, China
  • Received:2016-04-11 Revised:2017-04-25 Online:2017-11-25 Published:2017-11-25

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

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

Abstract: 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.

Key words: possibility theory, computation tree logic, model checking, time complexity, reduction

中图分类号: