Volume 16, Number 1
Model Checking for Multi-Agent Systems Modeled by Epistemic Process Calculus
Authors
Qixian Yu 1, Zining Cao 1,2,3, Zong Hui 1,4 and Yuan Zhou 1, 1 Nanjing University of Aeronautics and Astronautics, China, 2 Ministry Key Laboratory for Safety-Critical Software Development and Verification, P. R. China, 3 Collaborative Innovation Center of Novel Software Technology and Industrialization, P. R. China, 4 Huaiyin Institute Of Technology, P. R. China
Abstract
This paper presents a comprehensive framework for modeling and verifying multi-agent systems. The paper introduce an Epistemic Process Calculus for multi-agent systems, which formalizes the syntax and semantics to capture the essential features of agent behavior interactions and epistemic states. Building upon this calculus, we propose ATLE, an extension of Alternating-time Temporal Logic incorporating epistemic operators to express complex properties related to agent epistemic state. To verify ATLE specifications, this paper presents a model checking algorithm that systematically explores the state space of a multi-agent system and evaluates the satisfaction of the specified properties. Finally, a case study is given to demonstrate the method
Keywords
Multi-agent System, Epistemic Logic, Value-Passing CCS, ATL, Model Checking.