Computation Tree Logic Model Checking of Multi-Agent Systems Based on Fuzzy Epistemic Interpreted Systems  

作　　者：Xia Li Zhanyou Ma Zhibao Mian Ziyuan Liu Ruiqi Huang Nana He 

机构地区：[1]School of Computer Science and Engineering,North Minzu University,Yinchuan,750000,China [2]School of Computer Science,FoSE,The University of Hull,Hull,UK

出　　处：《Computers, Materials & Continua》2024年第3期4129-4152,共24页计算机、材料和连续体（英文）

基　　金：The work is partially supported by Natural Science Foundation of Ningxia(Grant No.AAC03300);National Natural Science Foundation of China(Grant No.61962001);Graduate Innovation Project of North Minzu University(Grant No.YCX23152).

摘　　要：Model checking is an automated formal verification method to verify whether epistemic multi-agent systems adhere to property specifications.Although there is an extensive literature on qualitative properties such as safety and liveness,there is still a lack of quantitative and uncertain property verifications for these systems.In uncertain environments,agents must make judicious decisions based on subjective epistemic.To verify epistemic and measurable properties in multi-agent systems,this paper extends fuzzy computation tree logic by introducing epistemic modalities and proposing a new Fuzzy Computation Tree Logic of Knowledge(FCTLK).We represent fuzzy multi-agent systems as distributed knowledge bases with fuzzy epistemic interpreted systems.In addition,we provide a transformation algorithm from fuzzy epistemic interpreted systems to fuzzy Kripke structures,as well as transformation rules from FCTLK formulas to Fuzzy Computation Tree Logic(FCTL)formulas.Accordingly,we transform the FCTLK model checking problem into the FCTL model checking.This enables the verification of FCTLK formulas by using the fuzzy model checking algorithm of FCTL without additional computational overheads.Finally,we present correctness proofs and complexity analyses of the proposed algorithms.Additionally,we further illustrate the practical application of our approach through an example of a train control system.

关 键 词：Model checking multi-agent systems fuzzy epistemic interpreted systems fuzzy computation tree logic transformation algorithm 

分 类 号：TP18[自动化与计算机技术—控制理论与控制工程]