Specification and Verification of Multi-Agent Systems with a Property-Preserving Component-Based Methodology

This paper presents a property-preserving component-based methodology for the specification and verification design of the Multi-agent system (MAS). It is assumed that the behavior of each agent in the MAS is specified as a Petri net process (PNP). According to the communication relationships between the agents, the system is specified and verified by applying the composition operators such as Enable, Choice, Interleave, Disable and Disable-resume. The local goals and system goals (Commitment) are specified as coverable markings in the Petri net models for the MAS. The methodology eliminates the requirements of verifying the MAS since the composition operators preserve the desirable properties (i. e., liveness, boundedness, reversibility, proper termination and coverability).