APICe » Publications » MableAamas2002

Model Checking Multi-Agent Systems with MABLE

Michael J. Wooldridge, Michael Fisher, Marc-Philippe Huget, Simon Parsons
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.
Keywords: agents, model checking, programming, verification
1st International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS 2002), pages 952-959, 15-19 July 2002.
Cristiano Castelfranchi, W. Lewis Johnson (eds.), ACM, New York, NY, USA
	Address = {New York, NY, USA},
	Author = {Wooldridge, Michael J. and Fisher, Michael and Huget, Marc-Philippe and Parsons, Simon},
	Booktitle = {1st International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS 2002)},
	Doi = {10.1145/544862.544965},
	Editor = {Castelfranchi, Cristiano and Johnson, W. Lewis},
	Isbn = {1-58113-480-0},
	Location = {Bologna, Italy},
	Month = {15--19~} # jul,
	Pages = {952--959},
	Publisher = {ACM},
	Title = {Model Checking Multi-Agent Systems with {MABLE}},
	Url = {http://dl.acm.org/citation.cfm?doid=544862.544965},
	Volume = 2,
	Year = 2002}