Verification and Strategy Synthesis for Coalition Announcement Logic
Journal article, Peer reviewed
Published version
Åpne
Permanent lenke
https://hdl.handle.net/11250/2989478Utgivelsesdato
2021Metadata
Vis full innførselSamlinger
Originalversjon
Journal of Logic, Language and Information. 2021, 30 (4), 671-700. 10.1007/s10849-021-09339-6Sammendrag
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.