基于双格的多值模型精化关系及对称化简

• 作 者: 陈娟娟
• 发表日期: 2014年01期
• 关键词: 模型检测 多值模型 双格 精化关系 对称化简

模型检测是一种自动验证系统行为属性的技术。传统的模型检测针对基于布尔逻辑建立的系统模型，要求对系统的所有行为给予确定的描述。然而，在软件开发的许多阶段，如在需求分析阶段，由于用户的要求不明确以及观点的不一致，模型中可能包含不确定或不一致信息，传统布尔模型无法满足此要求，而多值模型更适合在此类情况下进行建模和分析。多值模型一般采用基于德摩根代数的多值逻辑来定义，是传统布尔模型的扩展。与传统模型检测类似，多值模型检测也存在状态爆炸问题。精化关系是采用抽象和对称化简等方法解决状态爆炸问题的基础，用来刻画系统的具体模型和约简模型之间相对于时序逻辑所描述的行为属性的保持关系。现有的针对多值模型的精化关系定义过强，适用范围受到限制。因此，我们提出了一种新的更加通用的多值模型精化关系，并且以此为基础研究了多值模型的对称化简方法。我们以世界双格作为理论基础,其中的逻辑值之间存在两种序关系：真值序关系与信息序关系。任意一个德摩根代数均同构于世界双格的一个子格；同时,对行为属性的模型检测可根据逻辑值的真值序关系定义,而模型检测结果的精确度以及具体模型和约简模型之间的属性保持关系则可根据逻辑值的信息序关系定义。为此，我们首先定义了基于世界双格的多值模型,以及时序逻辑μ演算所对应的语义。然后，我们从两个角度刻画了新的多值模型的精化关系：（i）通过将多值模型分解为三值模型进行刻画，(ii)直接针对多值模型的结构进行刻画；证明了这两种刻画等价，是具体模型与约简模型满足对μ演算公式的模型检测保持信息序关系的充分必要条件；给出识别多值模型状态上的精化关系的算法。进一步，以此精化关系基础，定义了多值模型的对称化简商结构，证明商结构与原模型之间存在互为精化的关系，将对称化简扩展到一般的多值模型上。