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

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.