Verification and Strategy Synthesis for Coalition Announcement Logic
Journal article, Peer reviewed
Published version
View/ Open
Date
2021Metadata
Show full item recordCollections
Original version
Journal of Logic, Language and Information. 2021, 30 (4), 671-700. 10.1007/s10849-021-09339-6Abstract
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.