基于分解的多值模型的逼近关系

发布时间：2019-06-14 09:42

【摘要】：多值模型可用于对包含不确定与不一致信息的软件系统进行建模与验证。提出了采用基于分解的方式来刻画多值模型之间的逼近关系,这为采用抽象方法解决模型检测时所产生的状态爆炸问题奠定了理论基础。为此,首先给出了多值模型分解为多个三值模型的方法,并且证明了任意μ演算公式在多值模型上的检测结果等于在分解后所有三值模型上的检测结果的合并。进一步,由三值模型上的混合模拟关系给出了多值模型间逼近关系的结构定义,并证明对于任意给定的两个满足逼近关系的多值模型,μ演算公式在其上的检测结果在信息序关系上得以保持。
[Abstract]:Multi-valued model can be used to model and verify software systems with uncertain and inconsistent information. In this paper, a decomposition-based approach is proposed to depict the approximate relationship between multivalued models, which lays a theoretical foundation for solving the state explosion problem caused by model detection by abstract method. In this paper, the method of decomposing the multi-valued model into multiple ternary models is given, and it is proved that the detection results of any 渭 calculus formula on the multi-valued model are equal to the combination of the detection results on all the ternary models after decomposition. Furthermore, the structure definition of the approximation relation between the multivalued models is given from the mixed simulation relation on the ternary model, and it is proved that for any given two multivalued models satisfying the approximation relation, the detection results of the 渭 formula can be maintained in the information order relation.
【作者单位】：南京航空航天大学计算机科学与技术学院;
【基金】：国家自然科学基金项目(61170043,61100034)资助
【分类号】：TP306

【参考文献】