Verifiable semantic model for agent interactions using social commitments

Mohamed El-Menshawy, Jamal Bentahar, Rachida Dssouli

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

31 Scopus citations


Existing approaches about defining formal semantics of commitment usually consider operations as axioms or constrains on top of the commitment semantics, which fail to capture the meaning of interactions that are central to real-life business scenarios. Furthermore, existing semantic frameworks using different logics do not gather the full semantics of commitment operations and semantics of social commitments within the same framework. This paper develops a novel unified semantic model for social commitments and their operations. It proposes a logical model based on a new logic extending CTL* with commitments and operations to specify agent interactions. We also propose a new definition of assignment and delegation operations by considering the relationship between the original and new commitment contents. We prove that the proposed model satisfies some properties that are desirable when modeling agent interactions in MASs and introduce a NetBill protocol as a running example to clarify the automatic verification of this model. Finally, we present an implementation and report on experimental results of this protocol using the NuSMV and MCMAS symbolic model checkers.

Original languageBritish English
Title of host publicationLanguages, Methodologies, and Development Tools for Multi-Agent Systems - Second International Workshop, LADS 2009, Revised Selected Papers
Number of pages25
StatePublished - 2010
Event2nd International Workshop on Languages, Methodologies and Development Tools for Multi-agent Systems, LADS 2009 - Torino, Italy
Duration: 7 Sep 20099 Sep 2009

Publication series

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


Conference2nd International Workshop on Languages, Methodologies and Development Tools for Multi-agent Systems, LADS 2009


  • accessibility relations
  • Social commitments
  • the NuSMV and MCMAS model checkers
  • two and three party operations


Dive into the research topics of 'Verifiable semantic model for agent interactions using social commitments'. Together they form a unique fingerprint.

Cite this