Model Checking Cooperative Multi-agent Systems in BDI Logic

Traditional temporal logics such as LTL (Linear Temporal Logic) and CTL (Computation Tree Logic) have shown tremendous success in specifying and verifying hardware and software systems. However, this kind of logic can only model the dynamic behaviors for a single system, and fall short in capturing the joint and concurrent aspects in the composition of systems, such as the interactions and coordinations of agents in Multi-agent Systems. Although ATL (Alternating-time Temporal Logic) can solve the problem to a certain extent, by preceding the temporal operators with a selective path quanti?er, to specify that the interactions between entities inside the system can make sure that there is a strategy to reach a certain state, it can not formalize the rational mental attitudes of the agents such as the Belief, Desire and Intention (BDI) which plays an essential role in decision making during cooperation with other agents. This paper will investigate this problem by proposing a logic of ATLBDI (Alternatingtime Temporal Logic of Belief Desire and Intention) and discuss the algorithmic issues such as model checking algorithms and the computational complexity, along with examples to show its e?ectiveness. We conclude that model checking for ATLBDI is completely tractable and is in PTIME-Complete, which is quite an optimistic and promising result for further applications.