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

发布时间：2018-06-14 18:52

  本文选题：可能性理论 + 计算树逻辑　； 参考：《电子学报》2017年11期

【摘要】：本文首先分别给出了"约束可达","总是可达"这两个公式在广义可能性计算树逻辑(GPo CTL)中的另外两种等价形式;其次讨论了基于广义可能性测度的计算树逻辑的模型检测问题,将GPo CTL的模型检测问题规约为经典的CTL模型检测问题,利用截集的方法,给出了计算GPo CTL的模型检测问题的算法及其复杂度,并通过实例分析说明了这种算法的可行性;最后,研究了具有公平性假设的GPo CTL模型检测问题的计算复杂度,得到了与上面相似的结论.
[Abstract]:In this paper, we first give two other equivalent forms of "constraint reachability" and "always reachability" in generalized possibility computing tree logic (GPOCTL), and then discuss the model checking problem of computing tree logic based on generalized possibility measure. The model detection problem of GPO CTL is defined as a classical CTL model detection problem. The algorithm and complexity of the model detection problem for calculating the GPO CTL are given by using the method of truncation. The feasibility of the algorithm is illustrated by an example. In this paper, the computational complexity of the GPO CTL model detection problem with fairness hypothesis is studied, and a similar conclusion is obtained.
【作者单位】： 陕西师范大学数学与信息科学学院;商丘师范学院数学与统计学院;
【基金】：国家自然科学基金(No.11271237,No.11671244,No.11401363,No.11501345) 高等学校博士学科点专项科研基金(No.20130202110001)
【分类号】：TP301.6

【相似文献】

相关期刊论文 前10条

1 林惠民,张文辉;模型检测:理论、方法与应用[J];电子学报;2002年S1期

2 戎玫;张广泉;;模型检测新技术研究[J];计算机科学;2003年05期

3 肖健宇;张德运;郑卫斌;;过程提取用于改善程序模型检测的可伸缩性[J];西安交通大学学报;2006年06期

4 袁志斌;徐正权;王能超;;软件模型检测中的抽象[J];计算机科学;2006年07期

5 刘吉锋;孙吉贵;;基于抽象-验证-细化范例的软件模型检测[J];计算机科学;2006年12期

6 化志章;吴传孙;揭安全;薛锦云;;软件模型检测新技术研究[J];微计算机信息;2007年36期

7 王飞明;胡元闯;董荣胜;;模型检测研究进展[J];广西科学院学报;2008年04期

8 邝宏斌;罗贵明;;并行软件模型检测[J];计算机工程;2008年19期

9 何恺铎;顾明;宋晓宇;李力;李江;;面向源代码的软件模型检测及其实现[J];计算机科学;2009年01期

10 顾滨兵;;一种软件模型检测方法及其原型系统[J];微计算机应用;2010年11期

相关会议论文 前5条

1 高静;曹子宁;;基于空间逻辑和计算树逻辑的模型检测[A];2009年中国高校通信类院系学术研讨会论文集[C];2009年

2 许梅;曹子宁;;基于谓词μ演算和空间逻辑的模型检测算法研究[A];2009年中国高校通信类院系学术研讨会论文集[C];2009年

3 何青;骆翔宇;苏开乐;;对弈必胜策略的符号化模型检测[A];2006年全国理论计算机科学学术年会论文集[C];2006年

4 王飞明;胡元闯;董荣胜;;模型检测中状态爆炸及其优化策略研究[A];广西计算机学会2008年年会论文集[C];2008年

5 陈道喜;张广泉;陈冬火;;NSPK协议的Spin模型检测[A];2008年全国开放式分布与并行计算机学术会议论文集(下册)[C];2008年

相关博士学位论文 前8条

1 奚琪;基于模型检测的二进制代码恶意行为识别技术研究[D];解放军信息工程大学;2014年

2 黄镇谨;基于模型检测的时空性能分析若干问题研究[D];合肥工业大学;2016年

3 江华;界程演算模型检测[D];贵州大学;2008年

4 刘剑;传值进程与移动进程的模型检测方法[D];中国科学院研究生院（软件研究所）;2005年

5 赵璐;On-the-Fly和动态的软件模型检测方法研究[D];哈尔滨工程大学;2014年

6 田聪;命题投影时序逻辑的判定性、复杂性、表达性及模型检测[D];西安电子科技大学;2010年

7 黄宏涛;基于懒惰切片的模型检测技术研究[D];哈尔滨工程大学;2012年

8 刘金卓;基于符号化模型检测的软件演化过程模型验证[D];云南大学;2013年

相关硕士学位论文 前10条

1 张兴兴;基于广义可能性测度的互模拟及CTL不动点语义[D];陕西师范大学;2015年

2 王彬;基于多值模型检测的SaaS应用测试及其自动化研究[D];陕西师范大学;2015年

3 王凯;基于模型检测多反例对软件进行调试[D];电子科技大学;2015年

4 张恒;多值模型检测器的研究与实现[D];陕西师范大学;2015年

5 王舒鹏;基于外存的大规模模型检测新方法的研究[D];电子科技大学;2015年

6 刘晓芳;PPTL符号模型检测方法及工具研究[D];西安电子科技大学;2014年

7 王云云;基于分组压缩算法的并行程序模型检测[D];中国科学技术大学;2016年

8 段廷银;基于云计算平台的时态逻辑模型检测算法研究与实现[D];郑州大学;2016年

9 张岩;基于模型检测的Twig模式最小化技术[D];北京工业大学;2016年

10 张松年;基于模型检测的漏洞挖掘方法研究[D];西安电子科技大学;2015年

，

本文编号：2018607