# The Expressivity of Quantified Group Announcements

Natasha Alechina, Hans van Ditmarsch, Tim French, Rustam Galimullin

► To cite this version:

Natasha Alechina, Hans van Ditmarsch, Tim French, Rustam Galimullin. The Expressivity of Quantified Group Announcements. Journal of Logic and Computation, 2022, 33 (6), pp.1122-1151. 10.1093/logcom/exac082. hal-04238178

HAL Id: hal-04238178

https://hal.science/hal-04238178v1

Submitted on 12 Oct 2023

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
# The expressivity of quantified group announcements

NATASHA ALECHINA, Department of Information and Computing Sciences,
Utrecht University, Utrecht, 3584 CC, the Netherlands.

E-mail: n.a.alechina@uu.nl

HANS VAN DITMARSCH, Department of Computer Science, Open University,
Heerlen, 6401 DL, the Netherlands.

E-mail: hans.vanditmarsch@ou.nl

TIM FRENCH, Department of Computer Science and Software Engineering, The
University of Western Australia, Perth, 6009, Australia.

E-mail: tim.french@uwa.edu.au

RUSTAM GALIMULLIN, Department of Information Science and Media Studies,
University of Bergen, Bergen, 5020, Norway.

E-mail: rustam.galimullin@uib.no

## Abstract

Group announcement logic (GAL) and coalition announcement logic (CAL) allow us to reason about whether it is possible for groups and coalitions of agents to achieve their desired epistemic goals through truthful public communication. The difference between groups and coalitions in such a context is that the latter make their announcements in the presence of possible adversarial counter-announcements. As epistemic goals may involve some agents remaining ignorant, counter-announcements may preclude coalitions from reaching their goals. We study the relative expressivity of GAL and CAL and provide some results involving their more well-known sibling APAL. We also discuss how the presence of memory alters the relationship between groups and coalition.

## 1 Introduction

### Quantified dynamic epistemic logics

Multi-agent epistemic logic (EL) is a modal propositional logic with formulas $\Box_a\varphi$ standing for 'agent a knows proposition $\varphi$' [27]. The logic is typically interpreted on the so-called Kripke models that are relational structures with for each agent an equivalence relation on the domain of abstract states. Public announcement logic (PAL) is an extension of EL with dynamic epistemic operators that allow us to reason about the effects of agents simultaneously and publicly acquiring some truthful information [20, 33]. It contains formulas $[\psi]\varphi$ standing for 'after truthful public announcement of $\psi$, $\varphi$ (is true)'. The effect of the public announcement of $\psi$ is a restriction of the underlying model on which the formula is interpreted to the states where $\psi$ is true, and in the resulting model restriction, the formula $\varphi$ is then interpreted. ELs such as PAL where dynamic modalities are interpreted by way of model transformations are often known as *dynamic epistemic logics* (DELs). *Arbitrary public*

Vol. 33, No. 6, © The Author(s) 2022. Published by Oxford University Press.

This is an Open Access article distributed under the terms of the Creative Commons Attribution License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted reuse, distribution, and reproduction in any medium, provided the original work is properly cited.

Advance Access Publication on 24 November 2022 https://doi.org/10.1093/logcom/exac082
announcement logic (APAL) is a variant of PAL with quantification over public announcements [6]. It extends the language of PAL with formulas [!]φ that express that ‘after any public announcement, φ holds’ (i.e. on condition that this public announcement is true in the current state). Many versions of APAL have been proposed. The DELs with quantified announcements that we consider in this contribution are called *group announcement logic (GAL)* [2] and *coalition announcement logic (CAL)* [3]. In the former, [*G*]φ means that ‘after any (simultaneous) announcement by the agents in group *G*, φ holds’, whereas in the latter, [*G*]φ is read as ‘given any (simultaneous) announcement by the agents in group *G*, there is a simultaneous announcement by the remaining agents, such that φ holds afterwards’. The CAL quantifier thus hides an alternation of a universal and an existential quantifier. Both in GAL and CAL, such simultaneous announcements are conjunctions of formulas known by the agents, i.e. they have shape □<sub>*a*</sub>φ<sub>*a*</sub> ∧ ... ∧ □<sub>*z*</sub>φ<sub>*z*</sub> where {*a*, ..., *z*} is a subset of the set of all agents. In other words, agents only announce what they know.

