Rafael H. Bordini, Michael Fisher, Carmen Pardavila, Michael J. Wooldridge
Jeffrey S. Rosenschein, Michael J. Wooldridge, Tuomas Sandholm, Makoto Yokoo (a cura di)
2nd International Joint Conference on Autonomous Agents and Multi-Agents Systems (AAMAS 2003), pp. 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.
parole chiave
AgentSpeak(F), AgentSpeak(L), BDI Logic, Multiagent Systems
evento origine
