Formal verification of group and propagated trust in multi-agent systems

Nagat Drawel, Jamal Bentahar, Amine Laarej, Gaith Rjoub

Research output: Contribution to journalArticlepeer-review

18 Scopus citations


While modeling trust in multi-agent systems provides a fundamental basis for promoting safe interactions and imitating agents reasoning mechanisms, exploiting model checking techniques to govern the trust relationships between group of agents and other agents is yet to be investigated. In this paper, we present a formal framework that allows individual and group of agents to reason about their trust toward other agents. In particular, we propose a branching time temporal logic BT which includes operators that express concepts such as everyone trust, distributed trust and propagated trust. We develop efficient and scalable reduction algorithms by which model checking BT logic is feasible at design time. We analyze the satisfiability and model checking problems of this logic. Moreover, we present in this manuscript BTT, a new BT Transformation tool, which is developed to automate the verification process. Finally, we demonstrate extensive experimental results, which confirm the theoretical findings and make our approach practical.

Original languageBritish English
Article number19
JournalAutonomous Agents and Multi-Agent Systems
Issue number1
StatePublished - Apr 2022


  • Formal verification
  • Model checking
  • Temporal logic
  • Transformation tool
  • Trust


Dive into the research topics of 'Formal verification of group and propagated trust in multi-agent systems'. Together they form a unique fingerprint.

Cite this