Open Access

ARTICLE

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

Xia Li¹, Zhanyou Ma^1,*, 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

* Corresponding Author: Zhanyou Ma. Email:

Computers, Materials & Continua 2024, 78(3), 4129-4152. https://doi.org/10.32604/cmc.2024.047168

Received 27 October 2023; Accepted 05 February 2024; Issue published 26 March 2024

Abstract

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.

---

Keywords

---