Specifying, Verifying and Implementing a MAS: A case study

Abstract

Abstract. This paper deals with the design of multi-agent systems. We demonstrate the goal-oriented agent model called Goal Decomposition Tree on an already studied multi-agent example, that of robots which must clean pieces of garbage on Mars. As we show, the model allows to prove that the agents ’ behaviour indeed achieves their goal. We then compare our approach to other ones. 1