| 摘要 | 第3-5页 |
| Abstract | 第5-6页 |
| 第一章 前言 | 第10-18页 |
| 第二章 预备知识 | 第18-28页 |
| 2.1 格的基本知识 | 第18-20页 |
| 2.2 交替自动机 | 第20-24页 |
| 2.2.1 交替自动机的相关概念和性质 | 第20-23页 |
| 2.2.2 交替Buchi自动机与线性时序逻辑模型检测的联系 | 第23-24页 |
| 2.2.3 有向非循环图 | 第24页 |
| 2.3 格值自动机及格值计算树逻辑模型检测的相关概念 | 第24-28页 |
| 2.3.1 格值自动机和格值树自动机 | 第25-26页 |
| 2.3.2 格值计算树逻辑模型检测相关概念 | 第26-28页 |
| 第三章 格值交替自动机 | 第28-46页 |
| 3.1 格值正布尔公式 | 第28-29页 |
| 3.1.1 格值正布尔公式的概念 | 第28页 |
| 3.1.2 格值正布尔公式的等价性 | 第28-29页 |
| 3.2 格值交替自动机的相关概念 | 第29-32页 |
| 3.3 格值交替自动机的代数性质 | 第32-45页 |
| 3.3.1 格值交替自动机的表达能力 | 第33-36页 |
| 3.3.2 格值交替自动机的闭包性质 | 第36-45页 |
| 3.4 本章小结 | 第45-46页 |
| 第四章 格值交替Buchi自动机及若干可判定性问题 | 第46-70页 |
| 4.1 格值交替Buchi自动机的概念 | 第46-48页 |
| 4.2 格值交替Buchi自动机的代数性质 | 第48-67页 |
| 4.2.1 格值交替Buchi自动机的表达能力 | 第48-58页 |
| 4.2.2 格值交替Buchi自动机的闭包性质 | 第58-67页 |
| 4.3 格值交替Buchi自动机的若干可判定性问题 | 第67-68页 |
| 4.3.1 格值交替Buchi自动机的emptiness-值和universality-值问题 | 第67-68页 |
| 4.3.2 格值交替Buchi自动机的implication-值问题 | 第68页 |
| 4.4 本章小结 | 第68-70页 |
| 第五章 格值交替树自动机 | 第70-84页 |
| 5.1 格值交替树自动机的概念 | 第70-72页 |
| 5.2 格值交替树自动机的代数性质 | 第72-83页 |
| 5.2.1 格值交替树自动机的闭包性质 | 第72-76页 |
| 5.2.2 格值交替树自动机的表达能力 | 第76-83页 |
| 5.3 本章小结 | 第83-84页 |
| 第六章 格值交替Buchi树自动机与格值计算树逻辑模型检测 | 第84-108页 |
| 6.1 格值交替Buchi树自动机的概念 | 第84-86页 |
| 6.2 格值交替Buchi树自动机的代数性质 | 第86-91页 |
| 6.2.1 格值交替Buchi树自动机的闭包性质 | 第86-87页 |
| 6.2.2 格值交替Buchi树自动机的表达能力 | 第87-91页 |
| 6.3 格值交替Buchi树自动机与格值计算树逻辑模型检测的联系 | 第91-105页 |
| 6.3.1 广义格值交替Buchi树自动机的相关概念和表达能力 | 第92-93页 |
| 6.3.2 从格值计算树逻辑公式到广义格值交替Buchi树自动机 | 第93-102页 |
| 6.3.3 格值计算树逻辑模型检测研究的自动机方法 | 第102-105页 |
| 6.4 本章小结 | 第105-108页 |
| 第七章 结束语 | 第108-112页 |
| 7.1 研究内容的总结 | 第108-109页 |
| 7.2 可进一步研究的相关问题 | 第109-112页 |
| 参考文献 | 第112-122页 |
| 致谢 | 第122-124页 |
| 攻读博士学位期间的研究成果 | 第124页 |