The GAL and CAL modalities have been applied to specify notions and problems in imperfect information games and in security protocols (what can the principals guarantee after any protocol?) [2, 3], in epistemic game theory [32] and in general in reasoning about games and strategies (coalition announcements formalize *playability*) [11]. There are relations between GAL and CAL, and logics of strategic capability such as ATL [5] and ATEL [28], and between GAL and CAL, and logics of agency such as STIT and Next-STIT [29]. The relation is that the dual ([G]φ of the CAL quantifier can be interpreted as ‘the agents in *G* are capable of ensuring that φ’ and that the dual ⟨G⟩φ of the GAL quantifier can be interpreted as ‘after the agents in *G* act, φ is true’. To get a GAL-like (or CAL-like) effect in such logics, we need to combine agency modalities with temporal modalities in their logical languages: such logics are typically interpreted on larger structures where the model transformations of DELs appear within such larger models as transitions that interpret temporal modalities such as ‘next’-time operators.

Other DELs do not model public events such as public announcements, but private announcements and partial observation in general, where best known is *action model logic* [8]; for a recent survey, see [21]. Quantification over such modalities is also an actively pursued topic [14, 15, 16].

## History-based semantics for DELs

Typically, in DELs, the formulas are interpreted in the updated (transformed) model where, so to speak, it is no longer known how this came about. The agents are memoryless. History-based semantics for DEL, for agents with memory, have been proposed in such works as [12, 21, 34], as well as in [7, 9, 10], with an interesting difference in approaches. In the former, a sequence of events or actions (such as announcements) is stored in memory that is, in principle, available for agents and that allows to refer to past actions in the logical language (in typically some sort of converse modality). This is the ‘yesterday’ operator in [34–36]. In fact, in [12, 21], such histories of actions are then not used for agents to reason about the past, but in order to embed DELs into temporal ELs; however, in principle, such information is there. In contrast, [7, 9] contain operators that allow to refer to an initial information state from the current information state but abstracting from the sequence of announcements that may have led to the current state. So one cannot distinguish between different developments (different sequences with different intermediate information states) resulting in the same final state. We focus on *APAL with memory* (APALM) [9, 10] as its language contains a quantifier, like APAL. In APALM, instead of models with an abstract domain of states, we have models with an initial and a current domain of states. This has the effect that the initial information state remains available for interpretation of formulas in the current state. The logical language of APALM extends that of APAL with formulas φ⁰, for ‘φ was initially true’ (as well
<figure><img src="image_2.png" /><figcaption>FIGURE 1. An APAL vs. EL example.</figcaption></figure>

as other features, such as a universal modality). Therefore, in this logic, $\Box_a \varphi^0$ means that agent $a$ knows that $\varphi$ was true (in the past). The semantics are therefore history-based (although in the abstract sense that only considers the initial information state in the past, and not all intermediate stages leading to the current state). They hence allow to reveal more structure of updated models, also in a precise technical sense as follows. In PAL, it may happen that initially non-bisimilar states have become bisimilar in the updated model (for bisimulation, see [11]). But in APALM, we can still distinguish such states namely with the above $\varphi^0$ formulas (so that another notion of bisimilarity is required [9]). In our contribution, we also present versions of group announcement logic GAL and coalition announcement logic CAL with *Memory*, which we therefore call GALM and CALM (the former already appears in [10]). As we will show, the presence of memory affects their expressivity.

## Expressivity of DELs

A topic of interest for announcement logics is their relative *expressivity*. DELs such as announcement logics have various and surprising expressivity results, due to group epistemic phenomena and to the interaction of dynamic and epistemic features, and those results are often non-trivial to establish [1, 2, 6, 20, 24, 30]. It is known that EL is as expressive as PAL [33] and that APAL, GAL and CAL are (strictly) more expressive than PAL [2, 6]. The relative expressivity of APAL, GAL and CAL has been an open question for quite a while [2, 15]. We partially answer this question: we show that CAL is *not* at least as expressive as GAL. This is one direction needed to determine the relative expressivity of GAL and CAL. As a consequence, also APAL is not at least as expressive as GAL. Whether GAL is not at least as expressive as CAL remains unanswered. Additionally, we show that, in contrast, GALM is at least as expressive as CALM.

To introduce these expressivity results, we present some examples. Each formula in a logical language determines a set of pointed models on which that formula is true (we assume equivalence relations throughout). This is the property associated with that formula, and different languages may thus describe a different set of properties: they then have a different expressivity. The larger expressivity of APAL with respect to PAL (and EL) is because the APAL quantifier implicitly quantifies over all propositional variables in the language as well as over formulas of arbitrary modal depth (the modal depth is the maximal stack of epistemic modalities $\Box_a$ in a formula). One proof that APAL is more expressive than PAL is based on modal depth. Consider the three pointed models in Figure 1.

On the left a model wherein two agents $a, b$ are both ignorant about $p$. The actual state is framed. In the middle, a bisimilar infinite representation of the model. Now consider the formula $\langle ! \rangle (\Box_a p \wedge \neg \Box_b \Box_a p)$, for ‘there is announcement (model restriction) after which $a$ knows $p$ but $b$ does not know that’. No model restriction of the left model (or, therefore, of the middle one) can achieve that. But on the assumption that there is an epistemic formula $\psi$ equivalent to $\langle ! \rangle (\Box_a p \wedge \neg \Box_b \Box_a p)$ (so expressing the same property), it has a modal depth. Now consider a version of the middle model where beyond the modal depth from the actual framed state the ‘chain’ is cut off. The ‘endpoints’ satisfy the unique property that $a$ or $b$ there knows the truth about $p$. Therefore, in such a model, there is after all an announcement restricting it to the model on the right wherein $\Box_a p \wedge \neg \Box_b \Box_a p$
<figure><img src="image_3.png" /><figcaption>FIGURE 2. Model $M_t$ and various restrictions thereof. Announced formulas are superindexes and points of models are subindexes.</figcaption></figure>

is true (see [6]). On the other hand, this large finite model and the infinite model (and thus also the two-state model bisimilar to it) satisfy the same formulas of modal depth up to that of the assumed $\psi$. Therefore, this equivalent $\psi$ cannot exist. The expressivity arguments involving GAL and CAL are far more involved, but based on similar principles.

Now for GALM and CALM. A familiar phenomenon in PAL is that non-bisimilar states become bisimilar after an announcement, such as states $t$ and $u$ in the models $M$ and $M^P$ in Figure 2. Initially, $b$ does not know whether $p$ in $t$ ($\neg \Box_b p \wedge \neg \Box_b \neg p$) but knows that $p$ in $u$ ($\Box_b p$), whereas afterwards, $p$ is common knowledge in $t$ and in $u$.

Of course states do not have to become bisimilar. In the restriction $M^{\neg \Box_b p}$, the states $s$ and $t$ still make different formulas true. But $M^{p \wedge \neg \Box_b p}$, on the right, is bisimilar to $M^p$. These matters also play a part in logics with announcements made by agents such as GAL and CAL. The announcement $p$ has the same effect as $\Box_a p$ (an announcement by $a$), and $p \wedge \neg \Box_b p$ has the same effect as $\Box_a p \wedge \neg \Box_b \neg \Box_b p$ (a joint announcement by $a$ and $b$). The difference between GAL and CAL is that, given a group of agents $G$, in the latter, the remaining agents make their announcement simultaneously with those in $G$, whereas in the former they may make it afterwards. In much more complex models than the above, later then may be too late because the remaining agents would have needed the distinguishing power between states that were initially different but now no longer, such as $t$ and $u$ in $M$ respectively $M^P$. If those remaining agents can remember what was initially true, they can still make the distinction: in state $t$ of $M^P$, it holds that ($\neg \Box_b p \wedge \neg \Box_b \neg p$)$^0$, whereas in state $u$ it holds that ($\Box_b p$)$^0$. Consequently, in GALM and CALM, we expect groups of agents to have additional expressive ‘power’. And this is indeed the case.

## *Outline of the contribution*

In what follows, we first provide formal definitions of the concepts discussed here in Section 2. Then, as a warm-up, in Section 3, we show that CAL is not at least as expressive as APAL. In Section 4, we discuss why an intuitive translation of CAL formulas into GAL formulas does not work. To set the scene for the main result, we first introduce the notion of formula games for GAL and CAL in Section 5, and then, in Section 6, provide two classes of model distinguishable by a GAL formula. Finally, we prove that CAL is not at least as expressive as GAL in Section 7 and have that APAL is not at least as expressive as GAL as a corollary. On top of that, in Section 8, we show that GALM is at least as expressive as CALM. We conclude and discuss further research in Section 9.

# 2 Technical background

## 2.1 Languages and semantics

Let us fix a finite set of agents $A$ and a countable set of propositional variables $P$.
DEFINITION 1

The languages of epistemic logic $\mathcal{EL}$, public announcement logic $\mathcal{PAL}$, arbitrary public announcement logic $\mathcal{APAL}$, group announcement logic $\mathcal{GAL}$ and coalition announcement logic $\mathcal{CAL}$ are defined by the following grammars:

$$ 
\begin{array}{lclcl}
\mathcal{EL} & \exists & \varphi & ::= & p \mid \neg\varphi \mid (\varphi \land \varphi) \mid \Box_a\varphi \\
\mathcal{PAL} & \exists & \varphi & ::= & p \mid \neg\varphi \mid (\varphi \land \varphi) \mid \Box_a\varphi \mid [\varphi]\varphi \\
\mathcal{APAL} & \exists & \varphi & ::= & p \mid \neg\varphi \mid (\varphi \land \varphi) \mid \Box_a\varphi \mid [\varphi]\varphi \mid [!]\varphi \\
\mathcal{GAL} & \exists & \varphi & ::= & p \mid \neg\varphi \mid (\varphi \land \varphi) \mid \Box_a\varphi \mid [\varphi]\varphi \mid [G]\varphi \\
\mathcal{CAL} & \exists & \varphi & ::= & p \mid \neg\varphi \mid (\varphi \land \varphi) \mid \Box_a\varphi \mid [\varphi]\varphi \mid [(G)]\varphi,
\end{array}
$$

where $p \in P$, $a \in A$ and $G \subseteq A$. Duals are defined as $\diamond_a\varphi := \neg\Box_a\neg\varphi$, $\langle\psi\rangle\varphi := \neg[\psi]\neg\varphi$, $\langle!\rangle\varphi := \neg[!]\neg\varphi$, $\langle G\rangle\varphi := \neg[G]\neg\varphi$, $[G]\varphi := \neg[G]\neg\varphi$. Given some $G$, we will denote $A \setminus G$ as $\overline{G}$. We will also use abbreviations $\top := p \lor \neg p$ and $\bot := p \land \neg p$.

Formula $\Box_a\varphi$ is read as 'agent $a$ knows $\varphi$'; $[\psi]\varphi$ means that 'after the public announcement of $\psi$, $\varphi$ will hold'; $[!]\varphi$ is read as 'after any public announcement, $\varphi$ is true'; $[G]\varphi$ is read as 'after any joint public announcement by agents from group $G$, $\varphi$ holds'; and $[(G)]\varphi$ is read as 'for any announcement by coalition $G$, there is a simultaneous announcement by the anti-coalition such that $\varphi$ holds after the joint announcement'.

DEFINITION 2

A model $M$ is a tuple $(S, \sim, V)$, where $S$ is a non-empty set of states, $\sim: A \to 2^{S \times S}$ is an equivalence relation for each agent, and $V: P \to 2^S$ is the valuation function. We will denote model $M$ with a distinguished state $s$ as $M_s$ and sometimes call it a *pointed model*. Whenever necessary, we refer to the elements of the tuple as $S^M$, $\sim^M$ and $V^M$. We will also write $M_s^X = (S^X, \sim^X, V^X)$, where $X \subseteq S$, $s \in X$, $S^X = X$, $\sim_a^X = \sim_a \cap (X \times X)$ for all $a \in A$, and $V^X(p) = V(p) \cap X$.

It is assumed that for group and coalition announcements, agents know the formulas they announce. In the following, we write $\mathcal{EL}^G = \{ \bigwedge_{i \in G} \Box_i \psi_i \mid \text{for all } i \in G, \psi_i \in \mathcal{EL} \}$ (with typical elements $\psi_G$) to denote the set of all possible announcements by agents from group $G$.

DEFINITION 3

Let $M_s = (S, \sim, V)$ be a model, $p \in P$, $G \subseteq A$.

$$ 
\begin{array}{lclcl}
M_s \models p & \text{iff} & s \in V(p) & & \\
M_s \models \neg\varphi & \text{iff} & M_s \not\models \varphi & & \\
M_s \models \varphi \land \psi & \text{iff} & M_s \models \varphi \text{ and } M_s \models \psi & & \\
M_s \models \Box_a\varphi & \text{iff} & M_t \models \varphi & \text{for all } t \in S & \text{such that } s \sim_a t \\
M_s \models [\psi]\varphi & \text{iff} & M_s \models \psi & \text{implies } M_s^\psi \models \varphi & \\
M_s \models [!]\varphi & \text{iff} & M_s \models [\psi]\varphi & \text{for all } \psi \in \mathcal{EL} & \\
M_s \models [G]\varphi & \text{iff} & M_s \models [\psi_G]\varphi & \text{for all } \psi_G \in \mathcal{EL}^G & \\
M_s \models [(G)]\varphi & \text{iff} & M_s \models \psi_G \rightarrow \langle\psi_G \land \chi_G^\rangle\varphi & \text{for all } \psi_G \in \mathcal{EL}^G & \text{and some } \chi_G^\in \mathcal{EL}^{\overline{G}},
\end{array}
$$

where $M_s^\psi = (S^\psi, \sim^\psi, V^\psi)$ with $S^\psi = \{s \in S \mid M_s \models \psi\}$, $\sim_a^\psi$ is the restriction of $\sim_a$ to $S^\psi$ for all $a \in A$, and $V^\psi(p) = V(p) \cap S^\psi$ for all $p \in P$. We call a formula $\varphi$ valid, or a validity, if for all $M_s$ it holds that $M_s \models \varphi$.
## 2.2 Bisimulation and expressivity

### DEFINITION 4

Let $M = (S^M, \sim^M, V^M)$ and $N = (S^N, \sim^N, V^N)$ be models. We say that $M$ and $N$ are *bisimilar* if there is a non-empty relation $B \subseteq S^M \times S^N$, called a *bisimulation* and denoted $M \iff N$, such that for all $B(s, t)$, the following conditions are satisfied.

**Atoms** for all $p \in P$: $s \in V^M(p)$ if and only if $t \in V^N(p)$,

**Forth** for all $a \in A$ and $u \in S^M$ such that $s \sim_a^M u$, there is a $v \in S^N$ such that $t \sim_a^N v$ and $B(u, v)$,

**Back** for all $a \in A$ and $v \in S^N$ such that $t \sim_a^N v$, there is a $u \in S^M$ such that $s \sim_a^M u$ and $B(u, v)$.

We say that $M_s$ and $N_t$ are bisimilar and denote this by $M_s \rightleftarrows N_t$ if there is a bisimulation linking states $s$ and $t$.

As in the case of standard modal logic [26], bisimulation between models implies that the models satisfy the same formulas of APAL, GAL and CAL.

### THEOREM 1

Given $M_s$ and $N_t$, if $M_s \rightleftarrows N_t$, then for all $\varphi \in \mathcal{A}\mathcal{P}\mathcal{A}\mathcal{L} \cup \mathcal{G}\mathcal{A}\mathcal{L} \cup \mathcal{C}\mathcal{A}\mathcal{L}$, we have that $M_s \models \varphi$ if and only if $N_t \models \varphi$.

**PROOF.** The proof is by induction on $\varphi$. Propositional, boolean and epistemic cases are as usual. The case of public announcements follows from the corresponding result for action models [20, Theorem 6.21]. Finally, the cases of arbitrary, group and coalition announcements follow from the fact that public announcements preserve bisimilarity and the induction hypothesis. $\square$

### DEFINITION 5

Let $n \in \mathbb{N}$ and $M = (S^M, \sim^M, V^M)$ and $N = (S^N, \sim^N, V^N)$ be models. We say that $M_s$ and $N_t$ are *n-bisimilar* if there is a non-empty relation $B \subseteq S^M \times S^N$, called an *n-bisimulation* and denoted $M_s \rightleftarrows^n N_t$, which is defined inductively as follows. Relation $B$ is a 0-bisimulation between $M_s$ and $N_t$ if **Atoms** holds for $(s, t)$. Relation $B$ is $n+1$-bisimulation between $M_s$ and $N_t$ if the following conditions are satisfied.

**Atoms** for all $p \in P$: $s \in V^M(p)$ if and only if $t \in V^N(p)$,

**Forth** for all $a \in A$ and $u \in S^M$ such that $s \sim_a^M u$, there is a $v \in S^N$ such that $t \sim_a^N v$ and $M_u \rightleftarrows^n N_v$,

**Back** for all $a \in A$ and $v \in S^N$ such that $t \sim_a^N v$, there is a $u \in S^M$ such that $s \sim_a^M u$ and $M_u \rightleftarrows^n N_v$.

It is a standard result that $M_s \rightleftarrows^n N_t$ implies $M_s \models \varphi$ if and only if $N_t \models \varphi$ for $\varphi \in \mathcal{EL}$ with modal depth less or equal $n$ [26]. This, however, does not hold if $\varphi$ contains a quantified announcement, since these operators quantify over formulas of arbitrary modal depth.

### DEFINITION 6

Let $\mathcal{L}$ and $\mathcal{L}'$ be two languages and $\varphi \in \mathcal{L}$ and $\psi \in \mathcal{L}'$. Formulas $\varphi$ and $\psi$ are called *equivalent*, if for all $M_s$ it holds that $M_s \models \varphi$ iff $M_s \models \psi$.

### DEFINITION 7

Let $\mathcal{L}$ and $\mathcal{L}'$ be two languages. We say that $\mathcal{L}$ is *at least as expressive as* $\mathcal{L}'$, denoted $\mathcal{L}' \leq \mathcal{L}$, if for every $\varphi \in \mathcal{L}'$, there is an equivalent $\psi \in \mathcal{L}$. We write $\mathcal{L}' < \mathcal{L}$ if $\mathcal{L}' \leq \mathcal{L}$ and $\mathcal{L} \not\leq \mathcal{L}'$, and we say that
<figure><img src="image_4.png" /><figcaption>FIGURE 3. From left to right: models $M_s, M_s^{1a}$ (bottom), $M_u^{2a}$ (top), $M_s^{1b}, M_t^{2b}$ and $M_x^{a,b}$, with $x \in \{s, t, u, v\}$ (four single-state models).</figcaption></figure>

L is strictly more expressive than L'. We call L and L' incomparable if L' ≁ L and L ≁ L'. Finally, if L' ⊏ L and L ⊏ L', we call L and L' equally expressive and write L = L'.

The standard result from the literature [33] is that $\mathcal{EL} = \mathcal{PAL}$. It is also known that $\mathcal{PAL} < \mathcal{APAL}$ [6], $\mathcal{PAL} < \mathcal{GAL}$ [2] and $\mathcal{PAL} < \mathcal{CAL}$ [3].

## 3 Coalitions and arbitrary announcements

It was proved in [2] that $\mathcal{APAL} \not\subset \mathcal{GAL}$. The intuition behind the proof is that a group of agents $G$ can only force $G$-definable restrictions of a given model, whereas APAL modalities may force any restriction of the model up to bisimulation. The same reasoning can be applied to both groups and coalitions. Therefore, we use the proof from [2] and modify it to show that $\mathcal{APAL} \not\subset \mathcal{CAL}$.

**THEOREM 2**
$\mathcal{APAL} \not\subset \mathcal{CAL}$.

*PROOF.* Consider the APAL formula $\langle ! \rangle (\Box_a p \wedge \neg \Box_b \Box_a p)$. Let us assume that there is an equivalent CAL formula $\psi$. Without loss of generality, we also assume that propositional atom $q$ does not occur in $\psi$. Now, consider the models in Figure 3.

These models correspond to various restrictions of $M$ that agents can enforce. We need to show that the APAL formula distinguishes $M$ and $M^{1a}$, and no CAL formula can distinguish them. Formally, it should be the case that $M_s \models \psi$ and $M_s^{1a} \models \psi$, while $M_s \models \langle ! \rangle (\Box_a p \wedge \neg \Box_b \Box_a p)$ and $M_s^{1a} \not\models \langle ! \rangle (\Box_a p \wedge \neg \Box_b \Box_a p)$.

That $M_s \models \langle ! \rangle (\Box_a p \wedge \neg \Box_b \Box_a p)$ and $M_s^{1a} \not\models \langle ! \rangle (\Box_a p \wedge \neg \Box_b \Box_a p)$ is easy to check. In order to make $\Box_a p \wedge \neg \Box_b \Box_a p$ true, it is required to remove state $t$ and retain states $u$ and $v$. In model $M_s$ announcement of $p \lor q$ would do the trick. And in model $M_s^{1a}$, none of the possible updates satisfies the formula.

To prove that $M_s \models \psi$ if and only if $M_s^{1a} \models \psi$, we need to show that for all subformulas $\varphi$ of $\psi$, all states reachable from $s$, and all updates of $M$ by agents' announcements, the equivalence holds. We consider only cases of coalition announcements and prove only the first row of the equivalences (proofs for other three rows are similar).

Let $\varphi \in \mathcal{CAL}$ and $q$ does not appear in $\varphi$.
Induction hypothesis:

$$M_s \models \varphi \text{ iff } M_s^{1a} \models \varphi \text{ iff } M_u \models \varphi \text{ iff } M_u^{2a} \models \varphi$$

$$M_s^{a,b} \models \varphi \text{ iff } M_s^{1b} \models \varphi \text{ iff } M_u^{1b} \models \varphi \text{ iff } M_u^{a,b} \models \varphi$$

$$M_t \models \varphi \text{ iff } M_t^{1a} \models \varphi \text{ iff } M_v \models \varphi \text{ iff } M_v^{2a} \models \varphi$$

$$M_t^{a,b} \models \varphi \text{ iff } M_t^{2b} \models \varphi \text{ iff } M_v^{2b} \models \varphi \text{ iff } M_v^{a,b} \models \varphi$$

Case [[(Ø)]]φ. Let $M_s \models [[(Ø)]]φ$. This is equivalent to the fact that there is a joint {a, b}-announcement $\chi_a \wedge \chi_b$ such that $M_s^{\chi_a \wedge \chi_b} \models \varphi$. All possible results of updating $M_s$ with $\chi_a \wedge \chi_b$ are presented in Figure 3 (models $M_s$, $M_s^{1a}$, $M_s^{1b}$ and $M_s^{a,b}$). Therefore, at least one of the restrictions should satisfy $\varphi$, i.e. ($M_s \models \varphi$ or $M_s^{1a} \models \varphi$ or $M_s^{1b} \models \varphi$ or $M_s^{a,b} \models \varphi$) (*).

According to the induction hypothesis, (*) is equivalent to $M_s^{1a} \models \varphi$ or $M_s^{a,b} \models \varphi$. The latter means that there is an {a, b}-announcement in model $M_s^{1a}$ such that $\varphi$ holds in the resulting model, which is equivalent to $M_s^{1a} \models [[(Ø)]]\varphi$.

Statement (*) is also equivalent, by the induction hypothesis, to ($M_u \models \varphi$ or $M_u^{2a} \models \varphi$ or $M_u^{1b} \models \varphi$ or $M_u^{a,b} \models \varphi$). These are all possible restrictions of $M_u$ by {a, b}-announcements, which is equivalent to $M_u \models [[(Ø)]]\varphi$ by the semantics.

Finally, (*) is equivalent to ($M_u^{2a} \models \varphi$ or $M_u^{a,b} \models \varphi$), which holds if and only if there is an {a, b}-announcement in $M_u^{2a}$ such that $\varphi$ is true in the resulting updated model. This is equivalent to $M_u^{2a} \models [[(Ø)]]\varphi$ by the semantics.

Case [[(a, b)]]φ. The same as above with the replacement of ‘or’ with ‘and’ in (*).

Case [[(a)]]φ. Let $M_s \models [[(a)]]φ$. This is equivalent to the fact that for every a-announcement $\chi_a$ there is a b-announcement $\chi_b$ such that $M_s^{\chi_a \wedge \chi_b} \models \varphi$. We consider all these restrictions: ($M_s \models \varphi$ or $M_s^{1b} \models \varphi$) and ($M_s^{1a} \models \varphi$ or $M_s^{a,b} \models \varphi$)(†).

By the induction hypothesis, (†) is equivalent to ($M_s^{1a} \models \varphi$ or $M_s^{a,b} \models \varphi$), which means that for every a-announcement in model $M_s^{1a}$, there is a b-announcement such that $\varphi$ holds in the resulting model. The latter is equivalent to $M_s^{1a} \models [[(a)]]\varphi$ by the semantics.

According to the induction hypothesis, (†) is equivalent to ($M_u \models \varphi$ or $M_u^{1b} \models \varphi$) and ($M_u^{2a} \models \varphi$ or $M_u^{a,b} \models \varphi$). These are all possible combinations of a's announcements and b's responses in $M_u$. Hence, it is equivalent to $M_u \models [[(a)]]\varphi$ by the semantics.

Finally, (†) is equivalent to ($M_u^{2a} \models \varphi$ or $M_u^{a,b} \models \varphi$), and the latter holds if and only if for all a-announcements in $M_u^{2a}$ (agent a cannot change the model in a non-trivial way), there is a b-announcement such that $\varphi$ is true in the resulting updated model, which is equivalent to $M_u^{2a} \models [[(a)]]\varphi$ by the semantics.

Case [[(b)]]φ. Similar reasoning as above. □

# 4 Agents who forget how to play

While reasoning about the coalitional ability and announcements, it is quite natural to wonder whether coalition announcements could be equivalently defined by formulas of GAL. In particular, the semantics of $[G]\varphi$ suggests that we can consider a coalition's announcement and the anti-coalition's response as separate consecutive group announcements. In this section, we show that the most intuitive way of defining coalition announcement in terms of group announcements, $[G]\varphi \leftrightarrow \langle G \rangle [\bar{G}]\varphi$, is not valid.
<figure><img src="image_5.png" /><figcaption>FIGURE 4. Model $M_s^1$ and various restrictions thereof.</figcaption></figure>

This result is a consequence of how public announcements work. Indeed, in the updated model, all the states not satisfying the announced formula are removed, and agents forget that they considered these states possible. Such lack of memory may lead to the situation when agents lose their power to force certain submodels. We utilize this feature in the following proof, where after an announcement by $G$, some states, which $\bar{G}$ could distinguish in the original model, become bisimilar.

**PROPOSITION 1**
$\langle G \rangle[\bar{G}]\varphi \to \langle G \rangle\varphi$ is not valid.

**PROOF.** We present a counterexample (Figure 4) to the contraposition $\langle G \rangle\varphi \to [G]\langle \bar{G} \rangle\varphi$ (strictly speaking, the contraposition has $\neg\varphi$, but we refer to the form of the axiom).

Let $G = \{a\}$ and $\bar{G} = \{b, c\}$. Also, let $\varphi := \Diamond_a \Box_b \neg p \wedge \Diamond_a (\Diamond_b p \wedge \Diamond_b \neg p)$. This formula is a distinguishing formula of state $s$ of model $M^2$, i.e. $\varphi$ is true only in $M_s^2$ and nowhere else in this proof.

First, we show that $M_s^1 \models \langle [a] \rangle \varphi$. By the semantics of CAL, this means that for every $\psi_{[a]}$, there are $\chi_{[b]}$ and $\chi_{[c]}$ such that $M_s^1 \models \psi_a \to (\psi_{[a]} \wedge \chi_{[b]} \wedge \chi_{[c]})\varphi$. Observe that agent $a$ can update $M_s^1$ in two non-equivalent ways: either leaving the whole model as it is or restricting it to $\{u', t', s, t, u\}$. On the other hand, due to the fact that intersection of unions of relations of $b$ and $c$ is an identity relation, agents $\{b, c\}$ can force all possible submodels of $M_s^1$. For either of $a$'s announcements, agents $\{b, c\}$ can make an announcement such that the model is reduced to $\{t', s, t, u\}$. Particularly, $b$ announces a formula true in $\{u', t', s, t, u\}$, and $c$ announces a formula true in $\{t', s, t, u, v\}$. Such a simultaneous joint announcement results in model $M_s^2$ and $M_s^2 \models \varphi$.

Now, let us show that $M_s^1 \not\models [a]\langle\{b, c\}\rangle\varphi$, which is equivalent, by the semantics, to $M_s^1 \models \langle a \rangle[\{b, c\}]\neg\varphi$. Let $a$ announce $\psi_{[a]} := \Box_a(\neg p \to \Diamond_b p)$ that is true in $\{u', t', s, t, u\}$. The resulting model $M_s^{\psi_a}$ and a smaller bisimilar $M_s^3$ are presented in Figure 4.

In model $M_s^3$ agents $\{b, c\}$ can force the following updated models: $\{s, t, u\}$, $\{s, t\}$ and $\{s\}$. Results of corresponding updates are $M_s^3$ itself and $M_s^4$ and $M_s^5$, respectively. It is easy to check that none of them satisfy $\varphi$. Hence, $M_s^1 \not\models [a]\langle\{b, c\}\rangle\varphi$. $\square$
We have shown that an obvious way of defining CAL operators in GAL does not work. However, this does not tell us anything about the relative expressivity of the two logics. We approach this general problem in the following sections.

# 5 Formula games

The standard approach to comparing expressivity of modal languages is by using formula games [20, Chapter 8]. In this section, we present formula games for CAL and GAL. In order to deal with coalition announcement modalities, we use relativized group announcements<fnref n="1" /> that allow us to consider an announcement by a coalition and a counter-announcement by an anti-coalition as separate moves in the game.

**DEFINITION 8 (NNF).**

Negation normal form (NNF) is defined by the following BNF.

$$ \varphi ::= \begin{array}{l} \top | \varphi \wedge \varphi | \Box_a \varphi | [G]\varphi | [G, \varphi]\varphi | [[G]]\varphi \\ \bottomrule | \bot | p | \neg p | \varphi \vee \varphi | \Diamond_a \varphi | [\varphi]\varphi | \langle G \rangle \varphi | \langle G, \varphi \rangle \varphi | [G]\varphi \end{array} $$

If for some formula $\varphi$ in NNF, the outermost operator is from the top line, then we say that $\varphi$ is in universal negation normal form (UNNF), and if the outermost operator is from the line below, then $\varphi$ is in existential negation normal form (ENNF). We denote the corresponding languages as $U\mathcal{N}\mathcal{N}\mathcal{F}$ and $E\mathcal{N}\mathcal{N}\mathcal{F}$. We would also like to point out the absence of clause $\langle\varphi\rangle\varphi$ in the BNF. As it will become clear later, in Proposition 2, we can do without it.

The intended meaning of a relativized group announcement $\langle G, \psi \rangle \varphi$ is that ‘given some $\psi$, there is an announcement $\chi_G$ by the agents from $G$, such that after the simultaneous announcement of $\psi$ and $\chi_G$, $\varphi$ is true’. In other words, relativized group announcement are like normal group announcements with an additional given formula being announced at the same time with the agents’ announcement. In the context of coalition announcements $[[G]]\varphi$, relativized group announcement $\langle \bar{G}, \psi_G \rangle \varphi$ serves as an intermediate step in a game and as a means to ‘memorize’ announcement $\psi_G$ of $G$.

**PROPOSITION 2**

Every formula of GAL and CAL is equivalent to a formula in NNF.

**PROOF.** The proof is a straightforward ‘pushing’ of negations inside of the scope of operators. We use translation function $t: (GAL \cup CAL) \to \mathcal{N}\mathcal{N}\mathcal{F}$ that is defined as follows:

$$ \begin{array}{lclcl} t(\neg p) & = & \neg p & t(p) & = & p \\ t(\neg(\varphi \wedge \psi)) & = & t(\neg\varphi) \vee t(\neg\psi) & t(\varphi \wedge \psi) & = & t(\varphi) \wedge t(\psi) \\ t(\neg\Box_a\varphi) & = & \Diamond_a t(\neg\varphi) & t(\Box_a\varphi) & = & \Box_a t(\varphi) \\ t(\neg[\psi]\varphi) & = & t(\psi) \wedge t([\psi]\neg\varphi) & t([\psi]\varphi) & = & [t(\psi)]t(\varphi) \\ t(\neg[G]\varphi) & = & \langle G \rangle t(\neg\varphi) & t([G]\varphi) & = & [G]t(\varphi) \\ t(\neg[[G]]\varphi) & = & [[G]]t(\neg\varphi) & t([[[G]]]\varphi) & = & [[G]]t(\varphi) \end{array} $$

<footnote n="1">¹A sound and complete logic with coalition and relativized group announcements is presented in [23]. The truth conditions for the relativized group announcements are $M_s \models [G, \chi]\varphi$ iff $M_s \models \chi$ and $\forall \psi_G \in \mathcal{EL}^G: M_s \models [\psi_G \wedge \chi]\varphi$; $M_s \models \langle G, \chi \rangle \varphi$ iff $M_s \models \chi$ implies $\exists \psi_G \in \mathcal{EL}^G: M_s \models \langle \psi_G \wedge \chi \rangle \varphi$.</footnote>
Note that $\top, \bot, [G, \psi]\varphi$ and $\langle G, \psi\rangle\varphi$ will not appear in the image of the translation. These formulas, however, play the role of final and intermediate steps in games.

Now we are ready to define formula games.

**DEFINITION 9 (Formula games).**

Let some model $M_s$ and $\varphi$ in NNF be given, and suppose that $\mathcal{M}$ is the set of pointed submodels $N_t^X$ of model $M_s$, where $X \subseteq S$ and $s \in X$. A *formula game for $\varphi$ over $M_s$* is a tuple $G_{M_s}^\varphi = (V_\varphi, V_\exists, E, \Delta)$, where

* $V_\varphi = \{\upharpoonright N_t, \psi^\neg | N_t \in \mathcal{M}, \psi \in \mathcal{UNNF}\} \cup \{\upharpoonright N_t, X, \chi, \psi^\neg | N_t \in \mathcal{M}, X \subseteq S, \chi, \psi \in \mathcal{NNF}\}$ is the set of vertices of the $\forall$-player;

* $V_\exists = \{\upharpoonright N_t, \psi^\neg | N_t \in \mathcal{M}, \psi \in \mathcal{ENNF}\}$ is the set of vertices of the $\exists$-player;

* $E \subset (V_\varphi \cup V_\exists) \times (V_\varphi \cup V_\exists)$ is the set of edges, where

$$ E = \bigcup \left( \begin{array}{l} \{ (\upharpoonright N_t, p^\neg, \upharpoonright N_t, \top^\neg), (\upharpoonright N_t, \neg q^\neg, \upharpoonright N_t, \top^\neg) \mid t \in V(p) \text{ and } t \notin V(q) \} \\ \\ \{ (\upharpoonright N_t, p^\neg, \upharpoonright N_t, \bot^\neg), (\upharpoonright N_t, \neg q^\neg, \upharpoonright N_t, \bot^\neg) \mid t \notin V(p) \text{ and } t \in V(q) \} \\ \\ \{ (\upharpoonright N_t, \psi \wedge \chi^\neg, \upharpoonright N_t, \psi^\neg), (\upharpoonright N_t, \psi \wedge \chi^\neg, \upharpoonright N_t, \chi^\neg) \} \\ \\ \{ (\upharpoonright N_t, \psi \vee \chi^\neg, \upharpoonright N_t, \psi^\neg), (\upharpoonright N_t, \psi \vee \chi^\neg, \upharpoonright N_t, \chi^\neg) \} \\ \\ \{ (\upharpoonright N_t, \Box_a \psi^\neg, \upharpoonright N_u, \psi^\neg) \mid t \sim_a u \} \\ \\ \{ (\upharpoonright N_t, \Diamond_a \psi^\neg, \upharpoonright N_u, \psi^\neg) \mid t \sim_a u \} \\ \\ \{ (\upharpoonright N_t, [\chi] \psi^\neg, \upharpoonright N_t, X, \chi, \psi^\neg) \} \\ \\ \{ (\upharpoonright N_t, X, \chi, \psi^\neg, \upharpoonright N_u, \chi^\neg) \mid u \in X \} \\ \\ \{ (\upharpoonright N_t, X, \chi, \psi^\neg, \upharpoonright N_u, t(\neg \chi)^\neg) \mid u \in S \setminus X \} \\ \\ \{ (\upharpoonright N_t, X, \chi, \psi^\neg, \upharpoonright N_t^X, \psi^\neg) \} \\ \\ \{ (\upharpoonright N_t, [G] \psi^\neg, \upharpoonright N_t, [t(\psi_G)] \psi^\neg) \} \\ \\ \{ (\upharpoonright N_t, \langle G \rangle \psi^\neg, \upharpoonright N_t, t(\psi_G) \wedge [t(\psi_G)] \psi^\neg) \} \\ \\ \{ (\upharpoonright N_t, [[G]] \psi^\neg, \upharpoonright N_t, \langle \overline{G}, t(\psi_G) \rangle \psi^\neg) \} \\ \\ \{ (\upharpoonright N_t, \{G\}] \psi^\neg, \upharpoonright N_t, [\overline{G}, t(\psi_G)] \psi^\neg) \} \\ \\ \{ (\upharpoonright N_t, [G, \chi] \psi^\neg, \upharpoonright N_t, \chi \wedge [t(\psi_G) \wedge \chi] \psi^\neg) \} \\ \\ \{ (\upharpoonright N_t, \langle G, \chi \rangle \psi^\neg, \upharpoonright N_t, t(\neg \chi) \vee (t(\psi_G) \wedge [\chi \wedge t(\psi_G)] \psi^\neg) \} \end{array} \right) ; $$

* $\Delta$ is the initial vertex $\upharpoonright M_s, \varphi^\neg$.

The game is played between the $\forall$-player and the $\exists$-player, and a *play* consists of a sequence of vertices $\Delta, \Delta_1, \dots, \Delta_n$. The play is built by the players such that for some edge $(\Delta_m, \Delta_{m+1}) \in E$ if $\Delta_m \in V_\varphi$, then the universal player chooses $\Delta_{m+1}$, and if $\Delta_m \in V_\exists$, then the existential player chooses $\Delta_{m+1}$. If either player is unable to move, i.e. they are in a $\top$-vertex or $\bot$-vertex, then they lose the game. For examples of formula games, see Appendix A.
Whether a vertex in a formula game belongs to the $∃$-player or to the $∀$-player depends on the current subformula: if the subformula is in $\mathcal{ENNF}$, then it is the $∃$-player's move, and if the subformula is in $UNNF$, then it is the $∀$-player's move. Edges $E$ in Definition 9 specify which kinds of moves are available to the players in various vertices. For example, if we are in vertex $\lceil N_t, \psi \lor \chi \rceil$ of a formula game, then the existential player can choose either to move to vertex $\lceil N_t, \psi \rceil$ or to vertex $\lceil N_t, \chi \rceil$. If the current vertex of a game is $\lceil N_t \sqcap_a \psi \rceil$, then the $∀$-player can choose any $a$-successor state $u$ of $t$, and the game continues in $\lceil N_u \psi \rceil$.

Now, if a game is in vertex $\lceil N_t, [\chi] \psi \rceil$, then the $∃$-player chooses any subset $X$ of the set of states $S$ of the original model $M$. From the resulting vertex of the game $\lceil N_t, X, \chi, \psi \rceil$, the $∀$-player can challenge the choice of $X$ by the existential player in three following ways. First, she can check whether $\chi$ indeed holds in all states of $X$, or, formally, she makes a move to vertex $\lceil N_u, \chi \rceil$ for some $u \in X$. Alternatively, the $∀$-player can check whether all $\chi$-states were included in $X$ by making a transition to vertex $\lceil N_u, t(\neg \chi) \rceil$ for some $u \in S \setminus X$. Finally, the universal player can allow the game to carry on in submodel $N_t^X$ with subformula $\psi$, i.e. she can make a move to vertex $\lceil N_t^X, \psi \rceil$. All these three options are designed to mimic the semantics of public announcements.

As for quantifier modalities, consider, for instance, vertex $\lceil N_t, [[G]] \psi \rceil$. Since $[[G]] \psi \in UNNF$, the $∀$-player can move to any vertex $\lceil N_t, \langle \overline{G}, t(\psi_G) \rangle \rceil$, where $\psi_G \in \mathcal{EL}^G$. From the chosen vertex, the $∃$-player then moves to one of the vertices $\lceil N_t, t(\neg \psi_G) \rceil \lor (t(\chi_{\overline{G}}) \land [\psi_G \land t(\chi_{\overline{G}})] \psi) \rceil$ with $\chi_{\overline{G}} \in \mathcal{EL}^{\overline{G}}$. These moves follow the semantics of coalitional announcements.

Let us ensure that there are no loops in games, i.e. plays of games are finite.

**PROPOSITION 3**

Given formula $\varphi$ in NNF, pointed model $M_s$, and a game $G_{M_s}^{\varphi}$, every play of the game is finite.

**PROOF.** The proof is by induction on subformulas of $\varphi$.

*Base case:* in the case of a propositional variable, there is exactly one step in a play of the game.

*Induction hypothesis:* plays of the game for subformulas $\psi, t(\neg \chi)$ and $\chi$ are finite on all pointed submodels $N_t$ of $M$.

The propositional and epistemic cases are straightforward, so we omit them. Also note that it means that plays for epistemic formulas are finite.

*Case* $\lceil N_t, [\chi] \psi \rceil$: in this node of the game, the existential player chooses a subset of the set of states of the given model. Such a choice leads to one of the vertices $\lceil N_t, X, \chi, \psi \rceil$. Every possible choice of the $∀$-player from this vertex — $\lceil N_t, \chi \rceil$, $\lceil N_u, t(\neg \chi) \rceil$ or $\lceil N_t^X, \psi \rceil$—leads to a vertex with a play for either $\chi, t(\neg \chi)$ or $\psi$ that is finite by the induction hypothesis. Hence, a play of the game in $\lceil N_t, [\chi] \psi \rceil$ is finite.

*Case* $\lceil N_t, [G] \psi \rceil$: there is just one step from this vertex to some $\lceil N_t, [t(\psi_G)] \psi \rceil$, and using the induction hypothesis and the fact that agents can only announce epistemic formulas, we conclude that the play from this vertex is finite.

*Cases* $\lceil N_t, \langle G \rangle \psi \rceil$, $\lceil N_t, [G, \chi] \psi \rceil$ and $\lceil N_t, \langle G, \chi \rangle \psi \rceil$ are similar to the previous one.

*Case* $\lceil N_t, [[G]] \psi \rceil$: from this vertex, there is exactly one $∀$-step to some $\lceil \langle \overline{G}, t(\psi_G) \rangle \psi \rceil$. Since $t(\psi_G)$ is a formula of EL, and $\overline{G}$ can only announce epistemic formulas, we have that a play from $\lceil N_t, [[G]] \psi \rceil$ is finite.

*Case* $\lceil N_t, [[G]] \psi \rceil$ is the same as above. $\square$

<figure><img src="image_6.png" /></figure>

The next proposition ties together satisfiability and the existence of a winning strategy. In particular, we show that if a formula is true in a model, then the $∃$-player has a winning strategy in the corresponding formula game, and vice versa. Or, equivalently, a formula is false in a model if and only if in the corresponding formula game the $∀$-player has a winning strategy.
PROPOSITION 4

The $\exists$-player has a winning strategy in a game $G_{M_s}^\varphi$ if and only if $M_s \models \varphi$.

PROOF. *From right to left.* The proof is by induction on the size of subformulas of $\varphi$. Observe that this is straightforward to provide a size relation $c$ such that quantifiers are taken into account first. See [23] for an example of such a relation.

*Base case:* assume that $M_s \models p$. Then the corresponding formula game consists only of one $\exists$-step from $\lceil M_s, p \rceil$ to $\lceil M_s, \top \rceil$ and the latter is the winning vertex of the existential player. The same argument holds for $\neg p$.

*Induction hypothesis:* assume that for all pointed submodels $N_t$ of $M$ and all formulas $t(\psi)$ in NNF such that $c(t(\psi)) < c(\varphi)$, if $N_t \models t(\psi)$, then $\lceil N_t, t(\psi) \rceil$ is a winning position for the $\exists$-player.

Propositional and epistemic cases are straightforward.

*Case* $M_s \models [\psi]\chi$: by the semantics this means that $M_s \models \neg\psi$ or $M_s^\psi \models \chi$. If the former is the case, then consider $X = [[\psi]]_M$ and $Y = W \setminus [[\psi]]_M$, where $X$ can be an empty set. We have that for all $t \in X$: $M_t \models \psi$ and for all $u \in Y$: $M_u \models t(\neg\psi)$. By the induction hypothesis, this implies that $\lceil M_t, \psi \rceil$ and $\lceil M_u, t(\neg\psi) \rceil$ are winning positions for the existential player for all $t \in X$ and $u \in Y$. Hence, $\lceil M_s, X, \psi, \chi \rceil$ is also a winning position for the $\exists$-player that she can choose from $\lceil M_s, [\psi]\chi \rceil$.

If $M_s^\psi \models \chi$, then again, we consider $X = [[\psi]]_M$ similarly to the case of $M_s \models \neg\psi$. Since $s \in X$, we need to deal with an additional case $M_s^X \models \chi$. By the induction hypothesis, this means that $\lceil M_s^X, \chi \rceil$ is a winning position for the $\exists$-player. Hence, $\lceil M_s, X, \psi, \chi \rceil$ is also a winning position for the $\exists$-player that she can choose from $\lceil M_s, [\psi]\chi \rceil$.

*Case* $M_s \models \langle G \rangle \psi$: by the semantics, $M_s \models \langle G \rangle \psi$ is equivalent to $\exists \psi_G: M_s \models \langle \psi_G \rangle \psi$. The latter is equivalent to $M_s \models t(\psi_G) \wedge [t(\psi_G)]\psi$. By the induction hypothesis, that means that the $\exists$-player can always choose a step in the game that corresponds a winning position $\lceil M_s, t(\psi_G) \wedge [t(\psi_G)]\psi \rceil$. Thus, $\lceil M_s, \langle G \rangle \psi \rceil$ is also a winning position for the existential player.

*Case* $M_s \models [G]\chi$: a similar argument as above.

*Case* $M_s \models \langle G \rangle \psi$: by the semantics of coalition announcements, this is equivalent to $\exists \psi_G, \forall \chi_{\overline{G}}$: $M_s \models \psi_G \wedge [\psi_G \wedge \chi_{\overline{G}}]\varphi$. By the induction hypothesis, the latter is equivalent to the fact that $\lceil M_s, t(\psi_G) \wedge [t(\psi_G) \wedge t(\chi_{\overline{G}})] \rceil$ are winning positions of the existential player. This means that $\lceil M_s, [\overline{G}, t(\psi_G)] \rceil$ is also a winning position for the $\exists$-player, which she can choose from $\lceil M_s, \langle G \rangle \varphi \rceil$.

*Case* $M_s \models \langle G \rangle \psi$: similar to the previous one.

*From left to right.* A similar argument as in the opposite direction for the contraposition: if $M_s \not\models \varphi$, then the $\forall$-player has a winning strategy in a game $G_{M_s}^\varphi$. $\square$

# 6 Chain models

In order to compare the relative expressivity of GAL and CAL, it is not enough to consider just a pair of models. Suppose that for some $\varphi \in \mathcal{GAL}$, we have that $M_s \models \varphi$ and $N_t \not\models \varphi$. In this case, formula $\varphi$ must have subformulas with group announcement operators, for otherwise $\varphi$ would be a CAL formula as well. Hence, in $\varphi$ or its negation, there is an existential group announcement operator $\langle G \rangle \psi$. According to the semantics, this implies that we can substitute $\langle G \rangle \psi$ with some $\langle \psi_G \rangle \psi$. And $\varphi$ with such a substitution for all group announcements operators is a PAL (and hence CAL) formula. In other words, given two finite models, group announcement operators $[G]\varphi$ can be 'simulated' via a disjunction of finitely many (up to equivalence of corresponding updated models) possible updates $[\psi_G]\varphi$.
<figure><img src="image_7.png" /><figcaption>FIGURE 5. A (1, 12)-chain.</figcaption></figure>

<figure><img src="image_8.png" /><figcaption>FIGURE 6. A bisimulation (wavy arrows) between chains (1, 5) (in the middle) and (1, 10) (starts at the top and wraps around on the right to the bottom).</figcaption></figure>

The same argument can be carried out for any finite set of epistemic models. Therefore, in order to unleash the full potential of group announcement operators, we consider two infinite sets of models. After that, we show that there is GAL formula that is true in one such set and false in the other, and no CAL formula can capture the difference between the sets.

The models we are dealing with are called chain models.

**DEFINITION 10 (Chain models).**

A chain model, or a *chain*, is an epistemic model $M = (S, \sim, V)$, where

* $S = \{l, l+1, \dots, r-1, r\} \subset \mathbb{Z}$ is a finite set of consecutive integers,

* $x \sim_a y$ if and only if $y = x + 1$ and $x$ is even,

* $x \sim_b y$ if and only if $y = x + 1$ and $x$ is odd,

* $z - 1 \sim_c z \sim_c z + 1$ if and only if $z \bmod 3 = 1$,

* $V(p) = \{3k, 3k-1 \in S \mid k \in \mathbb{Z}\}$.

We use pair $(l, r)$ to refer to the corresponding chain model.

In a graphical representation of chains, we use a solid line for agent $a$'s relation, a dashed line for $b$'s relation and $c$ cannot distinguish states in the same dotted box. An example of a chain is presented in Figure 5.

Chain models are regular in their structure, and they may only differ from each other in leftmost and rightmost states. Hence, we can give a classification of chains based on their extremities.

**DEFINITION 11 (Classification of chains).**

Let some chain model $(x, y)$ be given.

* If $x \bmod 6 = 1$ ($y \bmod 6 = 4$), then $M_x \models \Box_a \neg p$ ($M_y \models \Box_a \neg p$).

* If $x \bmod 6 = 2$ ($y \bmod 6 = 3$), then $M_x \models \Box_b \Box_a p$ ($M_y \models \Box_b \Box_a p$).

* If $x \bmod 6 = 3$ ($y \bmod 6 = 2$), then $M_x \models \Box_a p$ ($M_y \models \Box_a p$). Note that for such an $x$ ($y$), chain $(x, y)$ is bisimilar to model $(2x - (y+1), y)$ ($(x, 2y - x + 1)$) via bisimulation $\{(x+k, x-k-1) \mid 0 \le k \le y-x\}$ ($(y+k+1, y-k) \mid 0 \le k \le y-x$). See Figure 6 for an example.
<figure><img src="image_9.png" /><figcaption>FIGURE 7. [1, 2]-Models.</figcaption></figure>

<figure><img src="image_10.png" /><figcaption>FIGURE 8. [0, 4]-Models.</figcaption></figure>

<figure><img src="image_11.png" /><figcaption>FIGURE 9. The only chain of type [0, 2] up to bisimulation (wavy arrows).</figcaption></figure>

* If $x \mod 6 = 4$ ($y \mod 6 = 1$), then $M_x \models \Box_b \neg p$ ($M_y \models \Box_b \neg p$).

* If $x \mod 6 = 5$ ($y \mod 6 = 0$), then $M_x \models \Box_a \Box bp$ ($M_y \models \Box_a \Box bp$).

* If $x \mod 6 = 0$ ($y \mod 6 = 5$), then $M_x \models \Box bp$ ($M_y \models \Box bp$). Note that for such an $x$ ($y$), chain $(x, y)$ is bisimilar to model $(2x - (y+1), y)$ ($(x, 2y - x + 1)$) via bisimulation $\{(x+k, x-k-1) \mid 0 \le k \le y-x\}$ ($(y + k + 1, y-k) \mid 0 \le k \le y-x$). See Figure 6.

Therefore, we can describe the type of a chain $(x, y)$ as the pair $[x \mod 6, y \mod 6]$.

In our proof, we are primarily interested in models of types [1, 2], [0, 4] and [0, 2], and their examples are depicted in Figures 7–9. We also note that models with ‘unbroken’ $c$-relations are all bismilar to a [0, 2]-chain (see Figure 9).

**DEFINITION 12 (Terminal state).**

Given a [1, 2]- or [0, 4]-chain $M$, state $x$ of the model is called terminal, if $M_x \models \Omega$, where $\Omega := \Box_a \neg p$.

In Figures 7 and 8, the terminal state is the leftmost and rightmost states, respectively. Note that in such models, there is only one terminal state.

In the next section, we use terminal states to define a property expressible in GAL (but not in CAL). Moreover, terminal states may be used to target other states in the model in order to ‘cut’ chains. For example, to specify a state that is exactly three steps from the $\Omega$-state, we can use the formula:

$$ \Omega + 3 := \Diamond_b \Diamond_a \Diamond_b \Omega \wedge \Box_a \Box_b \Box_a \neg \Omega. $$

See Figure 10 for representation of the formula.
<figure><img src="image_12.png" /><figcaption>FIGURE 10. Removing states from a model using $\Omega$.</figcaption></figure>

<figure><img src="image_13.png" /><figcaption>FIGURE 11. $Mid_a$ and $Mid_b$.</figcaption></figure>

In the example, if agent $b$ announces, for instance $\Box_b \neg (\Omega + 3)$, the updated model will be the one without the $b$-link with the $\Omega + 3$-state (squared). A similar announcement $\Box_a \neg (\Omega + 3)$ can be made by agent $a$, and group $\{a, b\}$ can cut any $a$- and $b$-links in models with terminal states.

Now let us consider non-terminal rightmost and leftmost states in [1, 2]- and [1, 4]-chains. They are presented in Figure 11. In Definition 11, we pointed out that no epistemic formula can distinguish these states from $n$-bisimilar ones in larger models. In other words, in order to specify such states, we should refer to the terminal one. Epistemic formulas, however, have a finite size, and hence formulas that refer to the terminal state are true only in chains of some depth, and we can always find a larger chain of the same type such that any given epistemic formula that was true in the smaller model will be false in the greater one.

Therefore, we use formulas of GAL to describe these non-terminal states, and we call these formulas $Mid_a$ and $Mid_b$. The former is defined as

$$ Mid_a := \Box_a p \wedge [A](\Diamond_b \neg p \rightarrow \Box_a \Diamond_b \neg p), $$

and it holds in the rightmost states of [1, 2]-models. The latter is defined as

$$ Mid_b := \Box_b p \wedge [A](\Diamond_a \neg p \rightarrow \Box_b \Diamond_a \neg p), $$

and it holds in the leftmost states of [0, 4]-models.

# 7 Groups versus coalitions

In this section, we define a property of [1, 2]-chains expressible in GAL (Section 7.1) and show that it is impossible to capture that property in CAL (Section 7.2).

## 7.1 What GAL can express

We start this section with formulas that are valid on a certain class of chain models. First,

$$ T(0, 2) := \Box_a \Box_b (\neg p \rightarrow [A]((\Diamond_a p \wedge \Diamond_b p) \rightarrow \Box_a \Box_b \neg (\Box_a p \wedge \Box_b p))) $$

distinguishes [0, 2]-models, as there is no announcement from any agent that can make $a$ and $b$ know $p$ without removing all $\neg p$ states.
<figure><img src="image_14.png" /><figcaption>FIGURE 12. A (1, 8)-model, where $s = 7$, and $(1, 8)_s$ is an $a$-model.</figcaption></figure>

Formulas for [1, 2]- and [0, 4]-models are as follows:

$$T(1, 2) := \neg T(0, 2) \wedge [\Box_b \neg \Omega] T(0, 2) \wedge [\neg Mid_b \wedge \Box_b \neg \Omega] T(0, 2),$$

$$T(0, 4) := \neg T(0, 2) \wedge [\Box_b \neg \Omega] T(0, 2) \wedge [\neg Mid_a \wedge \Box_b \neg \Omega] T(0, 2).$$

Intuitively, they mean that [1, 2]- and [0, 4]-chains are not bisimilar to [0, 2]-chains (first conjunct), removing the link with the terminal state makes them bisimilar to a [0, 2]-chain (second conjunct), and they differ between each other in extreme non-terminal states described by $Mid_a$ and $Mid_b$ (third conjunct). Note that group announcement operators appear only in $T(0, 2)$, $Mid_a$ and $Mid_b$, and none of these formulas mention agent c.

The actual property we are interested in applies to pointed models. Given a pointed model $(l, r)_s$ of type [1, 2], is the terminal node in the $a$ direction from $s$ ($(l, r)_s$ is an $a$-model), or the $b$ direction ($(l, r)_s$ is a $b$-model)? See Figure 12 for a representation of this problem.

We show that GAL can express whether a given pointed model is an $a$- or $b$-model.

The formula that expresses the property of $M_s$ being a $b$-model is

$$b : \Omega = \bigwedge \left( \begin{array}{l} \Box_a p \rightarrow \langle \{c\} \rangle (Mid_a \wedge T(1, 2)) \\ \neg p \rightarrow \Box_a (p \rightarrow \langle \{c\} \rangle (Mid_b \wedge T(0, 4))) \\ \Box_b p \rightarrow [\{c\}](Mid_b \rightarrow \neg T(0, 4)) \end{array} \right).$$

Formula $a : \Omega$ can be obtained by swapping subscripts $a$ and $b$, and formulas $T(1, 2)$ and $T(0, 4)$ in $b : \Omega$:

$$a : \Omega = \bigwedge \left( \begin{array}{l} \Box_b p \rightarrow \langle \{c\} \rangle (Mid_b \wedge T(0, 4)) \\ \neg p \rightarrow \Box_b (p \rightarrow \langle \{c\} \rangle (Mid_a \wedge T(1, 2))) \\ \Box_a p \rightarrow [\{c\}](Mid_a \rightarrow \neg T(1, 2)) \end{array} \right).$$

We sketch a proof of correctness of formula $a : \Omega$.

### LEMMA 1

Let sets $M_A$ and $M_B$ of all $a$ and $b$ pointed [1, 2]-chains be given. Then $M_s \models a : \Omega$ for all $M_s \in M_A$ and $N_t \not\models a : \Omega$ for all $N_t \in M_B$.

*PROOF.* The reader is encouraged to use figures from the previous section for reference. Let $M_s \models a : \Omega$ for some [1, 2]-chain $M_s$. Since no conjunction of any two formulas $\Box_b p, \neg p$ or $\Box_a p$ can be true in a pointed chain, we have that either $M_s \models \Box_b p$, or $M_s \models \neg p$, or $M_s \models \Box_a p$.

*Case* $\Box_b p$. Let $M_s \models \Box_b p$. By the construction of chain models, this means that $b$ cannot distinguish two $p$-states in two adjacent $c$-equivalence classes, and $a$ considers $\neg p$ possible in the current $c$-equivalence class. Hence, $c$ can cut $b$'s relation making the current state a $Mid_b$ state. Note that the terminal state remains intact, and thus we have that $T(0, 4)$ holds in the updated model. This means that $M_s \models \langle \{c\} \rangle (Mid_b \wedge T(0, 4))$.
Assume that $N_t \models \Box_b p$. As $N_t$ is a $b$: $\Omega$-model, every cut by $c$ either cuts the $b$-relation and hence cuts the path to the terminal state, or does not satisfy $Mid_b$ ($c$ cannot make the current state to be extreme). Therefore, $N_t \models [{c}](\neg Mid_b \vee \neg T(0, 4))$.

Case $\neg p$. Let $M_s \models \neg p$ and $M_u \models p$ for some $t$ such that $s \sim_b u$. By the construction of chain models, this means that $a$ cannot distinguish two $p$-states in two adjacent $c$-equivalence classes, and $b$ considers $\neg p$ possible in the current $c$-equivalence class. Hence, $c$ can cut $a$'s relation making the current state $t$ a $Mid_a$ state. Note that the terminal state remains intact, and thus we have that $T(1, 2)$ holds in the updated model. This means that $M_u \models p \wedge \langle\{c\}\rangle(Mid_a \wedge T(1, 2))$ for some $s \sim_b u$. We can make the latter formula less strict so that it holds in $\neg p$ states as well: $M_u \models p \rightarrow \langle\{c\}\rangle(Mid_a \wedge T(1, 2))$. By the construction of chains, there are only two states in $b$-relation with the current one: a $p$-state and a $\neg p$-state. Thus, $M_s \models \Box_b(p \rightarrow \langle\{c\}\rangle(Mid_a \wedge T(1, 2)))$, and we finally have that $M_s \models \neg p \rightarrow \Box_b(p \rightarrow \langle\{c\}\rangle(Mid_a \wedge T(1, 2)))$.

Assume that $N_t \models \neg p$ and $N_v \models p$ for some $v$ such that $t \sim_b v$. As $N_t$ is a $b$-model, $N_v$ is an $a$-model. So, every cut by $c$ either cuts the $a$-relation and hence cuts the path to the terminal state, or does not satisfy $Mid_a$ ($c$ cannot make the current state to be extreme). Therefore, $N_v \models [{c}](\neg Mid_a \vee \neg T(1, 2))$.

Case $\Box_a p$. Let $M_s \models \Box_a p$. By the construction of chain models, this means that $a$ cannot distinguish two $p$-states in two $c$-equivalence classes, and $b$ considers $\neg p$ possible in the current $c$-equivalence class. Hence, if $c$ cuts $a$-relation making $Mid_a$ true, she also makes the terminal state inaccessible from the current one. On the other hand, if the terminal state is still accessible from the current state, then in this case, the current state does not satisfy $Mid_a$. This means that $M_s \models [{c}](Mid_a \rightarrow T(1, 2))$.

Assume that $N_t \models \Box \Box_a p$. As $N_t$ is a $b$-model, $c$ has a cut such that $Mid_a$ and $T(1, 2)$ holds. Such a cut ‘removes’ all $c$-equivalence classes to the right of the current state and makes the current state the rightmost state in the updated model. Therefore, $N_t \models \neg [{c}](\neg Mid_a \vee \neg T(1, 2))$. $\Box$

## 7.2 What CAL cannot express

In this section, we show that no CAL formula can capture the property of a pointed model 'being an $a$-model'.

An intuition behind the proof is that CAL operators require all agents announce their knowledge formulas simultaneously. For our chain models, intersection of agents' relations is an identity, and hence if it is possible to force some configuration of an $a$-model, then agents together, whether in the same coalition, or divided, can replicate the same configuration in a $b$-model. Contrast this to formula $a$: $\Omega$ in the previous section. The only agent that makes any announcements is $c$, and her relation is not discerning enough to force isomorphic submodels of some $a$- and $b$-models. If $c$ preserves the terminal state in one class of models, she cannot replicate this announcement in the other class such that the resulting updated models are isomorphic ($c$ cannot cut her own equivalence class to make $\Omega$ true in the opposite direction).

### LEMMA 2

Let sets $M_A$ and $M_B$ of all $a$ and $b$ pointed [1, 2]-chains be given. Then, for all $\Psi \in CAL$, if $M_s \models \Psi$ for all $M_s \in M_A$, then there exists some $N_t \in M_B$ such that $N_t \models \Psi$.

**PROOF.** Suppose, contrary to our claim, that for all $M_s \in M_A$, there is a formula $\Psi \in CAL$ such that $M_s \models \Psi$ and for all $N_t \in M_B$ it holds that $N_t \not\models \Psi$. The proof proceeds by playing simultaneous formula games over all pointed chains.
We also assume that models in both sets are sufficiently large: for $|\Psi| = n$, we have that models in sets $\mathcal{M}_A$ and $\mathcal{M}_B$ are $2^n$-bisimilar to each other. This is to ensure that no epistemic formula can distinguish any two models.

Let us partition the sets of games into $\mathcal{G}_A$ and $\mathcal{G}_B$ where player $\exists$ will have a winning strategy for games in $\mathcal{G}_A$, and player $\forall$ will have a winning strategy for games in $\mathcal{G}_B$.

For all moves in games except moves via coalition announcements, we proceed as follows. If it is an $\exists$-player move, we consider the games played over $\mathcal{M}_A$ and play the move for the $\exists$-player's winning strategy on all models in $\mathcal{M}_A$. We also play the corresponding move over $\mathcal{M}_B$: in the case of disjunction, we choose the same disjunct, and in the case of $\diamond_a$-move in $2^k$-bisimilar states, we consider moves equivalent if the chosen states are $2^{k-1}$-bisimilar. If it is a $\forall$-player move, we play the move that agrees with the $\forall$ winning strategy in $\mathcal{G}_B$ games and copy this move in the $\mathcal{G}_A$ games. Thus, we are playing two winning strategies against one another, and the game ends if either $\exists$-player or $\forall$-player cannot move. However, this cannot happen because all pointed models are $2^n$-bisimilar.

Therefore, we need to show that we can maintain the following invariant: after step $i$ of the formula game, there are infinitely many models of the same type in $\mathcal{M}_A$ and $\mathcal{M}_B$ that are still $2^{n-i}$-bisimilar. In the final step of the game, we end up with some propositional variable on which both classes of models agree. Hence, we have a contradiction since both players have a winning strategy by the assumption.

Cases of boolean and epistemic formulas are trivial.

*Case [χ]ψ*. Assume that for some $M_s \in \mathcal{M}_A$, $\lceil M_s, [\chi] \psi \rceil$ is a winning position for the $\exists$-player. This means that there is a subset $X$ such that $\lceil M_s, X, \chi, \psi \rceil$ is also a winning position. Let for some $N_t \in \mathcal{M}_B$ such that $M_s$ and $N_t$ are $2^{n-i}$-bisimilar, $[[\chi]]_N = Y$. We consider two cases.

First, if $M_s^\chi$ is $2^{n-i-1}$ bisimilar to $N_t^\chi$, then $\exists$ can play the corresponding move $\lceil N_t, Y, \chi, \psi \rceil$ in $\mathcal{G}_B$, and the invariant continues to hold.

In the second case, if $M_s^\chi$ and $N_t^\chi$ are not $2^{n-i-1}$-bisimilar, there is some $u \in S^M$ and some $v \in S^N$ such that $M_u$ and $N_v$ disagree on the interpretation of $\chi$, and $s$ and $t$ are within the same $2^{n-i-1}$ steps from $s$ and $t$, respectively. Suppose $M_u \models \chi$ and $N_v \not\models \chi$. In this case, the $\exists$-player must still play the corresponding move $\lceil N_t, Y, \chi, \psi \rceil$ in $\mathcal{G}_B$, as any alternative to $Y$ would allow the $\forall$-player to have a winning strategy. The universal player, however, can respond with the moves $\lceil M_u, \chi \rceil$ in $\mathcal{G}_A$ and $\lceil N_v, t(\neg \chi) \rceil$ in $\mathcal{G}_B$. According to Proposition 4, the $\exists$-player has a winning strategy in $\lceil N_v, t(\neg \chi) \rceil$, and thus the $\forall$-player has a winning strategy in $\lceil N_v, \chi \rceil$. Since $u$ and $v$ are the same number of steps away from $s$ and $t$, we have that $M_u$ is an $a$-model if and only if $N_v$ is a $b$-model. Moreover, since $u$ and $v$ are within $2^{n-i-1}$ steps and the original models $M_s$ and $N_t$ are $2^{n-i}$-bisimilar, it follows that $M_u$ and $N_v$ are $2^{n-i-1}$-bisimilar. Hence, the invariant holds for those models and the proof proceeds in $M_u$ and $N_v$.

So, we must reach coalition operators. Note that at this point games may cease to be over [1, 2]-models since prior public announcements may have cut chains in various ways. However, this does not affect the proof as we are interested in agents' announcements rather than in chain types. Moreover, for the coalition cases, we do not have to keep the invariant since all these cases lead straight to a contradiction. Moreover, without loss of generality, we assume that agents' announcements are in NNF.

We will consider only existential coalition announcement operators $\llbracket G \rrbracket \psi$, and the corresponding results for $\llbracket G \rrbracket \psi$ can be obtained by swapping $A$ to $B$ and the $\exists$-player to the $\forall$-player.

*Case $\{\{a, b, c\}\} \psi$.* Let $M_s \models \{\{a, b, c\}\} \psi$. According to Definition 9, there is a relativized group announcement by $a, b$ and $c$ such that $\lceil M_s, [\emptyset, \psi_{\{a,b,c\}}] \psi \rceil$ is a winning position for the $\exists$-player. For this node, there is only one possible $\forall$-step: $\lceil M_s, [\psi_{\{a,b,c\}}] \psi \rceil$. Since $\mathcal{M}_B$ is infinite, there is a model
<figure><img src="image_15.png" /><figcaption>FIGURE 13. An *a*-model (above) and a *b*-model (below).</figcaption></figure>

$N_t$ and an announcement $\chi_{\{a,b,c\}}$ by $a$, $b$ and $c$, such that $M_s^{\psi_{\{a,b,c\}}}$ is isomorphic to $N_t^{\chi_{\{a,b,c\}}}$ (see Figure 13 for an example).

Indeed, consider set $S^{\psi_{\{a,b,c\}}}$. We can enumerate states in the set from left to right. Next, let $N^0 = (W^0, \sim^0, V^0)$ be a model such that $S^0 = S^{\psi_{\{a,b,c\}}}$, $s_{n+1-i} \in V^0(p)$ if and only if $s_i \in V(p)$ and $s_{n+1-i} \stackrel{\sim}{=} s_{n-i}$ if and only if $s_i \sim_a s_{i+1}$ for all $a \in A$. In other words, we flip model $M_s^{\psi_{\{a,b,c\}}}$ from left to right. Note that agents' relations are also flipped: if state $w$ was an $a$-state, it would become a $b$-state. Moreover, we can always find a $b$-model $N_t$ that has $N^0$ as a submodel. Since agents can together enforce any configuration of $N_t$, they have a joint announcement $\chi_{\{a,b,c\}}$ such that $N_t^{\chi_{\{a,b,c\}}}$ is isomorphic to $M_s^{\psi_{\{a,b,c\}}}$, where $N_t^{\chi_{\{a,b,c\}}} = N^0$. The same argument can be made in other cases of the proof.

Thus, $\lceil N_t, [\chi_{\{a,b,c\}}] \rceil \psi^{-}$ (and hence $\lceil N_t, [\emptyset, \chi_{\{a,b,c\}}] \rceil \psi^{-}$) is a winning position for the $\exists$-player, and she has a winning strategy for a model from $\mathcal{M}_B$. A contradiction. Note that since agents $a$, $b$ and $c$ can together enforce any configuration of a model (up to bisimulation), the argument holds for the case of arbitrary public announcements.

*Case* $\langle \{a, b\} \rangle \psi$. Let $M_s \models \langle \{a, b\} \rangle \psi$. This means that $\lceil M_s, \langle \{a, b\} \rangle \rceil \psi^{-}$ is a winning position for the $\exists$-player. Therefore, $\lceil M_s, \langle \{c\}, \psi_{\{a,c\}} \rangle \rceil \psi$ is also a winning node for the player. This means that whichever announcement $\psi_{\{c\}}$ by agent $c$ the $\forall$-player chooses, the $\exists$-player is still in a winning position $\lceil M_s, \psi_{\{a,b\}} \land [\psi_{\{a,b\}} \land \psi_{\{c\}}] \rceil \psi^{-}$. There is a model $N_t \in \mathcal{M}_B$ such that for some announcement $\chi_{\{a,b\}}$ by agents $a$ and $b$ it holds that $M_s^{\psi_{\{a,b\}}}$ is isomorphic to $N_t^{\chi_{\{a,b\}}}$, and $c$ has an isomorphic set of possible counter-announcements (see Figure 13 for an example). This is due to the fact that $a$ and $b$ can together force any configuration of a model. Hence, $\lceil N_t, \langle \{c\}, \chi_{\{a,b\}} \rangle \rceil \psi^{-}$ is also a winning position for the existential player, and this leads to a contradiction.

*Case* $\langle \{a, c\} \rangle \psi$. Let $M_s \models \langle \{a, c\} \rangle \psi$. This means that $\lceil M_s, \langle \{a, c\} \rangle \rceil \psi^{-}$ is a winning position for the $\exists$-player. Therefore, $\lceil M_s, \langle \{b\}, \psi_{\{a,c\}} \rangle \rceil \psi$ is also a winning node for the player. This means that whichever announcement $\psi_{\{b\}}$ by agent $b$ the $\forall$-player chooses, the $\exists$-player is still in a winning position $\lceil M_s, \psi_{\{a,c\}} \land [\psi_{\{a,c\}} \land \psi_{\{b\}}] \rceil \psi^{-}$. Consider a model $N_t \in \mathcal{M}_B$. If there is some announcement $\chi_{\{a,c\}}$ by agents $a$ and $c$ such that $M_s^{\psi_{\{a,c\}}}$ and $N_t^{\chi_{\{a,c\}}}$ are isomorphic, then, by the similar reasoning as in the previous case, we have a contradiction. See Figure 14, where counter-announcements by $b$ are depicted by dashed rectangles.

Note that $\{a, c\}$ sometimes cannot make such an announcement because the coalition cannot cut $a$'s relations that are within $c$-equivalence classes, and $M_s^{\psi_{\{a,c\}}}$ may contain some extreme state. In other words, this $a$'s relations that $a$ and $c$ cannot cut may have been cut by a previous public announcement (and hence, the corresponding state is the rightmost or the leftmost one). Since our chosen $a$-model is large enough even after being trimmed by public announcements (i.e. because the
<figure><img src="image_16.png" /><figcaption>FIGURE 14. An *a*-model (above) and a *b*-model (below).</figcaption></figure>

<figure><img src="image_17.png" /><figcaption>FIGURE 15. An *a*-model (above) and a *b*-model (below).</figcaption></figure>

invariant holds), there is an *a*-relation in $M_s^{\psi_{\{a,c\}}}$ between two *c*-equivalence classes that *b* can cut. Moreover, a submodel $M_s^{\psi'_{\{a,c\}}}$ of $M_s^{\psi_{\{a,c\}}}$ that is restricted by that *b*-cut can also be forced by $\{a,c\}$ (because *c* can cut this relation as well). Thus, replicating the corresponding move in $N_t$ allows the existential player to have a winning strategy in a *b*-model no matter what agent *b* announces at the same time, and in this case, the set of responses by *b* will be a subset of those she had in the *a*-model. This means that $\lceil N_t, [\{b\}, \chi_{\{a,c\}}] \psi \rceil$ is also a winning node for the $\exists$-player. Hence, a contradiction. For an example, see Figure 15, where the set of counter-announcements by *b* in a *b*-model is a subset of the set of counter-announcements by *b* in an *a*-model.

*Case* $[\{b, c\}]\psi$ is similar to the previous one.

*Case* $[\{a\}]\psi$. Similar to the case $[\{a, c\}]\psi$. If *a* cannot make $N_t$ isomorphic to $M_s^{\psi_{\{a\}}}$, then it is enough to cut a *b*-relation between two *c*-equivalence classes and 'announce' such a subset of $M_s^{\psi_{\{a\}}}$. In this case, it is still an *a*-announcement in the *b*-model, as well as it is one of the counter-announcements by $\{b, c\}$ in the *a*-model (*c* cuts *b*'s relation). Hence, the set of counter-announcements in the *b*-model is the subset of counter-announcements in the *a*-model.

*Cases* $[\{b\}]\psi$ and $[\{c\}]\psi$ are as the previous one.

This completes the proof. □

Combining Lemmas 1 and 2, we obtain the final result.
### THEOREM 3
$GAL \preceq CAL$.

In case $\langle \{a, b, c\} \rangle \psi$ of the proof agents $a, b$ and $c$ can together force any configuration of a given model. This is due to the fact that the intersection of the corresponding relations is an identity relation. Hence, for chain models $\langle \{a, b, c\} \rangle \psi$ is equivalent to $\langle ! \rangle \psi$ (and $\langle \{\{a, b, c\}\} \rangle \psi$ is equivalent to $\langle ! \rangle \psi$), and we have the following result.

### COROLLARY 1
$GAL \preceq APAL$.

That $GAL \preceq APAL$ was conjectured in [2], where it was also shown that $APAL \preceq GAL$. Now we combine these two results.

### THEOREM 4
$APAL$ and $GAL$ are incomparable.

## 8 Agents who remember how to play

Our counterexample to the validity of $\langle G \rangle \varphi \leftrightarrow \langle G \rangle [\bar{G}] \varphi$ in Proposition 1 relied on the fact that after a group announcement by $G$, $\bar{G}$ lose their ability to force submodels they were able to force in the initial situation. This is due to the fact that the $G$-announcement made some states of the model bisimilar. Since $\bar{G}$ do not ‘remember’ some of the states they considered possible in the original model, $\bar{G}$ lose their strategies in the current model.

The authors of [9, 10] analyse a similar situation arguing that the agents forget what was true after any non-trivial update. To mitigate this, they propose extensions of APAL and GAL with copies of initial models for each epistemic model. Moreover, they extend the syntax of APAL and GAL with operators that allow access to the initial model and call the new logics arbitrary public announcement logic with memory (APALM) and group announcement logic with memory (GALM). We similarly define coalition announcement logic with memory (CALM). The main result of [10] is a complete RE axiomatization of GALM [10, Theorem 25]. The authors do not consider CALM and do not present expressivity results for these logics. The language and semantics of GALM in our contribution and [10] are the same.<fnref n="2" />

### DEFINITION 13

Given a countable set of propositional variables $P$, and a finite set of agents $A$, the languages of APALM, GALM and CALM are defined by the following grammars:

$$ \mathcal{A}\mathcal{P}\mathcal{A}\mathcal{L}\mathcal{M} \quad \exists \varphi \quad := \quad \top \mid p \mid 0 \mid \varphi^0 \mid \neg\varphi \mid \varphi \wedge \varphi \mid \Box_a\varphi \mid U\varphi \mid [\psi]\varphi \mid [!]\varphi $$

$$ \mathcal{G}\mathcal{A}\mathcal{L}\mathcal{M} \quad \exists \varphi \quad := \quad \top \mid p \mid 0 \mid \varphi^0 \mid \neg\varphi \mid \varphi \wedge \varphi \mid \Box_a\varphi \mid U\varphi \mid [\psi]\varphi \mid [G]\varphi $$

$$ \mathcal{C}\mathcal{A}\mathcal{L}\mathcal{M} \quad \exists \varphi \quad := \quad \top \mid p \mid 0 \mid \varphi^0 \mid \neg\varphi \mid \varphi \wedge \varphi \mid \Box_a\varphi \mid U\varphi \mid [\psi]\varphi \mid [(G)]\varphi, $$

where $p \in P$, $a \in A$ and $\psi$ is a formula without quantifiers. We also refer to the fragment without quantifiers and public announcements as $\mathcal{ELM}$.

<footnote n="2">²One of the authors gave a talk at DaLí 2020 with Alexandru Baltag in the audience, after which they had a lively discussion on the possibility of defining something like GALM along the lines of APALM [9]. Then they each went their own way. Only much later, after submission, both groups of authors found out about each other’s GALM work and communicated on their respective results.</footnote>
**DEFINITION 14**

An epistemic model with memory is a tuple $M = (S, S^0, \sim, V)^3$ where $S \subseteq S^0$ is the initial domain, and everything else is the same as in an ordinary epistemic model. For $M$, the corresponding initial model is $M^0 = (S^0, S^0, \sim, V)$.

Now, in the extended languages, formulas with 0 have access to the initial model. Moreover, agents
can announce such formulas.

**DEFINITION 15**

Let an epistemic model with memory $M = (S, S^0, \sim, V)$ be given. The definition of semantics is an extension of the one for the logics without memory. The semantics<fnref n="4" /> of APALM, GALM and CALM are as usual with the following exceptions:

$$
\begin{align*}
M_s &\models 0 && \text{iff } S = S^0 \\
M_s &\models \varphi^0 && \text{iff } M_s^0 \models \varphi \\
M_s &\models U\varphi && \text{iff } M_t \models \varphi \text{ for all } t \in S \\
M_s &\models [!]\varphi && \text{iff } M_s \models [\psi]\varphi \text{ for all } \psi \in \mathcal{ELM} \\
M_s &\models [G]\varphi && \text{iff } M_s \models [\psi_G]\varphi \text{ for all } \psi_G \in \mathcal{ELM}^G \\
M_s &\models [[G]]\varphi && \text{iff } M_s \models \psi_G \rightarrow (\psi_G \wedge \chi_{\bar{G}}^\varphi)\varphi \text{ for all } \psi_G \in \mathcal{ELM}^G \text{ and some } \chi_{\bar{G}} \in \mathcal{ELM}^{\bar{G}},
\end{align*}
$$

where $\mathcal{ELM}^G$ and $\mathcal{ELM}^{\bar{G}}$ are defined similarly to $\mathcal{EL}^G$ and $\mathcal{EL}^{\bar{G}}$.

Of course, the set $S$ with the requirement $S \subseteq S^0$ of epistemic models with memory is not always a definable subset of $S^0$. Hence, a subset of these models is considered. An announcement model is an epistemic model with memory $M = (S, S^0, \sim, V)$ such that $S = (S^0)^\psi$ for some quantifier-free $\psi$.

Let us reconsider the counterexample to the validity of $\langle G \rangle \varphi \leftrightarrow \langle G \rangle [\bar{G}] \varphi$ from the perspective of GALM and CALM in Figure 16. Recall that $G = \{a\}$, $\bar{G} = \{b, c\}$ and $\varphi := \diamond_a \Box_b \neg p \wedge \diamond_a (\diamond_b p \wedge \diamond_c \neg p)$.

It is easy to see that announcement $\psi_{\{a\}} := \Box_a(\neg p \rightarrow \diamond_b p)$ of $\{u', t', s, t, u\}$ by $a$ does not make $u$ and $u'$, $t$ and $t'$ bisimilar in the updated model $M_s^{\psi_a}$, and hence $\{b, c\}$ retain their powers. In particular, $b$ and $c$ can make a subsequent announcement that refers to the initial model, $\chi_{\{b,c\}} := \Box_b(\diamond_b p)^0 \wedge \Box_c((p \rightarrow (\Box_b p \vee \diamond_c \neg p)))^0$. The resulting model, $M_s^{\psi_{\{a\}} \cdot \chi_{\{b,c\}}}$, satisfies $\varphi$.

Thus, in GALM and CALM, as opposed to GAL and CAL, agents do not lose their strategies after public announcements. Once they can distinguish a pair of states, they are always able to distinguish them by referring to the initial model.

Now we give this intuition a formal treatment. In what follows, we will occasionally use validities of PAL and of GALM. They can be found in [20, Chapter 4] and [10], respectively. In order to show that $\langle G \rangle [\bar{G}] \varphi \rightarrow \langle G \rangle \varphi$, let us first show a useful auxiliary proposition.

<footnote n="3">³We use the same letters for both standard epistemic models and epistemic models with memory because different types of models never appear in the same context in the paper.</footnote>

<footnote n="4">⁴Again, we use the same symbol $\models$ for both the semantics of APAL, GAL, CAL and their counterparts with memory.</footnote>
<figure><img src="image_18.png" /><figcaption>FIGURE 16. Model $M_s$ and its updates $M_s^{\psi_{\{a\}}}$ and $M_s^{\psi_{\{a\}} \cdot \chi_{\{b,c\}}}$, with the current model depicted in the rounded rectangles.</figcaption></figure>

PROPOSITION 5

$\Box_a(\Box_a\varphi)^0 \leftrightarrow (\Box_a\varphi)^0$ is valid.

PROOF. The validity of the formula from left to right follows from the validity of T axiom.

Consider the contrapositive of the other direction: $\Diamond_a \neg(\Box_a\varphi)^0 \rightarrow \neg(\Box_a\varphi)^0$. Using GALM validity $\neg\varphi^0 \leftrightarrow (\neg\varphi)^0$, we can rewrite the latter as $\Diamond_a(\Diamond_a\neg\varphi)^0 \rightarrow (\Diamond_a\neg\varphi)^0$.

Assume that for an arbitrary $M_s$ we have that $M_s \models \Diamond_a(\Diamond_a\neg\varphi)^0$. By the semantics, this means that there is $t \in S$ such that $s \sim_a t$ and $M_t \models (\Diamond_a\neg\varphi)^0$. The latter is equivalent to $M_t^0 \models \Diamond_a\neg\varphi$, which in turn is equivalent to the fact that there is $u \in S^0$ such that $t \sim_a u$ and $M_u^0 \models \neg\varphi$. By the definition of announcement models, it follows that if $s \in S$, then $s \in S^0$. Since $\sim_a$ is an equivalence relation, it follows from $s \sim_a t$ and $t \sim_a u$ that $s \sim_a u$. Hence, we have $M_s^0 \models \Diamond_a\neg\varphi$, which is equivalent to $M_s \models (\Diamond_a\neg\varphi)^0$ by the semantics. $\square$

From Proposition 5, it follows that if an agent knows some formula in the initial model, then after any update they will know that they knew the formula.

COROLLARY 2

$(\Box_a\varphi)^0 \wedge \psi \leftrightarrow \langle\psi\rangle\Box_a(\Box_a\varphi)^0$ is valid.

PROOF. Let $M_s \models (\Box_a\varphi)^0 \wedge \psi$ for some arbitrary $M_s$. It is a theorem of GALM that $\varphi^0 \leftrightarrow [\chi]\varphi^0$ for all quantifier-free $\chi$. Thus, $M_s \models (\Box_a\varphi)^0 \wedge \psi$ is equivalent to $M_s \models [\psi](\Box_a\varphi)^0 \wedge \psi$, and then, by PAL reasoning, to $M_s \models \langle\psi\rangle(\Box_a\varphi)^0$. Finally, the latter is equivalent to $M_s \models \langle\psi\rangle\Box_a(\Box_a\varphi)^0$ by Proposition 5. $\square$

The next proposition follows from the definition of announcements models. Informally, it states that we can make the announcement, by which the announcement model is defined, explicit.

PROPOSITION 6

Let $M_s = (S, S^0, R, V)$ be an announcement model such that $S = (S^0)^\tau$ for some $\tau$. Then the following holds:

$$M_s \models \varphi \text{ iff } M_s^0 \models \langle\tau\rangle\varphi.$$
PROPOSITION 7

Let $M = (S, S^0, R, V)$ be an announcement model, $S = (S^0)^\tau$ for some $\tau$, $\theta$ be a formula and $G \subseteq A$.
For all $\chi_G$, there is $\psi_G$ such that

$$M_s \models \langle \theta \rangle \langle \psi_G \rangle \varphi \text{ iff } M_s \models \langle \theta \wedge \chi_G \rangle \varphi.$$

PROOF. Assume that for an arbitrary $M_s$ with $S = (S^0)^\tau$ and $\chi_G := \bigwedge_{i \in G} \Box_i \psi_i$, we have $M_s \models \langle \theta \wedge \bigwedge_{i \in G} \Box_i \psi_i \rangle \varphi$. Consider $\psi_G := \bigwedge_{i \in G} \Box_i (\Box_i[\tau] \psi_i)^0$. We need to show that

$$M_s \models \langle \theta \rangle \langle \bigwedge_{i \in G} \Box_i (\Box_i[\tau] \psi_i)^0 \rangle \varphi \text{ iff } M_s \models \langle \theta \wedge \bigwedge_{i \in G} \Box_i \psi_i \rangle \varphi.$$

Consider $M_s \models \langle \theta \rangle \langle \bigwedge_{i \in G} \Box_i (\Box_i[\tau] \psi_i)^0 \rangle \varphi$. By Proposition 6, we can rewrite it as

$$M_s^0 \models \langle \tau \rangle \langle \theta \rangle \langle \bigwedge_{i \in G} \Box_i (\Box_i[\tau] \psi_i)^0 \rangle \varphi,$$

which is equivalent, by application of $\langle \psi \rangle \langle \chi \rangle \varphi \leftrightarrow \langle \psi \wedge \langle \psi \rangle \chi \rangle \varphi$ twice, to

$$M_s^0 \models \langle \tau \wedge \langle \tau \rangle \theta \wedge \langle \langle \tau \rangle \theta \rangle \bigwedge_{i \in G} \Box_i (\Box_i[\tau] \psi_i)^0 \rangle \varphi.$$

By Corollary 2, we get

$$M_s^0 \models \langle \tau \wedge \langle \tau \rangle \theta \wedge \bigwedge_{i \in G} (\Box_i[\tau] \psi_i)^0 \rangle \varphi,$$

and since the announcement is made in the initial model, we can get rid of zeroes in the announcement:

$$M_s^0 \models \langle \tau \wedge \langle \tau \rangle \theta \wedge \bigwedge_{i \in G} \Box_i[\tau] \psi_i \rangle \varphi.$$

By PAL reasoning (in particular, by validity $\psi \wedge \Box_a[\psi] \varphi \leftrightarrow \langle \psi \rangle \Box_a \varphi$), the latter is equivalent to

$$M_s^0 \models \langle \langle \tau \rangle \theta \wedge \langle \tau \rangle \bigwedge_{i \in G} \Box_i \psi_i \rangle \varphi,$$

and further to

$$M_s^0 \models \langle \tau \rangle \langle \theta \wedge \bigwedge_{i \in G} \Box_i \psi_i \rangle \varphi$$

by $\langle \psi \rangle \chi \wedge \langle \psi \rangle \varphi \leftrightarrow \langle \psi \rangle (\psi \wedge \chi)$ and $\langle \psi \rangle \langle \chi \rangle \varphi \leftrightarrow \langle \langle \psi \rangle \chi \rangle \varphi$. From the fact that $S = (S^0)^\tau$ by Proposition 6, we yield

$$M_s \models \langle \theta \wedge \bigwedge_{i \in G} \Box_i \psi_i \rangle \varphi.$$

□

Finally, we are to show that $[[G]]\varphi \leftrightarrow [G]\langle \bar{G} \rangle \varphi$.

PROPOSITION 8

$[[G]]\varphi \leftrightarrow [G]\langle \bar{G} \rangle \varphi$ is valid.
<figure><img src="image_19.png" /><figcaption>FIGURE 17. Overview of the expressivity results. An arrow from $\mathcal{L}_1$ to $\mathcal{L}_2$ means $\mathcal{L}_1 \le \mathcal{L}_2$. If there is no symmetric arrow, then $\mathcal{L}_1 < \mathcal{L}_2$. This relation is transitive, and we omit transitive arrows in the figure. An arrow from $\mathcal{L}_1$ to $\mathcal{L}_2$ is crossed out, if $\mathcal{L}_1 \not\le \mathcal{L}_2$. Arrows labelled with the question mark denote open problems.</figcaption></figure>

**PROOF.** *From left to right.* Assume that $M_s \models [(G)]\varphi$ for some arbitrary $M_s$. By the semantics, this means that $\forall\psi_G, \exists\psi_{\overline{G}}: M_s \models \psi_G \rightarrow (\langle\psi_G \wedge \psi_{\overline{G}}\rangle\varphi$. Pick an arbitrary true $\psi_G$ and the corresponding $\psi_{\overline{G}}$. By Proposition 7, there is a $\chi_{\overline{G}}$ such that $M_s \models \langle\psi_G\rangle\langle\chi_{\overline{G}}\rangle\varphi$, which implies $M_s \models [\psi_G]\langle\chi_{\overline{G}}\rangle\varphi$. Since $\psi_G$ was arbitrary, we can conclude that $M_s \models [G]\langle\overline{G}\rangle\varphi$. The other direction was proved in [25]. □

Having the validity in Proposition 8, it is straightforward to define a translation from formulas of $CALM$ into equivalent formulas of $GALM$. Whether there is a translation in the other direction is an open problem.

**COROLLARY 3**
$CALM \leq GALM$.

# 9 Conclusion and open questions

The interaction between group and coalition announcements is not trivial. As we showed, the simple rewriting via $[(G)]\varphi \leftrightarrow \langle G \rangle [\overline{G}]\varphi$ does not work; the agents may forget that they used to distinguish certain states and thus lose some of their strategies.

In order to tackle the problem of the relative expressivity of GAL and CAL, we introduced formula games that employed, apart from the normal formulas of the languages, relativized group announcements. The latter allowed us to split moves in game that corresponded to coalition announcements: first, we chose an announcement by a coalition, then we chose an announcement by the anti-coalition. The games were played on two infinite sets of chain models, and this leads to the proof of CAL being not at least as expressive as GAL. We get the corresponding result for APAL as a corollary and, moreover, showed that CAL is not at least as expressive as APAL.

The landscape of the expressivity results of the logics of quantified announcements and the remaining open questions are shown in Figure 17.

We also argued that agents do not forget their strategies if the access to the initial model is preserved. In particular, we showed that GALM is at least as expressive as CALM: if agents can refer to the initial model, then once they are able to distinguish states, they will always be able to do it (as long as the states are in the current model). Whether GALM is more expressive that CALM is
an open question. Our proof for GAL and CAL does not extend trivially to the logics with memory, since in the proof we rely on the fact that chains become bisimilar after being cut certain way. This cannot be guaranteed in the presence of memory.

Taking into account that all of APAL, GAL and CAL are undecidable [4], finding expressive decidable fragments is an interesting avenue of further research. One way to go about this is by restricting the range of quantification. APAL with boolean quantification and its expressivity was studied in [17]; APAL with the quantification over positive (universal) fragment of EL, wherein the negation appears only in front of propositional variables, was presented in [18], and the expressivity of other versions of APAL was discussed in [19].

## Acknowledgements

We would like to thank anonymous referees for this special issue and the reviewers of [22] for their comments and suggestions. Also, thank you to Alexandru Baltag for the inspiring discussion at DaLí 2020.

## References

[1] T. Ågotnes, N. Alechina and R. Galimullin. Logics with group announcements and distributed knowledge: Completeness and expressive power. *Journal of Logic, Language and Information*, **31**, 141–166, 2022.

[2] T. Ågotnes, P. Balbiani, H. van Ditmarsch and P. Seban. Group announcement logic. *Journal of Applied Logic*, **8**, 62–81, 2010.

[3] T. Ågotnes and H. van Ditmarsch. Coalitions and announcements. In *Proceedings of the 7th AAMAS*, L. Padgham, D. C. Parkes, J. P. Müller and S. Parsons, eds, pp. 673–680. IFAAMAS, 2008.

[4] T. Ågotnes, H. van Ditmarsch and T. French. The undecidability of quantified announcements. *Studia Logica*, **104**, 597–640, 2016.

[5] R. Alur, T. A. Henzinger and O. Kupferman. Alternating-time temporal logic. *Journal of the ACM*, **49**, 672–713, 2002.

[6] P. Balbiani, A. Baltag, H. van Ditmarsch, A. Herzig, T. Hoshi and T. de Lima. Knowable' as 'known after an announcement. *Review of Symbolic Logic*, **1**, 305–334, 2008.

[7] P. Balbiani, H. van Ditmarsch and A. Herzig. Before announcement. In *Proceedings of the 11th AiML*, L. D. Beklemishev, S. Demri and A. Maté, eds, pp. 58–77. College Publications, 2016.

[8] A. Baltag, L. S. Moss and S. Solecki. The logic of public announcements, common knowledge, and private suspicions. In *Proceedings of the 7th TARK*, I. Gilboa, ed., pp. 43–56. Morgan Kaufmann, 1998.

[9] A. Baltag, A. Özgün and A. L. V. Sandoval. APAL with memory is better. In *Proceedings of the 25th WoLLIC*, L. S. Moss, R. J. G. B. de Queiroz and M. Martínez, eds. Vol. 10944 of LNCS, pp. 106–129. Springer, 2018.

[10] A. Baltag, A. Özgün and A. L. V. Sandoval. Arbitrary public announcement logic with memory. *Journal of Philosophical Logic*, 2022. https://doi.org/10.1007/s10992-022-09664-6.

[11] J. van Benthem. *Logic in Games*. MIT Press, 2014.

[12] J. van Benthem, J. Gerbrandy, T. Hoshi and E. Pacuit. Merging frameworks for interaction. *Journal of Philosophical Logic*, **38**, 491–526, 2009.

[13] P. Blackburn, M. de Rijke and Y. Venema. *Modal Logic*. Vol. 53 of Cambridge Tracts in Theoretical Computer Science. CUP, 2001.
[14] L. Bozzelli, H. van Ditmarsch, T. French, J. Hales and S. Pinchinat. Refinement modal logic. *Information and Computation*, **239**, 303–339, 2014.

[15] H. van Ditmarsch. Quantifying notes. In *Proceedings of the 19th WoLLIC*, C.-H. L. Ong and R. J. G. B. de Queiroz, eds. Vol. 7456 of LNCS, pp. 89–109. Springer, 2012.

[16] H. van Ditmarsch. To be announced, 2022. CoRR, abs/2004.05802v3.

[17] H. van Ditmarsch and T. French. Quantifying over boolean announcements. *Logical Methods in Computer Science*, **18**, 20:1–20:22, 2022.

[18] H. van Ditmarsch, T. French and J. Hales. Positive announcements. *Studia Logica*, **109**, 639–681, 2021.

[19] H. van Ditmarsch, M. Liu, L. B. Kuijer and I. Sedlár. Expressivity of some versions of APAL. In *Proceedings of the 3rd DaLi*, M. A. Martins and I. Sedlár, eds. Vol. 12569 of LNCS, pp. 120–136. Springer, 2020.

[20] H. van Ditmarsch, W. van der Hoek and B. Kooi. *Dynamic Epistemic Logic*. Vol. 337 of Synthese Library. Springer, 2008.

[21] H. van Ditmarsch, W. van der Hoek and J. Ruan. Connecting dynamic epistemic and temporal epistemic logics. *Logic Journal of the IGPL*, **21**, 380–403, 2013.

[22] T. French, R. Galimullin, H. van Ditmarsch and N. Alechina. Groups versus coalitions: on the relative expressivity of GAL and CAL. In *Proceedings of the 18th AAMAS*, E. Elkind, M. Veloso, N. Agmon and M. E. Taylor, eds, pp. 953–961. IFAAMAS, 2019.

[23] R. Galimullin. Coalition and relativised group announcement logic. *Journal of Logic, Language and Information*, **30**, 451–489, 2021.

[24] R. Galimullin and T. Ågotnes. Quantified announcements and common knowledge. In *Proceedings of the 20th AAMAS*, F. Dignum, A. Lomuscio, U. Endriss and A. Nowé, eds, pp. 528–536. IFAAMAS, 2021.

[25] R. Galimullin and N. Alechina. Coalition and group announcement logic. In *Proceedings of the 16th TARK*, J. Lang, ed. Vol. 251 of EPTCS, pp. 207–220. Open Publishing Association, 2017.

[26] V. Goranko and M. Otto. Model theory of modal logic. In *Handbook of Modal Logic*, P. Blackburn, J. van Benthem and F. Wolter, eds. Vol. 3 of Studies in Logic and Practical Reasoning, pp. 249–329. Elsevier, 2007.

[27] J. Hintikka. *Knowledge and Belief*. Cornell University Press, 1962.

[28] W. van der Hoek, W. Jamroga and M. J. Wooldridge. A logic for strategic reasoning. In *Proceedings of the 4th AAMAS*, F. Dignum, V. Dignum, S. Koenig, S. Kraus, M. P. Singh and M. J. Wooldridge, eds, pp. 157–164. ACM, 2005.

[29] J. F. Horty. *Agency and Deontic Logic*. OUP, 2001.

[30] B. Kooi. Expressivity and completeness for public update logics via reduction axioms. *Journal of Applied Non-Classical Logics*, **17**, 231–253, 2007.

[31] L. S. Moss. Dynamic epistemic logic. In *Handbook of Epistemic Logic*, H. van Ditmarsch, W. van der Hoek, J. Y. Halpern and B. Kooi, eds, pp. 261–312. College Publications, 2015.

[32] A. Perea. *Epistemic Game Theory*. CUP, 2012.

[33] J. Plaza. Logics of public communications. *Synthese*, **158**, 165–179, 2007.

[34] J. Sack. *Adding Temporal Logic to Dynamic Epistemic Logic*. PhD Thesis, Indiana University, Bloomington, USA, 2007.

[35] J. Sack. Temporal languages for epistemic programs. *Journal of Logic, Language and Information*, **17**, 183–216, 2008.

[36] J. Sack. Logic for update products and steps into the past. *Annals of Pure and Applied Logic*, **161**, 1431–1461, 2010.
<figure><img src="image_20.png" /><figcaption>FIGURE A.1. Models (from left to right) $M_s^{\{s,t\}}$, $M_s^{\{s\}}$, $M_t^{\{s,t\}}$ and $M_t^{\{t\}}$.</figcaption></figure>

<figure><img src="image_21.png" /><figcaption>FIGURE A.2. Formula game for $[p] \diamond_a \neg p$ over $M_s$.</figcaption></figure>

## A Examples of formula games

Consider model $M$ and all its pointed submodels in Figure A.1 as an example. The set of pointed submodels of $M$ is $\{M_s^{\{s,t\}}, M_s^{\{s\}}, M_t^{\{s,t\}}, M_t^{\{t\}}\}$, and agent $b$'s relation is identity. The formula game for $[p] \diamond_a \neg p$ is presented in Figure A.2, and the formula game for $\{[b]\] \diamond_a p$ is partially shown in Figure A.3.

We have that $M_s \not\models [p] \diamond_a \neg p$ and $M_s \models \{[b]\] \diamond_a p$. Indeed, in Figure A.2 the $\exists$-player does not have a winning strategy, and in Figure A.3, she does (noting that none of $a$'s announcements modify the original model).
<figure><img src="image_22.png" /><figcaption>FIGURE A.3. Formula game for $({\{b\}\}}\square_a p$ over $M_s$.</figcaption></figure>