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

TL;DR

This paper introduces a new formal framework combining an epistemic process calculus with an extended temporal logic for modeling and verifying complex multi-agent system behaviors and knowledge states.

Contribution

It develops an epistemic process calculus and an extension of ATL with epistemic operators, along with a model checking algorithm for verifying multi-agent systems.

Findings

Successful formalization of multi-agent behaviors and knowledge states

Effective model checking algorithm for ATLE specifications

Case study demonstrating practical applicability

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.