模糊计算树逻辑的模型检测修复算法  

The repair algorithm of model checking fuzzy computation tree logic

作　　者：毛兆东 钱俊彦 蔡泳 MAO Zhaodong;QIAN Junyan;CAI Yong(School of Computer and Information Security,Guilin University of Electronic Technology,Guilin 541004,China)

机构地区：[1]桂林电子科技大学计算机与信息安全学院,广西桂林541004

出　　处：《桂林电子科技大学学报》2020年第5期394-399,共6页Journal of Guilin University of Electronic Technology

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

摘　　要：为了解决基于模糊逻辑的模型检测修复问题,提出了模糊计算树逻辑模型检测的模型修复算法。该算法采用原子修复操作来修复模糊Kripke结构,通过模糊Kripke结构之间的距离比较原始的模糊Kripke结构和修复后的模糊Kripke结构,并从多个修复后的模糊Kripke结构中,选出满足给定模糊计算树逻辑的α-极小的修复模型作为算法的最终返回结果。研究结果表明,模糊计算树逻辑中的命题逻辑以及X的修复问题能够在多项式时间内得到解决。In order to solve the repair problem of model checking based on fuzzy logic,the model repair algorithms of model checking fuzzy computation tree logic are given.The algorithms use the primitive repair operations to repair the fuzzy Kripke structures,and compare the original fuzzy Kripke structures and the repaired fuzzy Kripke structures through the distance between the fuzzy Kripke structures,and choose theα-minimal repair model which satisfies the given fuzzy computation tree logic as the result of the algorithm from multiple fuzzy Kripke structures after repair.The result shows that the problem of propositional logic and and X formula of fuzzy computing tree logic can be solved in polynomial time.

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

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