时间自动机可达性检测方法研究
| 摘要 | 第1-4页 |
| Abstract | 第4-8页 |
| 第一章 前言 | 第8-12页 |
| ·研究背景 | 第8-9页 |
| ·研究现状及内容 | 第9-11页 |
| ·本文结构 | 第11-12页 |
| 第二章 相关基础知识 | 第12-23页 |
| ·时间自动机 | 第12-15页 |
| ·时钟约束、时钟解释 | 第12-13页 |
| ·时间转换表 | 第13页 |
| ·时间自动机的语法 | 第13-14页 |
| ·时间自动机的语义 | 第14页 |
| ·时间自动机中的运行 | 第14-15页 |
| ·时钟区域及时钟带 | 第15-17页 |
| ·时钟区域 | 第15-16页 |
| ·时钟带 | 第16-17页 |
| ·不同界限值矩阵DBM | 第17-18页 |
| ·区域矩阵和n-自动机 | 第18-21页 |
| ·区域矩阵 | 第18-19页 |
| ·n-自动机 | 第19-21页 |
| ·布尔函数和BDD’s | 第21-23页 |
| 第三章 状态可达性计算 | 第23-53页 |
| ·可达性分析 | 第23-24页 |
| ·基于时钟区域的状念等价划分法 | 第24-28页 |
| ·求解含有不同时钟相互约束时间自动机的可达性关系 | 第28-36页 |
| ·时间自动机语义的符号化表示 | 第28页 |
| ·理论分析 | 第28-31页 |
| ·对标准化算法的改进 | 第31-36页 |
| ·使用BDD近似求解时间自动机的状态可达性关系 | 第36-46页 |
| ·使用BDD表示时钟带 | 第36-38页 |
| ·使用BDD表示时间自动机 | 第38-39页 |
| ·时钟带上的操作 | 第39-41页 |
| ·计算状态可达性关系 | 第41-42页 |
| ·计算可达性关系的算法实现 | 第42-44页 |
| ·对算法的分析 | 第44-46页 |
| ·基于复位点语义的状态可达性算法 | 第46-53页 |
| ·时间自动机表示形式的修改 | 第46页 |
| ·复位点语义 | 第46-47页 |
| ·基本运算分析 | 第47-49页 |
| ·基本运算的模型化 | 第49-53页 |
| 第四章 算法分析与改进 | 第53-58页 |
| ·算法分析 | 第53-54页 |
| ·算法改进 | 第54-58页 |
| ·改进的算法 | 第54-56页 |
| ·改进算法的正确性和可行性分析 | 第56-57页 |
| ·应用实例 | 第57-58页 |
| 第五章 总结与展望 | 第58-59页 |
| 致谢 | 第59-60页 |
| 参考文献 | 第60-65页 |
| 附录1 攻读硕士学位期间发表的论文 | 第65页 |
