当前位置:主页 > 社科论文 > 逻辑论文 >

基于广义可能性时序逻辑的定量模型检测

发布时间:2022-02-22 16:17
  经典的模型检测由于其自动化的特点被广泛用于系统的功能正确性和可靠性验证,其强调系统功能的绝对正确,是一种定性的验证方法.随着系统日益复杂,系统中不可避免地会出现一些不确定的信息,这就要求验证过程中不仅要考虑系统的功能需求,还要考虑系统满足该功能的可能性或精确度.为了有效的处理、刻画信息系统存在的不确定性,人们对这些不确定性信息进行定量分析,研究了定量的模型检测.广义可能性模型检测作为定量模型检测主要形式之一,在经典的时序逻辑上引入了可能性测度,不仅可以处理不满足测度可加性的模糊不确定现象,而且使时态性质可度量化,可以更加完整地验证系统的性质.广义可能性模型检测的研究目前处于发展阶段,还有很多工作亟待解决.本文首先利用经典模型的验证方法解决广义可能性模型检测问题,其结果丰富了广义可能性模型检测的研究方法,并有助于弥补其在模型检测工具方面的不足.其次,为了限制时序逻辑中不合理的属性发生,进而研究具有公平性约束的广义可能性时序逻辑.由于广义可能性时序逻辑只是对逻辑联结词和命题的模糊化,不能表示具有模糊时间特点的时序性质,引入能表示模糊时间的模糊时态词,从而研究能表示模糊时间性质的广义可能性时... 

【文章来源】:陕西师范大学陕西省211工程院校教育部直属院校

【文章页数】:126 页

【学位级别】:博士

【文章目录】:
摘要
Abstract
第一章 绪论
    1.1 研究背景与意义
    1.2 模型检测研究现状
    1.3 本文的主要工作
第二章 预备知识
    2.1 时序逻辑
        2.1.1 Kripke结构
        2.1.2 线性时序逻辑
        2.1.3 计算树逻辑
    2.2 广义可能性时序逻辑
        2.2.1 可能性测度理论
        2.2.2 广义可能性Kripke结构
        2.2.3 广义可能性线性时序逻辑
        2.2.4 广义可能计算树逻辑
第三章 广义可能性计算树逻辑的定量模型检测
    3.1 广义可能性计算树逻辑的模型检测
        3.1.1 Po(Φ∪Ψ)和Po(□Φ)的等价形式
        3.1.2 计算‖Po(Φ∪Ψ)‖(s)问题归约
        3.1.3 GPoCTL模型检测问题归约
    3.2 具有公平性约束的GPoCTL模型检测
    3.3 本章小结
第四章 广义可能性线性时序逻辑的定量模型检测
    4.1 广义可能性线性时序逻辑的模型检测
        4.1.1 路径公式的基本性质
        4.1.2 GPoLTL模型检测
        4.1.3 两类模糊线性时序属性的模型检测
    4.2 具有公平性约束的GPoLTL模型检测
    4.3 本章小结
第五章 具有模糊时态的GPoLTL模型检测
    5.1 具有模糊时态的GPoLTL语构和语义
    5.2 几类具有模糊时间的线性时序属性
    5.3 GPoFLTL的必要性阈值模型检测
    5.4 本章小结
第六章 具有模糊时态的GPoCTL模型检测
    6.1 具有模糊时态的GPoCTL语构和语义
    6.2 几类GPoFCTL公式的模型检测问题
    6.3 本章小结
第七章 总结与展望
    7.1 研究内容的总结
    7.2 研究展望
参考文献
致谢
攻读博士学位期间的研究成果


【参考文献】:
期刊论文
[1]模糊线性时序逻辑的可实现性[J]. 范艳焕,李永明.  电子学报. 2018(02)
[2]不确定型模糊Kripke结构的计算树逻辑模型检测[J]. 范艳焕,李永明,潘海玉.  电子学报. 2018(01)
[3]具有模糊时态的广义可能性线性时序逻辑的模型检测[J]. 梁常建,李永明.  电子学报. 2017(12)
[4]广义可能性计算树逻辑的模型检测问题[J]. 梁常建,李永明.  电子学报. 2017(11)
[5]基于决策过程的广义可能性计算树逻辑模型检测[J]. 马占有,李永明.  中国科学:信息科学. 2016(11)
[6]广义可能性计算树逻辑和计算树逻辑的关系[J]. 李丹,李永明.  计算机科学与探索. 2017(10)
[7]广义可能性决策过程的计算树逻辑模型检测[J]. 马占有,李永明.  计算机工程与科学. 2015(11)
[8]随机模型检验研究[J]. 刘阳,李宣东,马艳,王林章.  计算机学报. 2015(11)
[9]广义可能性计算树逻辑的不动点语义[J]. 邓楠轶,张兴兴,李永明.  陕西师范大学学报(自然科学版). 2015(04)
[10]广义可能性互模拟及其逻辑刻画[J]. 张兴兴,邓楠轶,马占有,李永明.  计算机工程与科学. 2015(05)

博士论文
[1]格值交替自动机的若干问题研究[D]. 魏秀娟.陕西师范大学 2018
[2]基于决策过程的广义可能性时态逻辑模型检测[D]. 马占有.陕西师范大学 2017



本文编号:3639806

资料下载
论文发表

本文链接:https://www.wllwen.com/shekelunwen/ljx/3639806.html


Copyright(c)文论论文网All Rights Reserved | 网站地图 |

版权申明:资料由用户341ac***提供,本站仅收录摘要或目录,作者需要删除请E-mail邮箱bigeng88@qq.com