多目Pi演算互模拟等价自动验证研究

论文摘要

本文通过对多目Pi演算的强开互模拟等价自动化验证算法的研究，针对已有算法中存在大量的递归调用、冗余数据、执行效率低等问题，建立了一套全新的数据结构用来表示多目Pi演算算式，并在此基础之上提出了对已有算法的优化建议。在多目Pi演算的强开互模拟等价自动化验证优化算法中，提出了一种新的算法执行方案，对算法中关键的Add方法和Match方法做出了修正，使得算法在处理拥有大量的并行与选择、抽象与凝结因子的多目Pi演算算式的时候，算法递归深度大量减少。同时对算法中的二元关系R和D的处理做出了修正，使得算法运行过程中的冗余数据大量减少，算法执行效率得到了优化。另外，本文还讨论了多目Pi演算的α等价与其强开互模拟等价验证之间的关系，并提出并实现了一个可行的α等价验证算法，使得算法整体的递归深度进一步减少，同时α等价验证算法也可以作为一个独立的功能呈现。

论文目录

• 摘要
• Abstract
• 第1章 引言
• 1.1 研究背景及课题意义
• 1.2 研究现状
• 1.3 本文的主要工作
• 1.4 本文的组织结构
• 第2章 多目 Pi 演算及其强开互模拟等价验证算法
• 2.1 多目 Pi 演算及其强开互模拟等价定义
• 2.1.1 多目 Pi 演算
• 2.1.2 多目 Pi 演算互模拟等价
• 2.2 互模拟等价验证算法
• 2.2.1 多目 Pi 演算互模拟等价定义的等价形式
• 2.2.2 多目 Pi 演算互模拟等价的验证算法
• 第3章 互模拟等价验证程序设计
• 3.1 互模拟等价验证程序的总体设计
• 3.1.1 算式的树形数据结构存储
• 3.1.2 总体操作流程
• 3.2 算式绘制算法以及节点点选算法
• 3.2.1 绘制算法
• 3.2.2 鼠标点选节点算法
• 3.3 树形数据结构存储详细设计
• 3.3.1 占位符节点类型
• 3.3.2 进程节点类型、向量节点类型以及名字节点类型
• 3.3.3 一元要素节点类型
• 3.3.4 二元要素节点类型
• 3.3.5 二叉树的形式化定义
• 3.4 本章小结
• 第4章 互模拟等价验证算法的优化与实现
• 4.1 对于二元关系 R 和 D 的处理
• 4.1.1 二元关系 R 和 D 的数据结构
• 4.1.2 对 R 和 D 的处理的优化
• 4.2 对算法中后继集合的处理
• 4.2.1 不同形式算式结构的后继集合
• 4.2.2 对 tree 数据结构的补充
• 4.3 对方法 add 和 match 的优化
• 4.3.1 对 add 的优化以及实现
• 4.3.2 对 match 的优化以及实现
• 4.4 本章小结
• 第5章 α变换以及α等价验证算法
• 5.1 α等价与互模拟等价验证算法的关系
• 5.1.1 α变换以及α等价
• 5.1.2 α等价对于互模拟等价算法的意义
• 5.2 α等价验证算法以及实现
• 5.2.1 α等价验证算法
• 5.2.2 α等价验证算法的实现
• 5.3 本章小结
• 第6章 实验与分析
• 6.1 抽象与凝结对算法改进前后的影响
• 6.2 并行与选择对算法改进前后的影响
• 6.3 本章小结
• 第7章 结语
• 参考文献
• 作者简介及在学期间所取得的科研成果
• 致谢