Group announcement logic

Two currently active strands of research on logics for multi-agent systems are dynamic epistemic logic, focusing on the epistemic consequences of actions, and logics of coalitional ability, focusing on what coalitions of agents can achieve by cooperating strategically. In this paper we bridge these topics by considering the question: “what can a coalition achieve by making public announcements?”. We propose an extension of public announcement logic with constructs of the form 〈G〉ϕ〈G〉ϕ, where G is a group of agents, with the intuitive meaning that G can jointly execute a publicly observable action such that ϕ will be true afterwards. Actions here are taken to be truthful public announcements, but turn out also to include sequences of such joint actions as well as protocols with alternating actions by different agents, in response to the actions of others. We also study in detail the difference between ‘knowing how’ (knowing de re) and ‘knowing that’ (knowing de dicto) in our framework: both can elegantly be expressed in the single-agent case. We present several meta-logical properties of this Group Announcement Logic, including a sound and complete axiomatization, expressivity and the complexity of model checking.