Towards a Rewriting Logic-Based Framework for Specifying FIPA Request Protocols

Abstract

This paper presents a practical and systematic approach for formally specifying interactions in multi-agent systems (MAS) based on the well-established FIPA request protocol. It aims to simplify and streamline the process of translating MAS interaction descriptions expressed with Agent UML diagrams into precise, unambiguous formal specifications using the Real-Time Maude language, which is founded on rewriting logic—a powerful and expressive formalism for specifying and analyzing concurrent and real-time systems. This integration enables enhanced analysis, rigorous verification, and validation of agent behaviors in complex and dynamic scenarios. The effectiveness and usability of the proposed approach are demonstrated through a detailed first aid case study, highlighting its practical applicability and benefits for designing reliable MAS interactions.