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

Corresponding author: Lăcrămioara Aştefănoaei ( l.astefanoaei@cwi.nl )

© Lăcrămioara Aştefănoaei, Mehdi Dastani, John-Jules Meyer, Frank De Boer.
This article is freely available under the J.UCS Open Content License.
Citation: Aştefănoaei L, Dastani M, Meyer J-J, De Boer FS (2009) On the Semantics and Verification of Normative Multi-Agent Systems. JUCS - Journal of Universal Computer Science 15(13): 2629-2652. https://doi.org/10.3217/jucs-015-13-2629
Open Access
Abstract
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.
Keywords
multi-agent systems, norms, verification, rewriting logic