Specification and verification of reconfigurable multi-agent system architectures

摘要

Multi-Agent Systems (MAS) can be subject to changes reflecting the continuous emergence of new requirements. Thus, diversity of the basics on one hand, and the complexity of the concepts related to agents on the other hand, make it difficult to conceive and develop a reconfigurable multi-agent system architecture. In this paper, we relay on formal methods to manage the complexity of these aspects and reason on the design of MAS architectures. Precisely, we propose a formal modelling approach based on Bigraphs (BRS) for the specification of multi-agent system architectures and their reconfiguration. BRS present a promising and effective solution for the development of high quality and safe MAS at reasonable cost and time span. In addition, they enable the verification of MAS relevant properties using a bigraphical model checking tool named BigMC.