Decision procedures for prepositional linear-time belief-desire-intention logics

Abstract

The study of situated systems that are capable of reactive and goal-directed behaviour has received increased attention in recent years. One approach to the design of such systems is based upon agent-oriented architectures, in which the system is viewed as a rational agent having certain mental attitudes. The description of these mental attitudes has led to the development of expressive logics that combine multiple modalities of beliefs, desires, and intentions with temporal modalities to describe or specify the behaviours of agents. However, none of these logics have sound and complete axiomatizations or tractable constructive decision procedures. In this paper, we consider some of the propositional variants of these BDI-logics based on a linear-time model and provide sound and complete axiomatizations and tableau-based decision procedures. Although the paper considers only BDI-logics the techniques can be applied to multi-modal logics with interacting modalities.