Towards a Rewriting Logic-Based Framework for Specifying FIPA Request Protocols
DOI:
https://doi.org/10.22399/ijcesen.4007Keywords:
Interaction Protocols, FIPA Request, rewriting logic, Real-Time Maude, First AidAbstract
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.
References
[1] Ölveczky, P. C. (2014, April). Real-Time Maude and its applications. In International Workshop on Rewriting Logic and its Applications (pp. 42-79). Cham: Springer International Publishing. https://doi.org/10.1007/978-3-319-12904-4_3
[2] Mokhati, F., Sahraoui, B., Bouzaher, S., & Kimour, M. T. (2010). A tool for specifying and validating agents’ interaction protocols: From Agent UML to Maude. Object Technology, 9(3). http://www.jot.fm/issues/issue_2010_05/article2/
[3] Mokhati, F., Boudiaf, N., Badri, M., & Badri, L. (2007). Translating AUML Diagrams into Maude Specifications: A Formal Verification of Agents Interaction Protocols. J. Object Technol., 6(4), 77-102. http://www.jot.fm/issues/issue_2007_05/article2
[4] FIPA Request Interaction Protocol Specification. 2002. http://www.fipa.org/specs/fipa00026/index.html
[5] Eker, S., Martí-Oliet, N., Meseguer, J., Rubio, R., & Verdejo, A. (2023). The Maude strategy language. Journal of Logical and Algebraic Methods in Programming, 134, 100887. https://doi.org/10.1016/j.jlamp.2023.100887
[6] Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., & Talcott, C. (2007). All about maude-a high-performance logical framework: how to specify, program, and verify systems in rewriting logic (Vol. 4350). Springer.
[7] Meseguer, J. (2012). Twenty years of rewriting logic. The Journal of Logic and Algebraic Programming, 81(7-8), 721-781. https://doi.org/10.1016/j.jlap.2012.06.003
[8] Liu, S. (2019). Design, verification and automatic implementation of correct-by-construction distributed transaction systems in Maude (Doctoral dissertation, University of Illinois at Urbana-Champaign)
[9] Liu, S., Ölveczky, P. C., Zhang, M., Wang, Q., & Meseguer, J. (2019, April). Automatic analysis of consistency properties of distributed transaction systems in Maude. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems (pp. 40-57). Cham: Springer International Publishing. https://doi.org/10.1007/978-3-030-17465-1_3
[10] Ölveczky, P. C. (2016, September). Formalizing and validating the P-Store replicated data store in Maude. In International Workshop on Algebraic Development Techniques (pp. 189-207). Cham: Springer International Publishing. https://doi.org/10.1007/978-3-319-72044-9_13
[11] Garavel, H., Tabikh, M. A., & Arrada, I. S. (2018, June). Benchmarking implementations of term rewriting and pattern matching in algebraic, functional, and object-oriented languages: The 4th rewrite engines competition. In International Workshop on Rewriting Logic and its Applications (pp. 1-25). Cham: Springer International Publishing. https://doi.org/10.1007/978-3-319-99840-4_1
[12] Olveczky, P. C. (2007). Real-time maude 2.3 manual. Department of Informatics, University of Oslo, 180.
[13] Durán, F., Eker, S., Escobar, S., Martí-Oliet, N., Meseguer, J., Rubio, R., & Talcott, C. (2024, September). Programming open distributed systems in Maude. In Proceedings of the 26th International Symposium on Principles and Practice of Declarative Programming (pp. 1-12).
https://doi.org/10.1145/3678232.3678237
[14] Liu, S., Meseguer, J., Ölveczky, P. C., Zhang, M., & Basin, D. (2022). Bridging the semantic gap between qualitative and quantitative models of distributed systems. Proceedings of the ACM on Programming Languages, 6(OOPSLA2), 315-344. https://doi.org/10.1145/3563299
[15] Amouroux, E., Chu, T. Q., Boucher, A., & Drogoul, A. (2007, November). GAMA: an environment for implementing and running spatially explicit multi-agent simulations. In Pacific Rim International Conference on Multi-Agents (pp. 359-371). Berlin, Heidelberg: Springer Berlin Heidelberg.
Downloads
Published
How to Cite
Issue
Section
License
Copyright (c) 2025 International Journal of Computational and Experimental Science and Engineering
This work is licensed under a Creative Commons Attribution 4.0 International License.
