Transformation-based model checking temporal trust in multi-agent systems

Several formal trust frameworks have been introduced in the area of Multi-Agent Systems (MASs). However, the problem of model checking trust logics is still a challenging research topic. In this paper, we address this challenge by proposing a formal and fully automatic model checking technique for two temporal logics of trust. We start by reviewing TCTL, a Computation Tree Logic of Trust, which has been recently proposed. We also introduce TCTL^C for conditional trust. Then, we introduce sound and complete transformation-based algorithms that automatically transform the problem of model checking TCTL and TCTL^C into the problem of model checking CTL. Moreover, we prove that although TCTL and TCTL^C extend CTL, their model checking algorithms still have the same time complexity for explicit models, which is P-complete with regard to the size of the model and length of the formula, and the same space complexity for concurrent programs, which is PSPACE-complete with regard to the size of the components of these programs. Finally, experiments conducted on a standard industrial case study of auto-insurance claim processing demonstrate the efficiency and scalability of our approach in verifying TCTL and TCTL^C formulae.