Specifying recursive agents with GDTs

The purpose of this article is to formalise the notion of recursive agent by extending the Goal Decomposition Tree formalism (GDT). A formal semantics of this decomposition is given, as well as the definition of operators to introduce various ways of recursively defining agents. Design patterns, that show various use cases for recursive agents, are also presented. Finally, to preserve the essential GDT characteristics (that is to allow the verification of agents behaviours), we give proof schemas that allow a proof of the correctness of a recursive agent.