Model Checking Multi-agent Systems with APTL
Haiyang Wang, Zhenhua Duan and Cong Tian
A symbolic model checking approach is presented in this paper to verify properties of Multi-agent Systems (MASs). Our approach aims to check whether a property which expressed by an Alternating Projection Temporal Logic (APTL) formula φ is valid on a MAS. First, the MAS is specified by an Interpreted System IS and then symbolically represented; meanwhile, ¬φ is transformed into normal form. Then, the set Sat(¬φ) is computed on the MAS, which contains all the states starting from which ¬φ holds on at least one computation. Finally, the validity of φ on the MAS is evaluated by checking whether the intersection of the set of initial states of IS and Sat(¬φ) is empty. The supporting model checker MCMAS APTL is developed and, as a case study, properties of a real-world MAS are verified.
Keywords: Multi-agent system, alternating projection temporal logic, interpreted system, symbolic model checking, verification.