命题投影时序逻辑的可判定性

发布时间：2022-01-25 16:04

　　本文主要研究命题投影时序逻辑（Propositional Projection Temporal Logic, PPTL）的可判定性问题。文中简要地介绍了PPTL公式的语法、语义及逻辑规则,定义了PPTL公式的正则形（Normal Form）和完备正则形（Complete Normal Form）。在正则形的基础上,给出PPTL公式正则图（Normal Form Graph）的归纳定义和可执行的算法,证明了该算法的可终止性。基于正则图,PPTL公式在无穷区间范围的可判定性问题得到解决。另外,本文也给出了命题区间时序逻辑（Propositional Interval Temporal Logic, PITL）在无穷区间范围的判定过程。逻辑的可判定性是基于该逻辑的模型检测方法的基础,本文给出的判定算法证实了基于PPTL的模型检测方法的可行性。文章最后回顾了模型检测工具的发展现状,分析了以PPTL为逻辑基础的模型检测工具的优越性,阐明了开发基于PPTL的模型检测器的必要性,且给出了基于PPTL的模型检测器的概要设计。 

【文章来源】：西安电子科技大学陕西省 211工程院校 教育部直属院校

【文章页数】：62 页

【学位级别】：硕士

【文章目录】：
摘要
Abstract
第一章 绪论
    1.1 形式化验证
    1.2 模型检测
        1.2.1 模型检测简介
        1.2.2 模型验证方法
        1.2.3 模型检测的发展
    1.3 时序逻辑
    1.4 区间时序逻辑的研究现状
    1.5 论文组织结构
第二章 命题投影时序逻辑
    2.1 命题投影时序逻辑
        2.1.1 PPTL 的语法
        2.1.2 PPTL 的语义
        2.1.3 可满足性与有效性
        2.1.4 优先级
        2.1.5 逻辑规则
    2.2 PPTL 与PITL 的比较
        2.2.1 chop 操作符的区别
        2.2.2 时序操作符prj 与proj
        2.2.3 投影应用实例
第三章 PPTL 公式的可判定性
    3.1 PPTL 公式的正则形
    3.2 PPTL 公式的正则图
        3.2.1 NFG 的定义
        3.2.2 NFG 的分类
        3.2.3 NFG 的构造算法
        3.2.4 NFG 的有穷性证明
    3.3 PPTL 公式可满足性的判定过程
        3.3.1 路径与模型
        3.3.2 PPTL 公式可满足性的判定过程
        3.3.3 应用实例
第四章 PITL 可满足性的判定过程
    4.1 命题区间时序逻辑(PITL)
    4.2 PITL 公式可满足性的判定过程
第五章 模型检测
    5.1 模型检测工具的研究现状
    5.2 基于PPTL 的模型检测工具
总结与展望
致谢
参考文献
研究成果


【参考文献】：
期刊论文
[1]基于PVS的UML类图和序列图的一致性检验[J]. 刘晓健,陈平.  系统工程与电子技术. 2004(10)
[2]基于PVS的飞机订票系统的形式化描述与验证[J]. 杨红丽,刘建元,韩俊刚.  西安邮电学院学报. 2001(03)

博士论文
[1]LTLC：面向实时与混成系统的连续时序逻辑[D]. 李广元.中国科学院软件研究所 2001



本文编号：3608832