YR-CONCUR
ATCAL: a model of information manipulation by concurrent announcements
Louwe B. Kuijer, Klara Rawska-Furman
We introduce Alternating-time Temporal Coalition Announcement Logic (ATCAL), a logic of epistemic manipulation that combines the one-shot manipulation of Coalition Announcement Logic (CAL) with the multi-round strategising of Alternating-time Temporal Logic (ATL). We define its syntax and semantics based on the concurrent announcement game over finite epistemic models, and show that the model checking is PSPACE-complete. We also show that the temporal aspect is essential, as for a fixed goal formula the number of announcement rounds a coalition needs can be forced arbitrarily large, and therefore ATCAL strategies cannot in general be compressed into the single round available in CAL.