Model Checking Multi-Agent Systems with MABLE

   page       BibTeX_logo.png   
Michael J. Wooldridge, Michael Fisher, Marc-Philippe Huget, Simon Parsons
Cristiano Castelfranchi, W. Lewis Johnson (eds.)
1st International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS 2002), pages 952-959
ACM, New York, NY, USA
15-19 July 2002

MABLE is a language for the design and automatic verification of multi-agent systems. MABLE is essentially a conventional imperative programming language, enriched by constructs from the agent-oriented programming paradigm. A MABLE system contains a number of agents, programmed using the MABLE imperative programming language. Agents in MABLE have a mental state consisting of beliefs, desires and intentions. Agents communicate using request and inform performatives, in the style of the fipa agent communication language. MABLE systems may be augmented by the addition of formal claims about the system, expressed using a quantified, linear temporal belief-desire-intention logic. MABLE has been fully implemented, and makes use of the spin model checker to automatically verify the truth or falsity of claims.

keywordsagents, model checking, programming, verification