© 1998 by Oxford University Press
| ||||||||||||||||||||||||||||||||||||||||||||||||||
Original Articles |
Decision Procedures for BDI Logics
Mitchell Madison Group Level 49, 120 Collins Street, Melbourne, Victoria 3000, Australia E-mail: anand_rao{at}mmg.net.au
Australian Artificial Intelligence Institute Level 6, 171 La Trobe Street, Melbourne, Australia. E-mail: georgeff{at}aaii.oz.au
The study of computational agents capable of rational behaviour has received increasing attention in recent years. A number of theoretical formalizations for such multi-agent systems have been proposed. However, most of these formalizations do not have a strong semantic basis nor a sound and complete axiomatization. Hence, it has not been clear as to how these formalizations could assist in building agents in practice. This paper explores a particular type of multi-agent system, in which each agent is viewed as having the three mental attitudes of belief (B), desire (D), and intention (I). It provides a family of multi-modal branching-time BDI logics with a possible-worlds semantics, categorizes them, provides sound and complete axiomatizations, and gives constructive tableau-based decision procedures for testing the satisfiability and validity of formulas. The computational complexity of these decision procedures is no greater than the complexity of their underlying temporal logic component.
Keywords: Rational agents; belief-desire-intention (BDI) model; multi-modal logic; modal logic; theorem proving; tableaux methods; branching time temporal logic; temporal logic
CiteULike 
Connotea 
Del.icio.us What's this?
This article has been cited by other articles:
|
|
 |
|
  R. H. Bordini, M. Fisher, M. Wooldridge, and W. Visser Property-based Slicing for Agent Verification J Logic Computation, June 16, 2009; (2009) exp029v1. [Abstract] [PDF]
|
|
|
|
|
|
V. Rybakov Linear Temporal Logic LTLK extended by Multi-Agent Logic Kn with Interacting Agents J Logic Computation, May 4, 2009; (2009) exp027v1. [Abstract] [PDF]
|
|