模糊Kripke结构的子模型修复算法  

The Sub-model Repair Algorithm of Fuzzy Kripke Structures

作　　者：王辉[1] 石铁柱 钱俊彦[1] 潘海玉 WANG Hui;SHI Tiezhu;Qian Junyan;PAN Haiyu(Guangxi Key Laboratory of Trusted Software,Guilin University of Electronic Technology,Guilin 541004,China;School of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 210000,China)

机构地区：[1]桂林电子科技大学广西可信软件重点实验室,广西桂林541004 [2]南京航空航天大学计算机科学与技术学院,江苏南京210000

出　　处：《郑州大学学报（理学版）》2023年第1期77-83,共7页Journal of Zhengzhou University:Natural Science Edition

基　　金：国家自然科学基金项目(62162014);广西自然科学基金项目(2018GXNSFAA281326);广西可信软件重点实验室项目(kx201911)。

摘　　要：在模糊模型检测时,如果模糊Kripke结构不满足性质规约,模型检测工具会给出模型中违反性质规约的反例,这往往需要设计人员手工修复,会导致效率低下,因此如何对模糊Kripke结构进行自动修复具有极大的研究意义。由此,提出一个基于模糊tableaux方法的子模型修复算法,从而将经典的模型修复算法提升到模糊系统中,使得模糊Kripke结构能够自动修复。通过一个医疗诊断的例子来阐述该算法在实际中的价值。In fuzzy model checking, if a fuzzy computation tree logic formula was not satisfied in the fuzzy Kripke structure, a counter example would be generated to identify errors. However, the existing model-checking methods needed manual repair. How to repair the models automatically was of great significance. A sub-model repair algorithm based on analytic fuzzy tableaux was proposed, to put the classical model repair algorithm into fuzzy systems. The practical value of sub-model was illustrated by an medical diagnosis example.

关 键 词：模型检测 计算树逻辑 模糊逻辑 模型修复 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]