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

摘要	第1-5页
Abstract	第5-8页
第一章 绪论	第8-16页
·形式化验证	第8-9页
·模型检测	第9-11页
·模型检测简介	第9-10页
·模型验证方法	第10页
·模型检测的发展	第10-11页
·时序逻辑	第11-12页
·区间时序逻辑的研究现状	第12-13页
·论文组织结构	第13-16页
第二章 命题投影时序逻辑	第16-26页
·命题投影时序逻辑	第16-20页
·PPTL 的语法	第16-17页
·PPTL 的语义	第17-18页
·可满足性与有效性	第18-19页
·优先级	第19页
·逻辑规则	第19-20页
·PPTL 与PITL 的比较	第20-26页
·chop 操作符的区别	第20-21页
·时序操作符prj 与proj	第21-22页
·投影应用实例	第22-26页
第三章 PPTL 公式的可判定性	第26-44页
·PPTL 公式的正则形	第26-27页
·PPTL 公式的正则图	第27-38页
·NFG 的定义	第27-28页
·NFG 的分类	第28-29页
·NFG 的构造算法	第29-31页
·NFG 的有穷性证明	第31-38页
·PPTL 公式可满足性的判定过程	第38-44页
·路径与模型	第38-40页
·PPTL 公式可满足性的判定过程	第40-41页
·应用实例	第41-44页
第四章 PITL 可满足性的判定过程	第44-48页
·命题区间时序逻辑(PITL)	第44页
·PITL 公式可满足性的判定过程	第44-48页
第五章 模型检测	第48-52页
·模型检测工具的研究现状	第48-49页
·基于PPTL 的模型检测工具	第49-52页
总结与展望	第52-54页
致谢	第54-56页
参考文献	第56-62页
研究成果	第62页