Verifying MSMAS model using CIFF

Emad Eldeen Elakehal, Marco Montali, Julian Padget

Research output: Chapter or section in a book/report/conference proceedingChapter in a published conference proceeding

3 Citations (SciVal)


MSMAS is a software development methodology that facilities the design and development of complex distributed systems based on the multiagent systems paradigm. MSMAS explicitly supports the institutional organisational structure and follows a declarative modelling style to specify behavioural restrictions on the members of the institution, their roles, the business processes regulating their behavior and the communication protocols regulating their mutual interactions. All these aspects are visually represented, by adapting the DECLARE graphical language, proposed for the declarative specification of constraint-based business processes. In this paper we discuss the main elements of MSMAS, and show how they can be equipped with a formal, expectation-based semantics, tailored to the CIFF Abductive Logic Programming-based framework. In particular, we show how the MSMAS constructs can be formalized in CIFF, and then exploit this correspondence to specify and verify formal properties over MSMAS models, by leveraging on the CIFF reasoning capabilities.

Original languageEnglish
Title of host publicationMultiagent System Technologies - 11th German Conference, MATES 2013, Proceedings
Number of pages15
Publication statusPublished - 9 Oct 2013
Event11th German Conference on Multiagent System Technologies, MATES 2013 - Koblenz, Germany
Duration: 16 Sept 201320 Sept 2013

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8076 LNAI
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference11th German Conference on Multiagent System Technologies, MATES 2013

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'Verifying MSMAS model using CIFF'. Together they form a unique fingerprint.

Cite this