A refinement framework for autonomous agents

Abstract

An autonomous agent is one that is not only directed by its environment, but is also driven by internal motivation to achieve certain goals. The popular Belief-Desire-Intention (BDI) design paradigm allows such agents to adapt to environmental changes by calculating a new execution path to their current goal, or when necessary turning to another goal. In this paper we present an approach to modelling autonomous agents using an extension to Object-Z. This extension supports both data and action refinement, and includes the use of LTL formulas to describe an agent's desire as a sequence of prioritised goals. It turns out, however, that the introduction of desire-driven behaviour is not monotonic with respect to refinement. We therefore introduce an additional refinement proof obligation to enable the use of simulation rules when checking refinement. © 2013 Springer-Verlag.