| 摘要 | 第1-5页 |
| ABSTRACT | 第5-13页 |
| 插图索引 | 第13-14页 |
| 第一章 引言 | 第14-26页 |
| ·CCS的由来 | 第14-15页 |
| ·研究现状和问题：观察理论 | 第15-19页 |
| ·进程的行为等价 | 第15-18页 |
| ·本文对观察理论的贡献 | 第18-19页 |
| ·研究现状和问题：表达能力 | 第19-22页 |
| ·Turing完备性 | 第19-20页 |
| ·相对表达能力 | 第20-21页 |
| ·本文对表达能力的贡献 | 第21-22页 |
| ·研究现状和问题：等价性验证 | 第22-24页 |
| ·等价验证问题 | 第22-23页 |
| ·本文对等价验证的贡献 | 第23-24页 |
| ·章节安排 | 第24-26页 |
| 第二章 基本术语 | 第26-42页 |
| ·CCS语言 | 第26-36页 |
| ·有限核心 | 第26-29页 |
| ·表达无限行为 | 第29-31页 |
| ·名的辖域和传名的能力 | 第31-32页 |
| ·选择操作子 | 第32-33页 |
| ·Alpha-转换？否？ | 第33-36页 |
| ·归约语义 | 第36页 |
| ·LTS上的常见关系及基本性质 | 第36-42页 |
| ·双模拟类关系的定义 | 第37-38页 |
| ·证明强双模拟等价的up-to技术 | 第38页 |
| ·强双模拟等价的性质 | 第38-39页 |
| ·测试类关系的定义 | 第39-41页 |
| ·行为性质 | 第41-42页 |
| 第三章 观察理论(I) ――行为相等的模型无关刻画 | 第42-66页 |
| ·什么是观察理论？ | 第42-45页 |
| ·对环境的假设 | 第42-43页 |
| ·模型无关刻画 | 第43-44页 |
| ·可扩展性（Extensionality） | 第44页 |
| ·交互能力（Interactive Capability） | 第44-45页 |
| ·可扩展性（Extentionality）和等势性（Equipollence） | 第45-47页 |
| ·共发散（Codivergence）和双模拟（Bisimulation） | 第47-50页 |
| ·双模拟性质 | 第47-48页 |
| ·发散守恒和共发散 | 第48-50页 |
| ·基于双模拟的相等：动态环境 | 第50-56页 |
| ·双模拟相等的定义 | 第50-51页 |
| ·行为性质 | 第51-52页 |
| ·一致性结果 | 第52-54页 |
| ·分离结果 | 第54-55页 |
| ·进一步讨论 | 第55-56页 |
| ·没有双模拟的相等：静态环境 | 第56-63页 |
| ·◇-相等和□-相等的定义 | 第57页 |
| ·行为性质 | 第57-58页 |
| ·迹等价和潜在失败等价 | 第58-61页 |
| ·一致性结果 | 第61-62页 |
| ·分离结果 | 第62-63页 |
| ·关于发散守恒性的新的思考 | 第63-66页 |
| 第四章 观察理论(II) ――行为近似的模型无关刻画 | 第66-82页 |
| ·什么是行为前序关系 | 第67-68页 |
| ·前序上的行为性质的定义 | 第68-69页 |
| ·行为前序：静态环境 | 第69-73页 |
| ·模型无关定义 | 第69-70页 |
| ·模型无关的行为性质 | 第70-71页 |
| ·一致性结果 | 第71-73页 |
| ·分离结果 | 第73页 |
| ·基于模拟的行为前序：动态环境 | 第73-80页 |
| ·模型无关的定义 | 第73-75页 |
| ·行为性质 | 第75-76页 |
| ·迹守恒（弱）模拟前序和失败守恒（弱）模拟前序 | 第76-77页 |
| ·一致性结果 | 第77-79页 |
| ·分离结果 | 第79-80页 |
| ·观察理论的总结 | 第80-82页 |
| 第五章 表达能力 | 第82-124页 |
| ·CCS~(Pdef)的Turing完备性 | 第82-87页 |
| ·Minsky机器与停机问题 | 第82-83页 |
| ·用CCS~(Pdef) 建模Minsky 机器 | 第83-85页 |
| ·CCS~(sPdef) 和CCS~(-Pdef） 的终止问题 | 第85-86页 |
| ·重标号 | 第86页 |
| ·带名俘获的递归 | 第86-87页 |
| ·相对表达能力及其评判标准 | 第87-89页 |
| ·相对表达能力的模型无关刻画 | 第87-88页 |
| ·CCS各子语言的相对表达能力评判标准 | 第88-89页 |
| ·CCS~μ和CCS~! 的相互翻译 | 第89-92页 |
| ·将CCS~! 翻译到CCSμ | 第89-90页 |
| ·将CCS~μ翻译到CCS~! | 第90-92页 |
| ·带护卫递归算子的CCS~μ | 第92-102页 |
| ·将CCS~! 翻译到CCS~(Gμ) | 第92-95页 |
| ·消去不受护卫的变量 | 第95-97页 |
| ·消去不受护卫的复制形式的变量 | 第97-98页 |
| ·消去受护卫的复制 | 第98-99页 |
| ·CCS~μ翻译到CCSG~μ | 第99-102页 |
| ·将CCSμ翻译到CCS~!（续） | 第102页 |
| ·CCS~! 的膨胀序 | 第102-109页 |
| ·序理论的知识 | 第102-103页 |
| ·并发范式 | 第103页 |
| ·忽略局部化算子的并发子表达式 | 第103-104页 |
| ·局部名嵌套深度 | 第104-105页 |
| ·结构膨胀序 | 第105-107页 |
| ·膨胀性质的证明 | 第107-109页 |
| ·CCS~μ和CCS~! 不具备Turing完备性 | 第109-111页 |
| ·不具备能力定义Count | 第109-110页 |
| ·发散问题的可判定性 | 第110页 |
| ·Turing完备性总结 | 第110-111页 |
| ·CCS~μ的膨胀序 | 第111-119页 |
| ·递归范式 | 第111-112页 |
| ·忽略局部化算子的并发子表达式 | 第112-114页 |
| ·局部名嵌套深度 | 第114-116页 |
| ·结构膨胀序 | 第116-117页 |
| ·膨胀性质的证明 | 第117-119页 |
| ·选择子的表达能力 | 第119-122页 |
| ·对已有的结果的影响 | 第119页 |
| ·用分离选择编码混合选择 | 第119-121页 |
| ·缺少选择操作子 | 第121-122页 |
| ·相对表达能力总结 | 第122-124页 |
| 第六章 双模拟等价和模拟前序的（不）可判定性 | 第124-144页 |
| ·导引 | 第124-127页 |
| ·局部名和进程表达能力 | 第124-125页 |
| ·本章的工作 | 第125-127页 |
| ·预备知识 | 第127-128页 |
| ·强双模拟的博弈刻画 | 第127页 |
| ·Minsky机器与停机问题（续） | 第127页 |
| ·防御者的胁迫 | 第127-128页 |
| ·带标号的Petri网和它的标号迁移语义 | 第128页 |
| ·CCS_·~μ～CCS_·~μ的不可判定性 | 第128-132页 |
| ·基本构造 | 第128-130页 |
| ·不可判定性证明 | 第130-132页 |
| ·CCS_·~! ～CCS_·~! 的不可判定性 | 第132-136页 |
| ·基本构造 | 第132-133页 |
| ·不可判定性证明 | 第133-136页 |
| ·与有限状态进程的强双模拟等价 | 第136-140页 |
| ·CCS~! ～FS 的不可判定性 | 第136-138页 |
| ·CCS_·~! ～FS 的可判定性 | 第138-140页 |
| ·与有限状态进程的强模拟前序 | 第140-142页 |
| ·FS(?)CCS_·~! 和CCS_·~!(?)FS的可判定性 | 第140页 |
| ·FS(?)CCS~!的可判定性 | 第140-142页 |
| ·等价验证可判定性总结 | 第142-144页 |
| 第七章 待解决的问题 | 第144-148页 |
| ·关于有限进程的证明系统 | 第144-145页 |
| ·关于有限状态进程的证明系统 | 第145-146页 |
| ·关于表达能力 | 第146-148页 |
| 参考文献 | 第148-158页 |
| 致谢 | 第158-160页 |
| 攻读学位论文期间发表的学术论文目录 | 第160-163页 |
| 上海交通大学博士学位论文答辩决议书 | 第163页 |
