On the relationship between BDI logics and standard logics of concurrency

Abstract

The behavior of an agent is mainly governed by the specific way it handles the rational balance between information and deliberation. Most popular among the formalisms capturing this very balance is Rao and Georgeff’s BDI theory. 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 similar purpose as the BDI theory, though 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 for the first time compared with each other. The result shows that the basic BDI theory, BDICTL*, can be captured within a standard logic of concurrency. The logic relevant here is Kozen’s propositional μ-calculus. The μ-calculus turns out to be even strictly stronger in expressive power than BDICTL*, while enjoying a computational complexity which is not higher than that BDICTL* ’s small fragment CTL. This correspondence brings us in a position to give the first complete axiomatization of Rao and Georgeff’s full theory.