关于时间自动机及其构造区域自动机的算法
| 引言 | 第1-7页 |
| 第一章 时间自动机的定义 | 第7-16页 |
| 1．1 ω-自动机 | 第7-8页 |
| 1．2 时间转换表 | 第8-13页 |
| 1．2．1 具有时间约束的转换表。 | 第10-11页 |
| 1．2．2 时钟约束与时钟解释 | 第11-12页 |
| 1．2．3 时间自动机 | 第12-13页 |
| 1．3 时间BUCHI自动机 | 第13-14页 |
| 1．4 时间MULLER自动机 | 第14-16页 |
| 第二章 区域自动机及新的构造算法 | 第16-33页 |
| 2．1 时钟区域 | 第16-18页 |
| 2．2 时间后继 | 第18-19页 |
| 2．3 等价类区域自动机 | 第19-22页 |
| 2．4 非时间构造 | 第22-23页 |
| 2．5 等价类区域自动机算法的初步实现 | 第23-24页 |
| 2．6 等价类区域自动机算法的改进 | 第24-26页 |
| 2．7 一种新的区域自动机构造方法 | 第26-31页 |
| 2．7．1 位移值与位移空间 | 第26-27页 |
| 2．7．2 相容、相容值与相容空间 | 第27-29页 |
| 2．7．3 新的区域自动机构造方法 | 第29页 |
| 2．7．4 新的区域自动机构造算法的实现 | 第29-31页 |
| 2．8 算法分析 | 第31-33页 |
| 第三章 其它类型的时间自动机 | 第33-37页 |
| 3．1 确定时间自动机 | 第33-34页 |
| 3．2 事件记录自动机 | 第34-35页 |
| 3．3 事件预测自动机 | 第35-36页 |
| 3．4 事件时钟自动机 | 第36-37页 |
| 第四章 时间语言类的性质 | 第37-47页 |
| 4．1 判空的复杂性 | 第37-38页 |
| 4．2 包含和等价 | 第38页 |
| 4．3 时间正则语言的性质 | 第38-40页 |
| 4．4 补操作的非封闭性 | 第40页 |
| 4．5 时钟约束的选择 | 第40-41页 |
| 4．6 封闭属性 | 第41-43页 |
| 4．7 表达能力 | 第43-47页 |
| 第五章 自动验证 | 第47-54页 |
| 5．1 验证 | 第47-52页 |
| 5．1．1 追踪语义 | 第47-49页 |
| 5．1．2 追踪中加入时间 | 第49-50页 |
| 5．1．3 ω-自动机和验证 | 第50页 |
| 5．1．4 使用时间自动机验证 | 第50-52页 |
| 5．2 验证实例 | 第52-54页 |
| 第六章 结语 | 第54-55页 |
| 致谢 | 第55-56页 |
| 参考文献 | 第56-57页 |
