On the Relationship Between BDI Logics and Standard Logics of Concurrency

The behavior of an agent is mainly governed by the specific way in which it handles the rational balance between information and deliberation. Rao and Georgeff's BDI theory is most popular among the formalisms capturing this very balance. This formalism has been proposed as a language for specifying agents in an abstract manner or, alternatively, for verifying various properties of agents implemented in some other programming language. In mainstream computer science, there are formalisms designed for a purpose similar to the BDI theory; not specifically aiming at agents, but at concurrency in general. These formalisms are known as logics of concurrent programs. In this paper these two frameworks are compared with each other for the first time. The result shows that the basic BDI theory, BDI_CTL*, can be captured within a standard logic of concurrency. The logic which is relevant here is Kozen's propositional -calculus. -calculus turns out to be even strictly stronger in expressive power than BDI_CTL* while enjoying a computational complexity which is not higher than that of BD_CTL*'s small fragment CTL. This correspondence puts us in a position to provide the first axiomatization of Rao and Georgeff's full theory. Immediate consequences for the computational complexity of BDI theory are also explored, both for theorem proving and model checking.