Model checking for coalition announcement logic

Abstract

Coalition Announcement Logic (CAL) studies how a group of agents can enforce a certain outcome by making a joint announcement, regardless of any announcements made simultaneously by the opponents. The logic is useful to model imperfect information games with simultaneous moves. We propose a model checking algorithm for CAL and show that the model checking problem for CAL is PSPACE-complete. We also consider a special positive case for which the model checking problem is in P. We compare these results to those for other logics with quantification over information change.