基于决策过程的广义可能性时态逻辑模型检测
发布时间：2022-07-04 22:20
随着计算机软硬件系统日益复杂,如何保证其正确性和可靠性,已成为大家广泛探讨的问题.模型检测由于其借助严格的数学方法来验证系统是否满足性质和自动化验证等特点,深受学术界和工业界的关注.经典的模型检测是一种定性的验证方法,其强调的是系统满足功能需求性质的绝对正确.然而很多实际的系统被赋予量化行为特征,需要定量分析其满足用户的功能和非功能需求性质的程度.近年来,学者们开始研究定量的模型检测.定量的模型检测不仅能体现系统多大程度满足其功能需求性质,还能体现系统的性能指标等非功能需求,极大地拓展了模型检测的应用范围.定量的模型检测包括概率模型检测和模糊模型检测,其中概率模型检测用于验证概率系统,对具有不确定信息和不相容信息的非概率系统,学者们提出了模糊模型检测.广义可能性模型检测是模糊模型检测的主要形式之一,由于其考虑了测度信息,它能更完善地验证模糊系统的性质.本文主要针对模糊系统,引入广义可能性决策过程（generalized possibilistic decision process,GPDP）模型来描述此类模糊系统的行为.利用可能性测度理论和决策过程的相关理论,将经典的计算树逻辑（Com...
【文章页数】：117 页
【学位级别】：博士
【文章目录】：
摘要
Abstract
第一章 绪论
1.1 研究背景与意义
1.2 模型检测技术研究现状
1.3 本文的主要工作
第二章 预备知识
2.1 Kripke结构
2.2 时态逻辑
2.2.1 线性时序逻辑(LTL)
2.2.2 计算树逻辑(CTL)
2.2.3 分支时态逻辑(CTL~*)
2.3 模糊集和模糊矩阵的基本概念
2.4 可能性测度理论
2.5 广义可能性Kripke结构及其广义可能性测度
2.6 Knaster-Tarski不动点定理
第三章 基于决策过程的广义可能性CTL模型检测
3.1 广义可能性决策过程
3.2 广义可能性计算树逻辑
3.3 广义可能性计算树模型检测
3.4 实例应用
3.5 本章小结
第四章 基于决策过程的广义可能性线性时间属性模型检测
4.1 广义可能性线性时间属性
4.2 广义可能性线性时间属性的可达可能性
4.2.1 最终可达事件的可能性
4.2.2 总是可达事件的可能性
4.2.3 限制可达事件的可能性
4.2.4 重复可达事件的可能性
4.2.5 持久可达事件的可能性
4.3 广义可能性线性时间属性的可能性测度
4.3.1 广义可能性正则安全属性的可能性测度
4.3.2 广义可能性ω-正则属性的可能性测度
4.4 本章小结
第五章 基于决策过程的GPoCTL~*模型检测和可能性互模拟
5.1 GPoCTL~*语法和语义
5.2 GPoLTL模型检测算法
5.2.1 GPoLTL PNF语法和语义
5.2.2 GPoLTL模型检测算法
5.3 GPoCTL~*模型检测算法
5.4 最大可能性互模拟及其逻辑刻画
5.4.1 最大可能性互模拟
5.4.2 GPoCTL/GPoCTL~*与最大可能性互模拟的等价性
5.5 本章小结
第六章 总结与展望
6.1 研究内容的总结
6.2 研究展望
参考文献
致谢
攻读博士学位期间的研究成果
【参考文献】：
期刊论文
[1]基于决策过程的广义可能性计算树逻辑模型检测[J]. 马占有,李永明. 中国科学:信息科学. 2016(11)
[2]广义可能性决策过程的计算树逻辑模型检测[J]. 马占有,李永明. 计算机工程与科学. 2015(11)
[3]随机模型检验研究[J]. 刘阳,李宣东,马艳,王林章. 计算机学报. 2015(11)
[4]一个命题投影时序逻辑符号模型检测器[J]. 逄涛,段振华,刘晓芳. 软件学报. 2015(08)
[5]广义可能性计算树逻辑的不动点语义[J]. 邓楠轶,张兴兴,李永明. 陕西师范大学学报(自然科学版). 2015(04)
[6]广义可能性互模拟及其逻辑刻画[J]. 张兴兴,邓楠轶,马占有,李永明. 计算机工程与科学. 2015(05)
[7]基于广义可能性测度的可达性问题的模型检测[J]. 马占有,李永明. 模糊系统与数学. 2014(06)
[8]可能LTL模型检测的两种方法[J]. 李永明. 陕西师范大学学报(自然科学版). 2014(06)
[9]基于可能性测度的工程管理决策的研究[J]. 李召妮,马占有,李永明. 计算机科学. 2014(08)
[10]马尔可夫决策过程的限界模型检测[J]. 周从华,邢支虎,刘志锋,王昌达. 计算机学报. 2013(12)
博士论文
[1]命题投影时序逻辑的完备公理系统与形式验证[D]. 张南.西安电子科技大学 2012
[2]状态转换系统的格值量化验证方法研究[D]. 潘海玉.华东师范大学 2012
[3]多智能体系统的符号模型检测[D]. 骆翔宇.中山大学 2006
本文编号：3656031
【文章页数】：117 页
【学位级别】：博士
【文章目录】：
摘要
Abstract
第一章 绪论
1.1 研究背景与意义
1.2 模型检测技术研究现状
1.3 本文的主要工作
第二章 预备知识
2.1 Kripke结构
2.2 时态逻辑
2.2.1 线性时序逻辑(LTL)
2.2.2 计算树逻辑(CTL)
2.2.3 分支时态逻辑(CTL~*)
2.3 模糊集和模糊矩阵的基本概念
2.4 可能性测度理论
2.5 广义可能性Kripke结构及其广义可能性测度
2.6 Knaster-Tarski不动点定理
第三章 基于决策过程的广义可能性CTL模型检测
3.1 广义可能性决策过程
3.2 广义可能性计算树逻辑
3.3 广义可能性计算树模型检测
3.4 实例应用
3.5 本章小结
第四章 基于决策过程的广义可能性线性时间属性模型检测
4.1 广义可能性线性时间属性
4.2 广义可能性线性时间属性的可达可能性
4.2.1 最终可达事件的可能性
4.2.2 总是可达事件的可能性
4.2.3 限制可达事件的可能性
4.2.4 重复可达事件的可能性
4.2.5 持久可达事件的可能性
4.3 广义可能性线性时间属性的可能性测度
4.3.1 广义可能性正则安全属性的可能性测度
4.3.2 广义可能性ω-正则属性的可能性测度
4.4 本章小结
第五章 基于决策过程的GPoCTL~*模型检测和可能性互模拟
5.1 GPoCTL~*语法和语义
5.2 GPoLTL模型检测算法
5.2.1 GPoLTL PNF语法和语义
5.2.2 GPoLTL模型检测算法
5.3 GPoCTL~*模型检测算法
5.4 最大可能性互模拟及其逻辑刻画
5.4.1 最大可能性互模拟
5.4.2 GPoCTL/GPoCTL~*与最大可能性互模拟的等价性
5.5 本章小结
第六章 总结与展望
6.1 研究内容的总结
6.2 研究展望
参考文献
致谢
攻读博士学位期间的研究成果
【参考文献】：
期刊论文
[1]基于决策过程的广义可能性计算树逻辑模型检测[J]. 马占有,李永明. 中国科学:信息科学. 2016(11)
[2]广义可能性决策过程的计算树逻辑模型检测[J]. 马占有,李永明. 计算机工程与科学. 2015(11)
[3]随机模型检验研究[J]. 刘阳,李宣东,马艳,王林章. 计算机学报. 2015(11)
[4]一个命题投影时序逻辑符号模型检测器[J]. 逄涛,段振华,刘晓芳. 软件学报. 2015(08)
[5]广义可能性计算树逻辑的不动点语义[J]. 邓楠轶,张兴兴,李永明. 陕西师范大学学报(自然科学版). 2015(04)
[6]广义可能性互模拟及其逻辑刻画[J]. 张兴兴,邓楠轶,马占有,李永明. 计算机工程与科学. 2015(05)
[7]基于广义可能性测度的可达性问题的模型检测[J]. 马占有,李永明. 模糊系统与数学. 2014(06)
[8]可能LTL模型检测的两种方法[J]. 李永明. 陕西师范大学学报(自然科学版). 2014(06)
[9]基于可能性测度的工程管理决策的研究[J]. 李召妮,马占有,李永明. 计算机科学. 2014(08)
[10]马尔可夫决策过程的限界模型检测[J]. 周从华,邢支虎,刘志锋,王昌达. 计算机学报. 2013(12)
博士论文
[1]命题投影时序逻辑的完备公理系统与形式验证[D]. 张南.西安电子科技大学 2012
[2]状态转换系统的格值量化验证方法研究[D]. 潘海玉.华东师范大学 2012
[3]多智能体系统的符号模型检测[D]. 骆翔宇.中山大学 2006
本文编号：3656031
本文链接：https://www.wllwen.com/guanlilunwen/lindaojc/3656031.html
