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