PPTL模型检测器的改进及应用

摘要	第1-4页
Abstract	第4-7页
第一章 绪论	第7-13页
·研究背景	第7-9页
·模型检测	第7-8页
·时序逻辑	第8-9页
·研究现状	第9-10页
·模型检测	第9-10页
·时序逻辑	第10页
·研究意义及目的	第10-11页
·研究内容及章节安排	第11-13页
第二章 命题投影时序逻辑	第13-19页
·PPTL的语法	第13-14页
·PPTL的语义	第14-15页
·联结词的扩充	第15-16页
·可满足性和有效性	第16-17页
·操作符的优先级	第17页
·逻辑法则	第17-19页
第三章 模型检测技术	第19-25页
·模型检测的原理	第19-20页
·模型检测技术的发展	第20-21页
·模型检测器SPIN	第21-25页
第四章 PPTL模型检测技术的改进	第25-43页
·基于SPIN的PPTL模型检测器	第25-28页
·PPTL到Never Claim的改进转换算法	第28-37页
·PPTL公式的范式	第28-33页
·PPTL公式的加标记的范式图	第33-36页
·PPTL公式的Never Claim	第36-37页
·改进的PPTL模型检测器的实现及使用方法	第37-43页
第五章 PPTL模型检测器的应用实例	第43-69页
·German协议验证	第43-53页
·German协议介绍	第43-45页
·German协议模型	第45-50页
·German协议验证	第50-53页
·Russian Cards扩展问题	第53-69页
·Russian Cards五人问题	第53-55页
·Russian Cards五人问题的系统模型	第55-67页
·Russian Cards五人问题的验证	第67-69页
第六章 结论	第69-71页
·总结	第69-70页
·展望	第70-71页
致谢	第71-73页
参考文献	第73-79页
作者在读期间的研究成果	第79-81页
附录A	第81-85页
附录B	第85-87页