形式化验证已经成为对系统设计和协议设计进行确认的重要手段,其方法分为两类<[42]>,一类是以逻辑推理为基础,另一类则以穷尽搜索为基础,穷尽搜索方法统称为模型检验.逻辑推理的不足之处在于推理的难度.对于稍微复杂的系统,自动化的推理就难以胜任.模型检验的好处在于它有全自动化的检验过程,并且如果一个性质不满足,它能给出这个性质不满足的理由,可据此对系统设计进行改进.状态爆炸[6]是模型检验中的一个重要难题.实际系统中的状态数目可能很大,以至无法在有限的时间和内存空间下进行完整的检验.对称归约是处理状态爆炸问题的有效技术之一.但是在实际系统验证时,如果是处于公平条件下,已有的对称归约算法很难有有效的作用.而在实际应用中,公平性是验证一些性质的先决条件.该文给出了一个模型检验的算法,在公平条件下利用对称归约化简状态空间,以改善状态爆炸问题.这个算法基于嵌套深度优先搜索(NDFS)算法.它假定要检验的性质用Buchi自动机<[19]>给定,因此,检验系统是否支持某个给定性质的问题,就归结为在图中寻找接受回路的问题<[7,6]>.该文首先叙述并分析了标准的NDFS算法<[7,17]>和带对称归约的NDFS算法<[3]>;然后通过对模型检验器Spin中的弱公平性算法(由Holzmann实现)进行扩展,提出了一个在弱公平条件下、未使用对称归约的、基于嵌套深度优先搜(NDFS)的模型检验策略,最后在此基础上提出基于NDFS的融合弱公平性和对称归约的算法.相对于基于寻找最大强连通分支(MSCC)的类似算法<[11,14]>,该算法具有基于NDFS的优势,每个状态的空间开销也要少,而且,虽然与它们有相同的最坏时间复杂度O(N·| h(T)|),但是在检测到性质的一个反例时,该算法需要遍历的状态要少得多,因此具有更好的时间和空间复杂性,同时也兼容于近似验证技术.该文还把这个算法的原型运用在通用的模型检验器Spin之上,对Peterson互斥协议等例子的进行验证实验.实验的结果显示,该文的算法使对称归约在弱公平条件下的化简效果接近于它不在弱公平条件约束下的化简效果.