Performative Patterns for Designing Verifiable ACLs

When people hear two actors reciting a conversation in a poem, they become attuned to the kinds of sounds that they are producing, which may not be apparent in the printed text of the poem. This result depends on certain habitual patterns of how people read or how things should be read in a performance. Performative patterns suggest certain kinds of rhythmic possibilities, time, timbre and intonation, which are not written on the page. Although their scope is quite different we claim that agents' conversations are subject to similar principles. In the same way agents' conversations are not completely specified by the logical description of the involved performatives and rules governing speech act interaction are needed to guarantee a reproducible and thus verifiable behaviour. In this paper we present a set of performative patterns for ACLs which specify how performatives should be executed in a concurrent and reactive way with respect to a given logical semantics. We provide a classification of the KQML and FIPA performatives in these patterns and we show how several properties of Multi-Agent Systems can be inferred and verified if an ACL adopt this approach.