Model Checking AgentSpeak

   page       BibTeX_logo.png   
Rafael H. Bordini, Michael Fisher, Carmen Pardavila, Michael J. Wooldridge
Jeffrey S. Rosenschein, Michael J. Wooldridge, Tuomas Sandholm, Makoto Yokoo (eds.)
2nd International Joint Conference on Autonomous Agents and Multi-Agents Systems (AAMAS 2003), pages 409-416
ACM Press, New York, NY, USA
11-14 July 2003

This paper introduces AgentSpeak(F), a variation of the BDI logic programming language AgentSpeak(L) intended to permit the model-theoretic verification of multi-agent systems. After briefly introducing AgentSpeak(F) and discussing its relationship to AgentSpeak(L), we show how AgentSpeak(F) programs can be transformed into Promela, the model specification language for the Spin model-checking system. We also describe how specifications written in a simplified form of BDI logic can be transformed into Spin-format linear temporal logic formul. With our approach, it is thus possible to automatically verify whether or not multi-agent systems implemented in AgentSpeak(F) satisfy specifications expressed as BDI logic formul. We illustrate our approach with a short case study, in which we show how BDI properties of a simulated auction system implemented in AgentSpeak(F) were verified.

keywordsAgentSpeak(F), AgentSpeak(L), BDI Logic, Multiagent Systems
origin event