Model Checking for Multi-Agent Systems Modeled By Epistemic Process Calculus
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , , |
|---|---|
| Format: | Preprint |
| Publié: |
2025
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866910805822275584 |
|---|---|
| author | Yu, Qixian Cao, Zining Hui, Zong Zhou, Yuan |
| author_facet | Yu, Qixian Cao, Zining Hui, Zong Zhou, Yuan |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2501_18155 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Model Checking for Multi-Agent Systems Modeled By Epistemic Process Calculus Yu, Qixian Cao, Zining Hui, Zong Zhou, Yuan Formal Languages and Automata Theory 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. |
| title | Model Checking for Multi-Agent Systems Modeled By Epistemic Process Calculus |
| topic | Formal Languages and Automata Theory |
| url | https://arxiv.org/abs/2501.18155 |