Model Checking for Multi-Agent Systems Modeled By Epistemic Process Calculus

2025/01/30 by Qingliang Yu, Zining Cao, Yu, Qixian +5
Business, Management and Accounting · Computer Science · #Business Process Modeling and Analysis #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Multi-Agent Systems and Negotiation #Semantic Web and Ontologies

paper · pdf · doi:10.48550/arxiv.2501.18155

openalex publication_date 2025/01/30 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

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.

Related

• A process algebraic framework for multi-agent dynamic epistemic systems
• Changing the Rules of the Game: Reasoning about Dynamic Phenomena in Multi-Agent Systems
• ATL*AS: An Automata-Theoretic Approach and Tool for the Verification of Strategic Abilities in Multi-Agent Systems
• Automatic Verification of Parameterised Interleaved Multi-Agent Systems
• Approximating Strategic Abilities under Imperfect Information: a Naive\n Approach