Model checking agentspeak

10 years 11 months ago
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...
Rafael H. Bordini, Michael Fisher, Carmen Pardavil
Added 06 Jul 2010
Updated 06 Jul 2010
Type Conference
Year 2003
Where ATAL
Authors Rafael H. Bordini, Michael Fisher, Carmen Pardavila, Michael Wooldridge
Comments (0)