Verification and Strategy Synthesis for Coalition Announcement Logic
Publication date
2021-12
Authors
Alechina, Natasha
van Ditmarsch, H.
Galimullin, Rustam
Wang, Tuo
Editors
Advisors
Supervisors
Document Type
Article
Metadata
Show full item recordCollections
License
cc_by
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.
Keywords
Citation
Alechina, N, van Ditmarsch, H, Galimullin, Rustam & Wang, T 2021, 'Verification and Strategy Synthesis for Coalition Announcement Logic', Journal of Logic, Language and Information, vol. 30, no. 4, pp. 671-700. https://doi.org/10.1007/s10849-021-09339-6