APICe » Publications » AgentspeakAamas2003

Model Checking AgentSpeak

Rafael H. Bordini, Michael Fisher, Carmen Pardavila, Michael J. Wooldridge
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.
Keywords: AgentSpeak(F), AgentSpeak(L), BDI Logic, Multiagent Systems
2nd International Joint Conference on Autonomous Agents and Multi-Agents Systems (AAMAS 2003), pages 409-416, 11-14 July 2003.
Jeffrey S. Rosenschein, Michael J. Wooldridge, Tuomas Sandholm, Makoto Yokoo (eds.), ACM Press, New York, NY, USA
	Address = {New York, NY, USA},
	Author = {Bordini, Rafael H. and Fisher, Michael and Pardavila, Carmen and Wooldridge, Michael J.},
	Booktitle = {2nd International Joint Conference on Autonomous Agents and Multi-Agents Systems (AAMAS 2003)},
	Doi = {10.1145/860575.860641},
	Editor = {Rosenschein, Jeffrey S. and Wooldridge, Michael J. and Sandholm, Tuomas and Yokoo, Makoto},
	Isbn = {1-58113-683-8},
	Location = {Melbourne, Australia},
	Month = {11-14~} # jul,
	Pages = {409--416},
	Publisher = {ACM Press},
	Title = {Model Checking {A}gent{S}peak},
	Url = {http://dl.acm.org/citation.cfm?doid=860575.860641},
	Year = 2003}