TitleModel Checking Electronic Institutions
Publication TypeConference Paper
Year of Publication2002
AuthorsHuguet M-P, Esteva M, Phelps S, Sierra C, Wooldridge M
Conference NameMoChArt 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.