Model checking multi-agent systems with MABLE

MABLE is a language for the design and automatic verification of multi-agent systems. MABLE is essentially a conventional im-perative programming language, enriched by constructs from the agent-oriented programming paradigm. A MABLE system con-tains a number of agents, programmed using the MABLE imper-ative programming language. Agents in MABLE have a mental state consisting of beliefs, desires and intentions. Agents commu-nicate 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, ex-pressed 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