International Journal of Software Engineering & Applications(IJSEA)

 Submit your Research Articles!!

International Journal of Software Engineering & Applications(IJSEA)

ISSN:0975-3834 [Online]; 0975-4679 [Print]

ERA Indexed, H Index 34

Web Page URL : https://airccse.org/journal/ijsea/ijsea.html

Current Issue link: https://www.airccse.org/journal/ijsea/vol16.html

Paper Title : 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.

Abstract URL :https://aircconline.com/abstract/ijsea/v16n1/16125ijsea01.html

Article URL :https://aircconline.com/ijsea/V16N1/16125ijsea01.pdf

Submission System: https://airccse.com/submissioncs/home.html

Contact Us : ijseajournal@airccse.org or ijsea@aircconline.com

Youtube URL: https://www.youtube.com/watch?v=kCAeRdXOLc0

#multiagent #system #epistemic #logic #valuepassing #ccs #atl #model #checking