Proving the effectiveness of negotiation protocols KQML in multi-agent systems using event-B

Abstract

Multi-Agents Systems (MAS) provide a good basis to build complex systems and in MAS a negotiation is a key form of interaction that enables agents to arrive at a final agreement. We present an event-B based approach to reasoning about a negotiation protocols in multi-agent systems (MAS), Key features of Event-B are the use of set theory as a modeling notation and it is a formal method that can be used in the development of reactive distributed systems and we propose using the Rodin modeling tool for Event-B that integrates modeling and proving. © Springer International Publishing AG 2017.