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

梁常建; 李永明

doi:10.3969/j.issn.0372-2112.2017.11.010

您当前的位置：

首页 >

文章列表页 >

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

学术论文 | 更新时间：2025-07-16

- 广义可能性计算树逻辑的模型检测问题
- The Model Checking Problem of Computing Tree Logic Based on Generalized Possibility Measures
- 电子学报 2017年45卷第11期页码：2641-2648
- 作者机构：
  
  1. 陕西师范大学数学与信息科学学院,陕西,西安,710119
  2. 商丘师范学院数学与统计学院,河南,商丘,476000
  3. 陕西师范大学数学与信息科学学院,陕西,西安,710119
  4. 商丘师范学院数学与统计学院,河南,商丘,476000
- 作者简介：
- 基金信息：
  
  国家自然科学基金 (No.11271237，No.11671244，No.11401363，No.11501345）;高等学校博士学科点专项科研基金 (No.20130202110001）
- DOI：10.3969/j.issn.0372-2112.2017.11.010
  中图分类号： TP301.2
- 网络出版：2017-11-25，
  
  纸质出版：2017
- 稿件说明：
移动端阅览
梁常建, 李永明. 广义可能性计算树逻辑的模型检测问题[J]. 电子学报, 2017,45(11):2641-2648.

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.
梁常建, 李永明. 广义可能性计算树逻辑的模型检测问题[J]. 电子学报, 2017,45(11):2641-2648. DOI： 10.3969/j.issn.0372-2112.2017.11.010.

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.

摘要

本文首先分别给出了约束可达，总是可达这两个公式在广义可能性计算树逻辑（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.

关键词

Keywords

references

浏览量

240

下载量

CSCD

文章被引用时，请邮件提醒。

提交

工具集

关联资源

不确定型模糊Kripke结构的计算树逻辑模型检测

时间感知Web服务交互行为建模与失配检测方法研究

实时模型检测中基于驻留环的精确加速

基于XYZ/ADL的Web服务组合描述与验证

缓冲区溢出漏洞精确检测方法研究