Towards a Unified Approach for Modeling and Verification of Multi-Agent Systems

Abstract

For complex software systems an agent-oriented design is assumed. The question of modeling and verification is our research area. In this presentation we outline an unified approach for multi agent systems with respect to modeling and verification. This general architecture called - Mulan - is formulated in terms of high level Petrinets, namely reference nets. The formalism of reference nets is based on the "nets within nets" paradigm of Valk, which fits well in the context of agent systems. Here, we first show how multi agent systems should be modeled. In the second step we analyze which are the requirements for a verification systems dealing with multi agent systems. In both cases we arrive at the conclusion that reference nets are well suited to model and verify central aspects of agent systems, like mobility, adaptation, and cooperation. In this work we focus on modeling and verification of agent conversations. Our approach is based on inter-acting agent protocols. To express our ideas we have chosen the well known producer-consumer scenario both for the model and the formal treatment.