Verifying temporal trust logic using CTL model checking

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 that has not been sufficiently investigated yet. In this paper, we address this challenge by proposing a formal and fully automatic model checking technique for a temporal logic of trust. From the logical perspective, the starting point of our proposal is TCTL, a Computation Tree Logic of preconditional Trust that has been recently proposed. We extend this logic by introducing a new modality for conditional trust and describe the logical relationship between preconditional and conditional trust. From the formal verification perspective, we develop transformation-based algorithms fully implemented in a Java toolkit that automatically interacts with the NuSMV model checker. Our verification approach automatically transforms the problem of model checking TCTL into the problem of model checking CTL. We also develop a model checking algorithm for the conditional trust. We provide proofs of the soundness and completeness of our transformation algorithms. 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 conditional trust formulae.