具有模糊时态的广义可能性线性时序逻辑的模型检测

发布时间：2018-10-24 08:47

【摘要】：本文首先定义了具有模糊时态的广义可能性线性时序逻辑GPoFLTL(Generalized Possibilistic Fuzzy Linear Tempora Logic)的语构以及基于路径和基于语言的两种语义解释,证明了GPoFLTL在模糊时态方面对GPo LTL(Generalized Possibilistic Linear Tempora Logic)进行了扩张,并通过实例说明了GPoFLTL比GPo LTL具有更强的表达能力;其次在广义可能性测度下通过模糊矩阵运算讨论了"不久","几乎总是"等几类模糊时态性质的模型检测问题;最后研究了模糊时态性质的必要性阈值模型检测问题,给出了基于自动机的GPoFLTL的阈值模型检测算法及算法的复杂度.
[Abstract]:In this paper, we first define the construction of generalized possibilistic linear temporal logic (GPoFLTL (Generalized Possibilistic Fuzzy Linear Tempora Logic) with fuzzy tenses and two semantic interpretations based on path and language. It is proved that GPoFLTL extends GPo LTL (Generalized Possibilistic Linear Tempora Logic) in fuzzy tenses. The examples show that GPoFLTL has stronger expressive ability than GPo LTL, and then some fuzzy temporal properties such as "soon" and "almost always" are discussed by fuzzy matrix operation under generalized possibility measure. Finally, the necessity threshold model detection problem of fuzzy temporal properties is studied, and the algorithm of threshold model detection based on automata for GPoFLTL and the complexity of the algorithm are given.
【作者单位】： 陕西师范大学数学与信息科学学院;商丘师范学院数学与统计学院;
【基金】：国家自然科学基金(No.11271237,No.11671244,No.11401363,No.11501345) 高等学校博士学科点专项科研基金项目(No.20130202110001)
【分类号】：TP301

【相似文献】

相关期刊论文 前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年

相关博士学位论文 前10条

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

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

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

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

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

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

7 逄涛;命题投影时序逻辑符号模型检测及其应用研究[D];西安电子科技大学;2014年

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

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

10 刘万伟;扩展时序逻辑的推理及符号化模型检验技术[D];国防科学技术大学;2009年

相关硕士学位论文 前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年

，

本文编号：2290898