On the Semantics and Verification of Normative Multi-Agent Systems

This paper presents a programming language that facilitates the implementation of coordination artifacts which in turn can be used to regulate the behaviour of individual agents. The programming language provides constructs inspired by social and organisational concepts. Depending on the scheduling mechanism of such constructs, different operational semantics can be defined. We show how one such possible operational semantics can be prototyped in Maude, which is a rewriting logic software. Prototyping by means of rewriting is important since it allows us both to design and to experiment with the language definitions. To illustrate this, we define particular properties (like enforcement and regimentation) of the coordination artifacts which we then verify with the Maude LTL model-checker.