Towards an approach for behavioral specification of Reactive Multi-Agent system

Reactive Multi-Agent system (RMAS) has emerged as an attractive technology for the design and implementation of distributed and cooperative systems. The RMAS main challenge is how to clearly identify its local and global behavior. Several approaches have been introduced to deal with behavioral specification of RMAS. However, there is a lack in the specification and verification process that facilitates understanding the system from goals identification that the system expects to achieve to formal verification of system properties. In this paper, we are interested to the specification problem of Reactive Multi-Agent System (RMAS) for both individual and collective behavior by taking into account two modes of specification: normal mode and fault-tolerance mode. To do so, we propose a method called BECAMEDA (Behavioral SpEcification and VerifiCAtion of RMAS based on E-MDRA) for the specification and verification of reactive Multi-agent system based on the MDRA (Multi-Decisional Reactive Agent) models. The MDRA specifies the reactive agent behavior by highlighting the decisional aspect of the agent. The BECAMEDA method will be described throughout an example of Car Crisis Management.