INFDok - Dokumentenvolltextserver des Fachbereichs Informatik

Kurzfassung auf Englisch:

The question of modelling and verification of agent-oriented systems is our research area. In multi agent systems the interplay of three parts of the system - called Delta-pattern - is central: first, local elements (e.g. agents), second, global elements (e.g. the multi agent system), and, third, the composition structure (e.g. the mobility structure in the agent system). The dynamic nature of agent systems makes composition a concept on its own rather than an implicit aspect of the two other concepts. Multi agent systems are based on three major concepts: mobility, adaptivity, and cooperation, which are structured by the Delta-pattern. In this presentation we focus on agent conversations to present a model, which describes the interplay of local and global parts as well as the dynamic configuration structure of a conversation. This model is based on the multi agent architecture MULAN - designed at our department. It is used to model mobility, adaptivity, and cooperation in a unified way. MULAN is a Petri net based architecture, which is both an implementation of a multi agent platform and also a framework for the modelling of agent applications. Here we deal with the analysis of liveness preserving composition of Petri nets. The two areas of agent-oriented modelling and compositional verification - both in the setting of the Petri net theory - are combined by dealing with a class of models which have a restricted structure: For the special case of communication closed protocols it is shown that liveness of conversations is a structural property. This result is of crucial importance to compose agent protocols at run-time.