| 摘要 | 第4-6页 |
| ABSTRACT | 第6-7页 |
| 第一章 绪论 | 第12-20页 |
| 1.1 反应式并发系统及其形式化规范 | 第12-14页 |
| 1.2 混合规范 | 第14-15页 |
| 1.3 逻辑标记转换系统 | 第15-17页 |
| 1.4 本文的主要工作 | 第17-18页 |
| 1.5 本文的内容安排 | 第18-20页 |
| 第二章 预备知识 | 第20-26页 |
| 2.1 记号约定 | 第20页 |
| 2.2 逻辑标记转换系统与预备模拟关系 | 第20-23页 |
| 2.3 转换系统规范理论 | 第23-26页 |
| 第三章 CLL_R及其操作语义 | 第26-40页 |
| 3.1 CLL_R的语法及结构化操作语义规则 | 第26-29页 |
| 3.2 CLL_R的稳固模型与标记转换系统 | 第29-31页 |
| 3.3 CLL_R转换模型的基本性质 | 第31-38页 |
| 3.4 本章小结 | 第38-40页 |
| 第四章 展开、环境与转换 | 第40-58页 |
| 4.1 展开及其基本性质 | 第40-42页 |
| 4.2 环境与单步转换 | 第42-50页 |
| 4.3 τ转换序列和典范路径 | 第50-57页 |
| 4.4 本章小结 | 第57-58页 |
| 第五章 CLL_R的前同余性 | 第58-78页 |
| 5.1 若干引理 | 第58-71页 |
| 5.2 (?)RS的前同余性 | 第71-76页 |
| 5.3 本章小结 | 第76-78页 |
| 第六章 CLL_R的公理系统 | 第78-96页 |
| 6.1 公理系统AX_(CLL) | 第78-81页 |
| 6.2 AX_(CLL)的可靠性 | 第81-86页 |
| 6.3 范式定理与基完备性 | 第86-94页 |
| 6.4 本章小结 | 第94-96页 |
| 第七章 CLL_R中一类方程的解 | 第96-112页 |
| 7.1 唯一解定理 | 第96-105页 |
| 7.2 最大解定理 | 第105-110页 |
| 7.3 本章小结 | 第110-112页 |
| 第八章 CLL_R与基于动作的计算树逻辑 | 第112-126页 |
| 8.1 基于动作的计算树逻辑的一个片段在CLL_R中的编码 | 第112-113页 |
| 8.2 编码的正确性 | 第113-121页 |
| 8.3 例子 | 第121-124页 |
| 8.4 本章小结 | 第124-126页 |
| 第九章 总结与展望 | 第126-128页 |
| 参考文献 | 第128-138页 |
| 致谢 | 第138-140页 |
| 在学期间的研究成果及发表的学术论文 | 第140页 |