有界模型检测是寻找系统错误的一种符号化模型检测技术。它使用可满足性问题求解器求解模型检测问题，避免了其他模型检测技术面临的状态空间爆炸问题，然而它的计算时间复杂度是指数级别的。有界模型检测方法的一个最大不足是，它虽然能有效的证明系统不满足某一性质，但很难或不能证明系统满足某一性质，即只能证伪不能证实。所以有界模型检测对系统的验证是不完全的或者说是不完备的。每一个有限状态系统模型M和线性时态逻辑公式δ，都存在一个自然数CT，如果找不到长度小于CT的线性时态逻辑公式δ的反例，那么系统模型满足公式δ，记作M|=δ，这个自然数称为完备性阈值CT(CompletenessThreshold)。完备性阈值的计算是很困难的，有时候计算出来的值是巨大的。本文讨论了系统模型的表示，提出系统关键变量和等价简化模型的概念，通过寻找非系统关键变量来合并系统状态，得到等价简化模型。在这个模型上计算完备性阈值，提高了计算的效率同时得到简化模型的缩小的完备性阈值。本文实现了基于深度优先搜索的算法来计算可达性递归直径，修正了以往算法存在的对同一状态可能重复计算的缺点。最后通过实验分别对本文算法和模型简化策略进行测试，结果表明：本文算法计算出的可达递归直径是正确的而且在递归直径大于40的时候开始表现出好于以往算法的效果；采用本文方法构造出优先队列模型的等价简化模型，计算其递归直径更加直观，而且保证了简化模型同样满足验证性质。本文的方法可应用于有界模型检测器的实现以提高其有效性。