Model checking agentspeak

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. Categories and Subject Descriptors I.2.11 [Artificial Intelligence]: Distributed Artificial Int...

• Type: Conference
• Year: 2003
• Where: ATAL
• Authors: Rafael H. Bordini, Michael Fisher, Carmen Pardavila, Michael Wooldridge
• Keywords: ATAL 2003, BDI Logic, Bdi Logic Programming, Logic Formulæ