Reasoning about BDI Agents from a Programming Languages Perspective.
Wayne Wobcke · 2007
In this paper, we summarize an approach to reasoning about a class of BDI agent architectures based on PRS. The theory is formalized using a logic, Agent Dynamic Logic (ADL), that combines elements from Computation Tree Logic, Proposi-tional Dynamic Logic and Rao and Georgeff’s BDI Logic. The motivation of this work is to develop a logical frame-work that is at once rigorous in providing formal notions of belief, desire and intention, yet which is also computationally grounded in the operational behaviour of this architecture, so as to enable formal reasoning about the behaviour of agents in this class. We illustrate the model theory with a simple “waypoint following ” agent. Methodology Following a symposium on intentions in communica-tion almost exactly twenty years ago, papers that were eventually published as Bratman (1990) and Cohen and Levesque (1990b) established a research direction in the in-teraction between philosophical and formal logic theories of intention and action, explicitly recognized in Allen’s com-mentary (Allen, 1990). Perhaps the main issue can be con-cisely stated as to provide a general formal modelling of in-tention and action (and their relationship) for rational agents that is consistent with philosophical theories of intention, action and rationality. Such a theory would enable reason-ing about rational agents using a logical approach, possibly even to prove the rationality of complex “BDI agents”, those based on notions of belief, desire and intention. The problem of developing a general logical theory of intention and rationality for BDI agents, however, remains open. We believe that part of the difficulty in developing such a general theory is that formal modellings inevitably build in some architectural assumptions about the agents they model, so inevitably a formal theory applies only to certain classes of BDI agents. Moreover, when it comes to reasoning about agents in that class, what is required is a systematic mapping from the computational states of the agent to formal BDI models. This requirement is what Wooldridge (2000) has called computational grounding. If a formal theory is not computationally grounded, properties