| 广义可能性计算树逻辑的模型检测问题 |
| |
| 引用本文： | 梁常建,李永明. 广义可能性计算树逻辑的模型检测问题[J]. 电子学报, 2017, 45(11): 2641-2648. DOI: 10.3969/j.issn.0372-2112.2017.11.010 |
| |
| 作者姓名： | 梁常建 李永明 |
| |
| 作者单位： | 1. 陕西师范大学数学与信息科学学院, 陕西西安 710119;2. 商丘师范学院数学与统计学院, 河南商丘 476000 |
| |
| 基金项目： | 国家自然科学基金,高等学校博士学科点专项科研基金 |
| |
| 摘 要： | 本文首先分别给出了"约束可达","总是可达"这两个公式在广义可能性计算树逻辑（GPoCTL）中的另外两种等价形式;其次讨论了基于广义可能性测度的计算树逻辑的模型检测问题,将GPoCTL的模型检测问题规约为经典的CTL模型检测问题,利用截集的方法,给出了计算GPoCTL的模型检测问题的算法及其复杂度,并通过实例分析说明了这种算法的可行性;最后,研究了具有公平性假设的GPoCTL模型检测问题的计算复杂度,得到了与上面相似的结论.
|
| 关 键 词： | 可能性理论 计算树逻辑 模型检测 时间复杂性 规约 |
| 收稿时间： | 2016-04-11 |
The Model Checking Problem of Computing Tree Logic Based on Generalized Possibility Measures |
| |
| LIANG Chang-jian,LI Yong-ming. The Model Checking Problem of Computing Tree Logic Based on Generalized Possibility Measures[J]. Acta Electronica Sinica, 2017, 45(11): 2641-2648. DOI: 10.3969/j.issn.0372-2112.2017.11.010 |
| |
| Authors: | LIANG Chang-jian LI Yong-ming |
| |
| Affiliation: | 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 |
| |
| 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. |
| |
| Keywords: | possibility theory computation tree logic model checking time complexity reduction |
| 本文献已被 万方数据 等数据库收录！ |
| 点击此处可从《电子学报》浏览原始摘要信息 |
|
点击此处可从《电子学报》下载免费的PDF全文 |
|
