Title: Specifying and verifying holonic agents with GDT4MAS
Author: B. Mermet, G. Simon
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.
Int. J. of Agent-Oriented Software Engineering, 2010 Vol.4, No.3, pp.281 - 303
Submission date: 07 Dec 2009
Date of acceptance: 08 Jul 2010
Available online: 20 Nov 2010