随着时代的不断发展,计算机软硬件系统的复杂度不断提高,形式化验证在计算机科学中的应用也越来越广泛。互模拟作为软件形式化验证方法的重要组成部分,有良好的数学性质,可以很好的描述系统行为之间的等价关系,满足互模拟关系的两个迁移系统可以模仿彼此的行为。互模拟等价验证算法主要分为全局算法与局部算法:全局算法主要用于判断任意的状态是否满足互模拟关系,需要预先知道整个系统的迁移关系;局部算法主要用于判断给定状态是否满足互模拟关系,只需对要判断的状态及其后续状态进行遍历,在对不满足互模拟关系的状态对进行判断时,具有更好的效率。局限于定性分析的经典系统模型已经不能满足实际需求,模糊理论作为分析系统不确定性的重要方法,受到了计算机工作者的广泛关注。从20世纪70年代开始,计算机科学工作者将模糊理论应用于迁移系统并对模糊迁移系统下的互模拟等价关系进行了深入的研究。为了更加快速地判断模糊迁移系统间的状态是否满足模糊互模拟关系,对模糊互模拟等价验证算法的研究显得尤为重要。本文的主要贡献如下:1.提出了模糊互模拟的等价类划分算法。模糊互模拟等价类划分算法是全局算法的一种,建立在划分精化的思想基础上。该算法不断利用迁移对状态进行等价类划分,同时也利用状态对迁移进行等价类划分,直到满足以下条件:（1）所有满足模糊互模拟条件的状态都在一个等价类中;（2）任意等价类中的状态都满足模糊互模拟关系。2.提出了模糊互模拟等价验证的局部算法。该算法采用深度优先遍历的方法,在对要判断的状态对及其后继状态对进行遍历的同时,对后继状态对是否满足模糊互模拟关系进行判断。最坏情况下,即当所有的后继状态都遍历完成时,算法给出最后的判断结果。3.使用Java语言对模糊互模拟等价类划分算法和模糊互模拟等价验证的局部算法进行实现。之后,通过理论分析与实验对比相结合的方式对模糊互模拟等价类划分算法、模糊互模拟等价验证的局部算法以及已有的全局算法相互进行比较,分析了不同情况下算法的运行效率,并对算法的优缺点以及适用性进行讨论和说明。