Specification and automatic verification of trust-based multi-agent systems

Nagat Drawel, Hongyang Qu, Jamal Bentahar, Elhadi Shakshuki

Research output: Contribution to journalArticlepeer-review

36 Scopus citations


We present a new logic-based framework for modeling and automatically verifying trust in Multi-Agent Systems (MASs). We start by refining TCTL, a temporal logic of trust that extends the Computation Tree Logic (CTL) to enable reasoning about trust with preconditions. A new vector-based version of interpreted systems is defined to capture the trust relationship between the interacting parties. We introduce a set of reasoning postulates along with formal proofs to support our logic. Moreover, we present new symbolic model checking algorithms to formally and automatically verify the system under consideration against some desirable properties expressed using the proposed logic. We fully implemented our proposed algorithms as a model checker tool called MCMAS-T on top of the MCMAS model checker for MASs along with its new input language VISPL (Vector-extended ISPL). We evaluated the tool and reported experimental results using a real-life scenario in the healthcare field.

Original languageBritish English
Pages (from-to)1047-1060
Number of pages14
JournalFuture Generation Computer Systems
StatePublished - Jun 2020


  • Model checking
  • Multi-agent systems
  • Reasoning postulates
  • Temporal logic
  • Trust


Dive into the research topics of 'Specification and automatic verification of trust-based multi-agent systems'. Together they form a unique fingerprint.

Cite this