Title: Specifying and verifying holonic agents with GDT4MAS

Authors: B. Mermet, G. Simon

Addresses: GREYC-UMR 6072 and Universite du Havre, Campus Cote de Nacre, Boulevard du Marechal Juin, BP 5186, 14032 CAEN Cedex, France. ' GREYC-UMR 6072 and Universite du Havre, Campus Cote de Nacre, Boulevard du Marechal Juin, BP 5186, 14032 CAEN Cedex, France

Abstract: This paper describes how specific holonic multi-agent systems can be specified and how their correctness can be proven with an extended version of the GDT4MAS model. This model allows the specification of multi-agent systems and the verification of their correctness with theorem proving techniques. Introducing holonic agents in this model allows the enhancement of its expressiveness. Moreover, the proof system associated to this model can be easily extended in order to prove the correctness of multi-agent systems using such agents. The paper first describes the initial GDT4MAS model. Then the need for some kinds of holonic agents and their proposed specification based on specific decomposition operators are presented. It is followed by a focus on how the proof system can be adapted to prove the correctness of the behaviour of these new agents. Last but not least, all these proposals are illustrated on a case study.

Keywords: holonic agents; formal specification; verification; multi-agent systems; MAS; agent-based systems.

DOI: 10.1504/IJAOSE.2010.036985

International Journal of Agent-Oriented Software Engineering, 2010 Vol.4 No.3, pp.281 - 303

Received: 07 Dec 2009
Accepted: 08 Jul 2010
Published online: 20 Nov 2010 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article