符号化模型检测算法的研究

提要	第1-7页
第1章 前言	第7-9页
·研究背景	第7-8页
·本文的主要内容	第8-9页
第2章 模型检测概述	第9-19页
·模型检测的特点	第9-10页
·模型检测的过程	第10-11页
·Kripke结构	第11页
·时态逻辑	第11-17页
·计算树逻辑CTL~*	第12-14页
·线性时态逻辑LTL	第14-15页
·分支时态逻辑CTL	第15-17页
·三种时态逻辑之间的关系	第17页
·公平性约束	第17-19页
第3章 显式模型检测算法	第19-29页
·Labelling算法	第19-22页
·公平性约束的处理	第22-23页
·Tableau算法	第23-27页
·本章小结	第27-29页
第4章 符号化模型检测算法	第29-44页
·量化布尔公式	第29-30页
·有序二元决策图	第30-33页
·不动点理论基础	第33-34页
·符号化模型检测CTL~*算法的框架	第34-43页
·Kripke结构的符号化过程	第35-36页
·时态算子的不动点刻画	第36-38页
·CTL*的符号化模型检测算法	第38-43页
·本章小结	第43-44页
第5章 系统实现	第44-52页
·NuSMV简介	第44-45页
·具体实现	第45-51页
·本章小结	第51-52页
第6章 总结与展望	第52-53页
·总结	第52页
·展望	第52-53页
参考文献	第53-57页
在读期间发表的学术论文	第57-58页
致谢	第58-59页
摘要	第59-61页
Abstract	第61-63页