Verification and Strategy Synthesis for Coalition Announcement Logic
Natasha Alechina, Hans van Ditmarsch, Rustam Galimullin, Tuo Wang · Journal of Logic Language and Information · 2021
Abstract Coalition announcement logic (CAL) is one of the family of the logics of quantified announcements. It allows us to reason about what a coalition of agents can achieve by making announcements in the setting where the anti-coalition may have an announcement of their own to preclude the former from reaching its epistemic goals. In this paper, we describe a PSPACE-complete model checking algorithm for CAL that produces winning strategies for coalitions. The algorithm is implemented in a proof-of-concept model checker.