Multiagent technology has many interesting potential applications, but it seems that the more interesting the application is to society, the more demands it puts on the technology in terms of correctness and reliability. These issues have not yet been deeply explored in the area of multiagent systems. From this perspective, this contribution is a very important step in that direction.

The authors consider how to use a well-known tool for software verification, Spin, to verify a multiagent specification language, AgentSpeak(L). This specification language has to be fit into process metalanguage (PROMELA), the input language for Spin. Due to syntax and semantics mismatches between AgentSpeak(L) and PROMELA, the proposal provides verification for a subset of AgentSpeak(L), termed AgentSpeak(F). Further restrictions have to be made to accommodate the original specification and the fact that Spin only deals with finite-state systems. Channels are used for communication between agents.

The main activities that are typical of the belief-desire-intention (BDI) paradigm in modeling multiagent systems, belief revision, checking interagent communication, event selection, and intention selection are considered atomic activities, so interleaving is focused on them. A mapping from BDI logic properties to linear temporal logic formulas, the language for property specification accepted by Spin, is provided.

Exercises in this line of inquiry are very important, and many lessons can be learned about which particular functions a specification language can request from an already-existing verification technology. However, the ultimate goal would be to have tools that are more specifically equipped to deal efficiently with all the distinctive features of languages like AgentSpeak(L).