Verification and Strategy Synthesis for Coalition Announcement Logic

N Alechina, H van Ditmarsch, R Galimullin*, T Wang

*Corresponding author for this work

Research output: Contribution to journalArticleAcademicpeer-review


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.
Original languageEnglish
Pages (from-to)671-700
Number of pages30
JournalJournal of Logic, Language and Information
Issue number4
Publication statusPublished - Dec 2021


  • Coalition announcement logic
  • Dynamic epistemic logic
  • Group announcement logic
  • Model checking


Dive into the research topics of 'Verification and Strategy Synthesis for Coalition Announcement Logic'. Together they form a unique fingerprint.

Cite this