第一章 绪论 1
1.1 研究背景 1
1.2 研究对象和成果 3
1.3 相关研究工作 4
1.4 本文结构 6
第二章 进程代数 7
2.1 引言 7
2.2 进程代数概论 8
2.3 通信系统演算CCS 10
2.4 传值CCS 12
2.5 π-演算 14
第三章 基于符号迁移图的互模拟验证算法：强和弱 17
3.1 引言 17
3.2 符号迁移图及其操作语义 18
3.3 迟弱互模拟和迟观察同余 22
3.4 迟符号观察图和迟符号同余图 28
3.5 互模拟验证算法 32
3.6 早互模拟 36
3.7 小结 39
第四章 STGA的变种及其互模拟验证：强和弱 40
4.1 引言 40
4.2 带赋值的符号迁移图 43
4.3 早强操作语义和早强互模拟 46
4.4 早弱互模拟和早观察同余 47
4.5 互模拟算法 52
4.6 迟互模拟 55
4.7 小结 57
第五章 π-演算的符号迁移图及其互模拟验证算法：强和弱 59
5.1 引言 59
5.2.1 布尔表达式、条件式、等名式和替换 60
5.2 π-演算及其符号迁移图 60
5.2.2 π-演算的符号迁移图 65
5.3 迟强操作语义和迟强互模拟 68
5.4 迟弱操作语义和迟弱互模拟 73
5.5 迟符号观察图和迟符号同余图 83
5.6 互模拟验证算法 86
5.7 早互模拟 91
5.8 小结 94
第六章 π-演算开互模拟的符号刻画和完备推理系统：强和弱 95
6.1 引言 95
6.2 π-演算的开互模拟 97
6.3 开互模拟的完全符号刻画 100
6.4 开互模拟的符号证明系统 104
6.5 弱开互模拟和开观察同余的完全符号刻画 108
6.6 开观察同余的符号证明系统 113
6.7 小结 117
第七章 带不等名测试的π-演算的开互模拟：强和弱 119
7.1 引言 119
7.2 π≠-演算的开互模拟 122
7.3 开互模拟的完全符号刻画 123
7.4 开互模拟的符号证明系统 127
7.5 弱开互模拟和开观察同余的完全符号刻画 133
7.6 开观察同余的符号证明系统 136
7.7 小结 141
第八章 结束语 143
8.1 本文的主要贡献 143
8.2 关于模型检测 145
8.3 未来的工作 146
致谢 148
攻读博士学位期间发表和出版的论文和著作 151
参考文献 153
后记 159