Verifying Multi -Agent Coordination Correctness for BDI Agents

The popular Belief-Desire-Intention (BDI) architecture structures agents' behavior around beliefs, desires, and intentions, enabling effective pursuit of collective objectives and optimal system performance. Many complex situations require agent developers to design a coordination model/plan involving multiple BDI agents working together to achieve a given goal. However, a semantic notion of state has been missing in most current accounts of BDI agent execution, making it impossible to assess at design time if a coordination model/plan is able to achieve the goal. Thus, in this paper, we introduce a framework that permits us to identify the state that accrues at any point in agent execution. This enables us to determine, at design time, if a multi-agent coordination model/plan accomplishes a given goal. Our framework facilitates the verification of coordination correctness in such complex multi-agent systems.