因为无穷状态系统拥有无穷多个状态，基于它的可判定性理论更加复杂，对于无穷状态系统的强、弱互模拟等价的判定比有穷状态系统的判定更有难度。我们对无穷状态系统BPA(Basic Process Algebra)、BPP(Basic ParallelProcesses)进程的互模拟等价的判定算法进行研究。研究BPA、BPP模型的行为，判断它们的互模拟等价。　　 首先，作者用tableau方法解决了totally normed BPA的弱互模拟等价的判定问题。作者研究与弱互模拟紧密相关的分解属性。同时，为了使弱互模拟判定具有分解属性，提出了相对于r的弱互模拟(weak bisimulation w.r.tГ)的定义，该定义是基于Hirshfeld的“弱互模拟相当”概念提炼得到。它是使用tableau方法证明可判定性的基础。然后，提出了tableau的规则，证明tableau方法的有限性，可靠性以及完备性。同时，简单分析其时间复杂度。　　 接着，作者使用tableau方法解决了totally normed BPP的弱互模拟等价判定问题。由于其同样没有像证明normed BPP强互模拟所使用的分解属性，因此，为了使tableau方法得以应用，作者应用“控制”和“改进”的概念，它是使用tableau方法证明可判定性的基础。根据BPP进程的特点，提出适用于弱互模拟判定的tableau的规则，同样给出tableau方法的有限性，可靠性以及完备性的证明，也显示如何从tableau系统获得一个可靠且完备的判定totally normedBPP进程弱互模拟等价的等式理论。　　 然后，作者将判定totally normed BPA的弱互模拟的限定条件减弱，使其norm值可以为零。这样，就会产生无穷分支的问题。为了更好的对问题的描述，作者应用弱迁移关系符号化特征的定义，分析了tableau方法得以应用的条件，提出新的规则解决无穷分支的问题。同样，给出tableau方法的有限性，可靠性以及完备性的证明。　　 最后，作者使用关系最粗划分(Relational Coarsest Partition)算法判定normed BPA的强互模拟等价。突破了这种算法只被用于证明有穷状态系统的等价问题，作者所做的工作是将这种算法应用于无穷状态系统的互模拟判定。因为它要求对系统的所有状态进行划分，但是，无穷状态系统的状态数是无穷多个，没有办法将它们全部枚举出来。作者的工作是将无穷状态空间的问题转化到有穷状态空间上解决，使得RCP算法得以应用。