多值模型是传统布尔模型的扩展。与布尔模型相比,多值模型更适合对包含不确定和不一致信息的软件系统进行建模。为了解决模型检测时的状态爆炸问题,研究了对基于双格的多值模型的对称化简方法。提出了一种新的多值模型的精化关系,证明其保持对μ演算公式的模型检测结果的正确性。定义多值模型的对称化简商结构,证明商结构与原模型之间存在互为精化的关系,因此对μ演算公式的模型检测在二者上可以得到相同的结果。