|Títol||Model Checking Electronic Institutions|
|Publication Type||Conference Paper|
|Year of Publication||2002|
|Authors||Huguet M-P, Esteva M, Phelps S, Sierra C, Wooldridge M|
|Conference Name||MoChArt 2002 at ECAI 2002|
The design and development of open multiagent systems is one of the main areas in multiagent research. Human societies have successfully coped with a similar issue by creating institutions, which can broadly be understood as formal or semi-formal frameworks that provide commonly understood collections of rules within which people can interoperate. In ongoing work, we have been developing a framework called ISLANDER for the specification and developed of electronic institutions, within which software agents can meet and interoperate within a commonly understood terms of reference. This framework includes both a formal specification language for institutions and software tools to assist in their construction. In this paper, we are concerned with providing tools to support the design-time verification and validation of such institutions. We present some preliminary results in the use of a SPIN-based multiagent model checking framework called MABLE to enable verification of ISLANDER models.
- Quant a IIIA