Formal specification of role components in open multi-agent systems

Roles are an important concept used for different purposes like the modeling of organizational structure of multi-agent systems, the modeling of protocols, and as basic building blocks for defining the behavior of agents. Modeling interactions by roles gives several advantages, the most important of which is the separation of concerns by distinguishing the agent-level and system-level with regard to interaction. However, in open MASs, the composition of independently developed roles may lead to unexpected emergent behavior of the agents. This paper identifies requirements for modeling role-based interactions, and presents a formal specification model of roles for complex interactions. Our approach aims to integrate specification and verification into the Component Based Development (CBD) of roles. An application example of interactions protocols is given to illustrate our formal framework.