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.