| 中文摘要 | 第1-7页 |
| 英文摘要 | 第7-12页 |
| 1 引言 | 第12-20页 |
| ·时序逻辑 | 第12-13页 |
| ·判定性、复杂性和表达性 | 第13-15页 |
| ·判定性和复杂性 | 第13-14页 |
| ·表达性 | 第14-15页 |
| ·模型检测 | 第15-16页 |
| ·本文的贡献及结构 | 第16-20页 |
| 2 投影时序逻辑 | 第20-30页 |
| ·命题投影时序逻辑 | 第20-23页 |
| ·带星的投影时序逻辑 | 第23-24页 |
| ·投影时序逻辑 | 第24-26页 |
| ·关于投影的讨论 | 第26-30页 |
| 3 PPTL的可判定性 | 第30-70页 |
| ·PPTL的正则形 | 第30-39页 |
| ·正则图 | 第39-47页 |
| ·基于正则图的可满足性 | 第47-55页 |
| ·基于LNFG的判定算法 | 第55-58页 |
| ·无穷区间PITL的可判定性 | 第58-59页 |
| ·PPTL与S1S | 第59-67页 |
| ·区间与(?)-结构 | 第59-61页 |
| ·从PPTL到S1S的转换 | 第61-67页 |
| ·其它转换 | 第67页 |
| ·本章小结 | 第67-70页 |
| 4 PPTL的复杂性 | 第70-76页 |
| ·PPTL的复杂性下界 | 第70-73页 |
| ·讨论 | 第73-74页 |
| ·本章小结 | 第74-76页 |
| 5 PPTL的表达性 | 第76-92页 |
| ·Buchi自动机 | 第76页 |
| ·扩展的正则表达式 | 第76-78页 |
| ·PPTL、ERE和SBA的等价性 | 第78-84页 |
| ·从PPTL到SBA的转换 | 第78-81页 |
| ·从SBA到ERE的转换 | 第81-82页 |
| ·从ERE到PPTL的转换 | 第82-84页 |
| ·PPTL子集的刻画 | 第84-90页 |
| ·L(next,chop)的表达能力 | 第84-86页 |
| ·L(next,chop,chop~*)的表达能力 | 第86-87页 |
| ·L(chop)和L(chop,chop~+)的表达能力 | 第87-89页 |
| ·其它子集的刻画 | 第89-90页 |
| ·PITL的表达能力 | 第90页 |
| ·本章小结 | 第90-92页 |
| 6 基于SPIN的PPTL模型检测 | 第92-100页 |
| ·基本方法 | 第92页 |
| ·复杂性讨论 | 第92-93页 |
| ·基于PPTL的性质规范 | 第93-94页 |
| ·时间区间 | 第93页 |
| ·顺序和迭代 | 第93-94页 |
| ·并发自治 | 第94页 |
| ·青蛙寻路问题的模型检测 | 第94-95页 |
| ·基于PPTL的RMS模型检测 | 第95-98页 |
| ·RMS系统的建模 | 第96-97页 |
| ·RMS系统的性质 | 第97页 |
| ·验证 | 第97-98页 |
| ·本章小结 | 第98-100页 |
| 7 基于PTL的统一模型检测 | 第100-110页 |
| ·建模、仿真和验证语言 | 第100-102页 |
| ·框架技术 | 第100页 |
| ·MSVL语言 | 第100-102页 |
| ·MSVL的正则形和正则图 | 第102-104页 |
| ·基于SAT的PTL统一模型检测 | 第104-109页 |
| ·基本方法 | 第105-107页 |
| ·模型检测器 | 第107页 |
| ·验证实例 | 第107-109页 |
| ·本章小结 | 第109-110页 |
| 8 状态空间化简 | 第110-126页 |
| ·打结不变PLTL公式产生算法 | 第110-115页 |
| ·打结不变PLTL | 第110页 |
| ·PLTL公式的CF范式 | 第110-112页 |
| ·基于CF范式的产生算法 | 第112-115页 |
| ·抽象精化模型检测算法 | 第115-125页 |
| ·抽象函数 | 第116-117页 |
| ·抽象精化 | 第117-123页 |
| ·抽象模型检测的框架 | 第123-125页 |
| ·本章小结 | 第125-126页 |
| 9 交互式投影时序逻辑 | 第126-144页 |
| ·并发博弈结构及其自动机 | 第126-130页 |
| ·并发博弈结构 | 第126-128页 |
| ·并发博弈结构上的自动机 | 第128-130页 |
| ·交互式区间时序逻辑 | 第130-133页 |
| ·交互式区间时序逻辑 | 第130-131页 |
| ·交互式投影时序逻辑 | 第131-133页 |
| ·基于APTL的性质规范 | 第133页 |
| ·APTL到GBCG的转换 | 第133-142页 |
| ·正则形 | 第133-137页 |
| ·从APTL到正则图的转换 | 第137-138页 |
| ·从NFG到GBCG的转换 | 第138-142页 |
| ·APTL的可满足性和模型检测 | 第142页 |
| ·本章小结 | 第142-144页 |
| 10 总结与展望 | 第144-148页 |
| ·全文总结 | 第144-146页 |
| ·未来的研究工作 | 第146-148页 |
| 致谢 | 第148-150页 |
| 参考文献 | 第150-162页 |
| 发表的论文 | 第162-164页 |
| 附录A:命题区间时序逻辑 | 第164-166页 |
| 附录B:命题线性时序逻辑 | 第166-168页 |
| 附录C:单后继单项二阶逻辑 | 第168-169页 |