An outline of the use of transition systems to formalize JADE agents and multi-agent systems

This paper presents the key aspects of a proposed formalization of JADE agents and multi-agent systems based on transition systems. Such a formalization is meant to be useful to describe and clarify how JADE multi-agent systems work and to provide a theoretical instrument to validate and analyze the semantics of JADE agents. This is needed to decouple agent-oriented and object-oriented parts of an agent design and to avoid misunderstandings on the semantics of JADE agents. The chosen approach is to define a structural operational semantics for Java programs written using JADE, and the proposed formalization consists in two parts: the first identifies and defines the main entities that together compose a JADE multi-agent system; the second provides the transition system and rewriting rules. The paper terminates with two explanatory examples of the usage of the transition system. A brief recapitulation of the work concludes the paper.