| 摘要 | 第1-4页 |
| ABSTRACT | 第4-7页 |
| 引言 | 第7-11页 |
| 1、研究背景与研究现状 | 第7-9页 |
| 2、研究内容和研究意义 | 第9页 |
| 3、本文结构 | 第9-11页 |
| 第一章 时间自动机 | 第11-24页 |
| 1．1 时间语言 | 第11-12页 |
| 1．2 时间约束和时钟解释 | 第12页 |
| 1．3 时间自动机的语法和语义 | 第12-14页 |
| 1．4 时间正则语言 | 第14-15页 |
| 1．5 确定型时间自动机 | 第15-16页 |
| 1．6 区域自动机 | 第16-19页 |
| 1．6．1 时钟区域 | 第16-17页 |
| 1．6．2 区域自动机 | 第17-19页 |
| 1．7 带自动机 | 第19-21页 |
| 1．8 时间正则表达式 | 第21-22页 |
| 1．8．1 语法 | 第21页 |
| 1．8．2 语义 | 第21-22页 |
| 1．8．3 时间自动机的Kleene定理 | 第22页 |
| 1．9 时间自动机识别语言的一个条件定理 | 第22-24页 |
| 第二章 时间树自动机 | 第24-38页 |
| 2．1 运行在无穷树上的自动机 | 第24-26页 |
| 2．2 时间树自动机 | 第26-28页 |
| 2．3 时间树自动机的区域构造 | 第28-29页 |
| 2．4 时间树语言类的关系 | 第29-30页 |
| 2．5 封闭性和判定问题 | 第30-31页 |
| 2．6 应用 | 第31-35页 |
| 2．7 时间树自动机识别语言的一个条件定理 | 第35-38页 |
| 第三章 信号自动机 | 第38-46页 |
| 3．1 信号 | 第38-40页 |
| 3．2 信号自动机与信号正则表达式 | 第40-41页 |
| 3．3 时间自动机与信号自动机行为的等价性 | 第41-43页 |
| 3．4 离散步长双向模拟算法 | 第43-46页 |
| 3．4．1 从SA到TA | 第43-44页 |
| 3．4．2 从TA到SA | 第44页 |
| 3．4．3 对算法的说明 | 第44-46页 |
| 第四章 基于时间自动机的实时系统验证 | 第46-54页 |
| 4．1 使用时间自动机验证 | 第46-47页 |
| 4．2 一个实例:使用验证工具KRONOS验证CSMA/CD协议 | 第47-54页 |
| 4．2．1 KRONOS工具介绍 | 第47-48页 |
| 4．2．2 为CSMA/CD协议建模 | 第48-50页 |
| 4．2．3 使用TCTL逻辑验证 | 第50-51页 |
| 4．2．4 基于KRONOS的验证 | 第51-52页 |
| 4．2．5 验证CSMA/CD协议 | 第52-54页 |
| 第五章 应用研究:基于时间自动机的基因网络逻辑模型 | 第54-58页 |
| 5．1 基于有限状态自动机的基因网络模型 | 第54-55页 |
| 5．2 基于时间自动机的基因网络模型 | 第55-58页 |
| 第六章 结束语 | 第58-59页 |
| 致谢 | 第59-60页 |
| 参考文献 | 第60-67页 |
| 附录1 攻读硕士学位期间发表的论文 | 第67页 |