Verifying conformance of multi-agent commitment-based protocols

Mohamed El-Menshawy, Jamal Bentahar, Warda El Kholy, Rachida Dssouli

Research output: Contribution to journalArticlepeer-review

42 Scopus citations


Although several approaches have been proposed to specify multi-agent commitment-based protocols that capture flexible and rich interactions among autonomous and heterogeneous agents, very few of them synthesize their formal specification and automatic verification in an integrated framework. In this paper, we present a new logic-based language to specify commitment-based protocols, which is derived from ACTL *c, a logic extending CTL * with modalities to represent and reason about social commitments and their actions. We present a reduction technique that formally transforms the problem of model checking ACTL *c to the problem of model checking GCTL * (an extension of CTL * with action formulae). We prove that the reduction technique is sound and we fully implement it on top of the CWB-NC model checker to automatically verify the NetBill protocol, a motivated and specified example in the proposed specification language. We also apply the proposed technique to check the compliance of another protocol: the Contract Net protocol with given properties and report and discuss the obtained results. We finally develop a new symbolic algorithm to perform model checking dedicated to the proposed logic.

Original languageBritish English
Pages (from-to)122-138
Number of pages17
JournalExpert Systems with Applications
Issue number1
StatePublished - Jan 2013


  • Commitment-based protocols
  • Multi-agent systems
  • Reduction
  • Symbolic model checking
  • Verification


Dive into the research topics of 'Verifying conformance of multi-agent commitment-based protocols'. Together they form a unique fingerprint.

Cite this