循环对称化简及在三值模型上的扩展

• 作者: 徐丙凤 蔡昕烨 袁泳 魏欧 黄志球
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 模型检测 对称化简 循环对称 三值模型
• 年，卷（期）: 2011,（6）
• 所属期刊栏目: 形式化方法与工具专刊
• 页码范围: 1169-1184
• 分类号: TP301
• 字数: 13928字
• 语种: 中文
• DOI: 10.3724/SP.J.1001.2011.04020

摘要

为了将对称化简扩展到更多的非对称系统上,扩展了传统的基于自同构的对称性,提出了一种称为循环对称的新的对称性.证明了采用循环对称置换群或者由一组循环对称置换所生成的置换群仍可得到与原模型互模拟的对称商结构,从而达到化简系统规模的目的.进一步地,研究如何将对称化简应用于多值模型.多值模型可以有效地表示系统中的不确定信息,正越来越多地用于软件系统的建模与分析中.针对一种具体的多值模型--三值模型,定义传统的对称化简和循环对称化简在其上面的扩展.最后,分析三值模型的商结构与由约简得到的二值模型商结构之间的关系,证明了两种途径的等价性.