JUCS - Journal of Universal Computer Science 15(13): 2629-2652, doi: 10.3217/jucs-015-13-2629
On the Semantics and Verification of Normative Multi-Agent Systems
expand article infoLăcrămioara Aştefănoaei, Mehdi Dastani§, John-Jules Meyer§, Frank S. De Boer
‡ CWI, Amsterdam, Netherlands§ Universiteit Utrecht, Utrecht, Netherlands
Open Access
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.
multi-agent systems, norms, verification, rewriting logic