本论文第二章主要介绍研究的基础和主要方法工具，有了研究基础和主要方法才能为后续工作奠定基础。第三章主要介绍等价性判断算法，首先要考虑如何在两个进程之间构造一个交织互模拟，即可判断等价。除此之外，用约简算法进行等价性论证分析也是很有必要的。第四章主要用举例子的方式来验证交互进程等价，共给出三个例子，其中由第三个例子得出来的结果表明“商进程”和“原进程”之间是行为等价的，这在判断两个进程等价时可以作为一个很好的方法工具，也有很多好的应用。

......

进程代数是一门很好的刻画并发系统的高层语言，建立了进程的对称性概念，用等价关系表示系统中的对称性。因此，进程代数的操作语义在研究交互进程之间的行为等价时，可作为一种很好的方法和工具。

采用事件结构建模，引用了置换群的对称性概念。等价关系就是建立在置换群上，置换群中的每一个置换就是一个自同构，它刻画了该系统相同或同构的组件。在此基础上，称该置换群为自同构群。事件结构具有对称性，意味着存在非平凡的置换群（自同构群）。

引入了事件结构的商结构模型，证明了商结构与事件结构是互模拟等价的。同时建立了针对事件结构的对称约简算法，阐明了对称约简不改变等价在动作细化下的保持。据此还建立了对称约简算法，验证了约简算法的正确性，并证明了约简后的进程与进程是交织互模拟等价的。具体工作总结如下。

（1）等价性判断算法

在论文第三章中，引用了商进程结构。商进程结构是基于进程项集合上的一个自同构群得到的。它的行为是明确的，所涉及到的动作集合和进程的动作集合是相同的。商进程是一个独立的进程，且保留了进程的行为。在此基础上，为了研究在动作细化下行为等价是否保持问题，在商进程和进程之间，用归纳法构造了一个交织互模拟。可以得到：商进程和进程是交织互模拟等价的。根据这些结论建立了对称约简算法，并用例子说明对称约简是不影响等价行为在动作细化下的保持，是有必要且有意义的工作。

（2）约简算法

在论文给出的例子中，很好的说明了在对进程进行对称约简后得到的商进程，其行为与进程是等价的。它能够完整地刻画“原进程”的整个行为。这可以作为一个桥梁，有助于进一步的研究两个进程之间是否行为等价。

商事件结构与事件结构的交织迹、交织互模拟等价在动作细化下是保持的，说明对称约简不仅保留了事件结构的行为和结构，还保留了事件结构的性质。在模型检验中，对称约简也是有效的约简算法。在此基础上，建立了对称约简算法，并举例说明了算法的正确性。