| 摘要 | 第1-4页 |
| Abstract | 第4-8页 |
| 第一章 引言 | 第8-16页 |
| 1．1 有穷状态自动机的提出 | 第8-11页 |
| 1．2 时间自动机 | 第11-14页 |
| 1．3 模型验证 | 第14-15页 |
| 1．4 论文内容及结构 | 第15-16页 |
| 第二章 公式时钟自动机 | 第16-22页 |
| 2．1 线性命题时态逻辑公式的语法 | 第16页 |
| 2．2 线性命题时态逻辑公式的语义 | 第16-17页 |
| 2．3 公式记录时钟与公式预测时钟 | 第17-19页 |
| 2．4 公式时钟自动机的语法和语义 | 第19-22页 |
| 第三章 确定性与非确定性公式时钟自动机的等价性 | 第22-26页 |
| 3．1 确定的公式时钟自动机 | 第22页 |
| 3．2 确定性与非确定性公式时钟自动机的等价性 | 第22-26页 |
| 第四章 公式时钟自动机的性质 | 第26-33页 |
| 4．1 用标记变换系统描述公式时钟自动机的语义 | 第26-27页 |
| 4．2 公式时钟自动机的域构造 | 第27-29页 |
| 4．3 公式时钟自动机在布尔运算下的封闭性 | 第29-30页 |
| 4．4 公式时钟Büchi自动机与公式时钟Muller自动机 | 第30-31页 |
| 4．5 公式时钟自动机与事件时钟自动机之间的关系 | 第31-33页 |
| 第五章 用公式时钟自动机进行验证 | 第33-42页 |
| 5．1 轨迹语义 | 第33-34页 |
| 5．2 给轨迹加上时间 | 第34-36页 |
| 5．3 ω自动机与验证 | 第36-37页 |
| 5．4 用公式时钟自动机进行验证 | 第37页 |
| 5．5 验证举例 | 第37-42页 |
| 第六章 总结与展望 | 第42-44页 |
| 6．1 总结 | 第42页 |
| 6．2 展望 | 第42-44页 |
| 致谢 | 第44-49页 |
| 发表论文 | 第49页 |