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

论文摘要

本文主要研究命题投影时序逻辑(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的模型检测器的概要设计。

论文目录

• 摘要
• 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 的模型检测工具
• 总结与展望
• 致谢
• 参考文献
• 研究成果