基于模糊多智能体系统的模型检测  

Model checking based on fuzzy multi-agent systems

作　　者：马占有[1] 李霞 高滢囡 刘子源 MA Zhanyou;LI Xia;GAO Yingnan;LIU Ziyuan(School of Computer Science and Engineering,North Minzu University,Yinchuan 750021,China)

机构地区：[1]北方民族大学计算机科学与工程学院,宁夏银川750021

出　　处：《华中科技大学学报（自然科学版）》2024年第11期64-71,共8页Journal of Huazhong University of Science and Technology(Natural Science Edition)

基　　金：宁夏自然科学基金资助项目(AAC03300);北方民族大学研究生创新资助项目(YCX23152)。

摘　　要：针对智能体之间沟通产生的异构性,采用社会可及性关系来形式化表示智能体之间的沟通,并对具有非确定性沟通的多智能体系统模型检测问题进行研究.首先引入模糊解释系统模型对具有非确定性沟通的多智能体系统进行描述;其次在模糊计算树逻辑的基础上添加承诺和实现模态词,得到带承诺的模糊计算树逻辑,用于描述系统的属性;然后提出一种间接的模型检测算法,将基于模糊解释系统的带承诺模糊计算树逻辑的模型检测问题转换为基于模糊Kripke结构的模糊计算树逻辑的模型检测问题;最后给出该算法的正确性证明和复杂度分析.研究结果表明:所提出的间接模糊模型检测算法不仅能够有效处理具有非确定性沟通的多智能体系统属性验证问题,而且在处理复杂性方面表现出更优的性能,验证了其在实际应用中的可行性和有效性.The heterogeneity arising from communication between agents was addressed by using social accessibility relations to formalize the communication between agents.The problem of model checking for multi-agent systems with uncertain communication was studied.First,a fuzzy interpreted system model was introduced to describe fuzzy multi-agent systems with uncertain communication.Next,based on fuzzy computation tree logic,commitment and fulfillment modal operators were added to obtain a fuzzy computation tree logic with commitments,which was used to describe the properties of the system.Then,an indirect model checking algorithm was proposed,converting the model checking problem of fuzzy computation tree logic with commitments based on fuzzy interpreted systems into a model checking problem of fuzzy computation tree logic based on fuzzy Kripke structures.Finally,the correctness proof and complexity analysis of the algorithm were provided.Research results show that the proposed indirect fuzzy model checking algorithm not only effectively handles the property verification problem of fuzzy multi-agent systems with uncertain communication but also demonstrates superior performance in terms of handling complexity,validating its feasibility and effectiveness in practical applications.

关 键 词：多智能体系统 模糊解释系统 模糊计算树逻辑 转换算法 模型检测 

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