基于双格的多值模型的精化关系与对称化简
多值模型是传统布尔模型的扩展。与布尔模型相比，多值模型更适合对包含不确定和不一致信息的软件系统进行建模。为了解决模型检测时的状态爆炸问题，本文研究了对基于双格的多值模型的对称化简方法。为此，本文首先提出了一种新的多值模型的精化关系，证明其保持对“演算公式的模型检测结果的正确性。进一步，我们定义多值模型的对称化简商结构，证明商结构与原模型之间存在互为精化的关系，因此对Ⅳ演算公式的模型检测在两者上可以得到相同的结果。
陈娟娟 魏欧 黄志球 陈哲
南京航空航天大学计算机科学与技术学院,南京 210016
国内会议
南京
中文
1-9
2012-10-20（万方平台首次上网日期，不代表论文的发表时间）