To be announced

Hans van Ditmarsch

► To cite this version:

Hans van Ditmarsch. To be announced. Information and Computation, 2023, 292, pp.105026. 10.1016/j.ic.2023.105026. hal-04237920

HAL Id: hal-04237920

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

Submitted on 31 Mar 2025

**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>
# To Be Announced

Hans van Ditmarsch*

## Abstract

In this survey we review dynamic epistemic logics with modalities for quantification over information change. Of such logics we present complete axiomatizations, focussing on axioms involving the interaction between knowledge and such quantifiers, we report on their relative expressivity, on decidability and on the complexity of model checking and satisfiability, and on applications. We focus on open problems and new directions for research.

## 1 Introduction

*Truthful public announcement* is the misnomer of the year. Which year? Not the year 1989, the publication of Jan Plaza's 'Logics of public communications' [114]. Plaza does not use 'announcement'. Not the year 1998 either, the publication of Alexandru Baltag et al.'s 'The logic of public announcements (...) ' [30], as there are prior occurrences such as in Jelle Gerbrandy's [79] from 1997. Whereas in 1986, before [114], Yoram Moses et al.'s [106] uses 'announcement' (possibly, because the statements made by the Queen of Mamajorca are announcements by virtue of her being a queen), but not 'public' nor 'truthful'. So in the end, it is not known which year.

*Truthful* is a misnomer, because a statement may be truthful (what you *believe* to be true, a subjective criterion) but not true (an objective criterion). Only truth is formally required. The twain meet because announcements are assumed to be made by an omniscient and benevolent agent, for whom being truthful is the same as saying the truth, and who will not say what she does not know to be true. More down to earth: the listener assumes that the speaker wants to inform (is truthful) and is also correct (says the truth).

*Announcement* is a misnomer, because the observed information may be heard as well as seen (the light is on, or off). Such forms of observation are also modelled as an announcement in the logics that we deal with in this contribution. So it need not be a real announcement, which is presumably a speech act. There may not be an announcer anyway, in the sense of an agent modelled in a system. The source of the new information is typically assumed to be anonymous, whereas an announcement of a proposition by an agent modelled in the system is formalized as 'the agent knows the proposition'.

<footnote>*University of Toulouse, CNRS, IRIT, France.</footnote>
*Public* is, after all, not a misnomer. The new information is assumed to be received synchronously. That is a backdoor towards making ‘announcement’ acceptable terminology: ‘announcement’ carries the legal sense that all are supposed to have heard, and liable for the consequences even if they did not. Announcements tend to be public by definition.

We will often omit ‘truthful’ from ‘truthful public announcement’. Untruthful announcements play no role in this survey. Public announcements have also been called *revelations*, a very suitable name but that did not stick (unlike in game theory and mechanism design). It is on the same delightfully pretentious scale as calling a state a *world*. And public announcements have been called *public events*, another suitable name that might or might not stick but so far survives in the community. Or public actions, which carries a notion of agency. Personally, I like *public observation*, precisely as it lacks agency. Either way, it always concerns a true proposition that is simultaneously or synchronously observed by a set of agents and as a consequence of which they adjust their knowledge bases, they update what they know to be true.

*Public announcement logic* (PAL) [114] is an extension of epistemic logic, the logic of knowledge. Let us survey those origins. Jaakko Hintikka proposed the modal logic of knowledge to give a relational semantics for the perceived properties of knowledge, namely that what you know is true, that you know what you know, and that you know what you don't know [89]. He compares these with the properties of other epistemic notions such as belief (you may believe something even when it is false; in this survey we focus on knowledge). Already in [89] the analysis of Moorean phenomena [105] played an important role: you cannot be informed that you are ignorant of a (true) fact without ‘losing’ that ignorance: you cannot know that some fact *p* is true and that you don’t know this. This is inconsistent in a single-agent logic of knowledge. In a multi-agent logic of knowledge similar phenomena are not so paradoxical: there is no issue with *me* knowing that *p* is true and that *you* don’t know this.

Further developments involved on the one hand group epistemic notions such as common knowledge [23, 103] and distributed knowledge [88], topics that we will largely bypass in this contribution.

On the other hand, it involved dynamics of knowledge: the multi-agent logic of knowledge led to increased interest in the analysis of agents informing each other of their ignorance and knowledge, often inspired by logic puzzles [106, 103]. This culminated in the already mentioned public announcement logic, wherein such informative actions (called public communications in [114]) became full members of the logical language besides the knowledge modalities. ‘Culminated’ is attributed in retrospect, as the importance of this somewhat informal publication only increased over the years. There were also parallel developments of dynamic but not epistemic logics of information change such as [161, 121].

*Action model logic* (AML) [30] provided a generalization of knowledge dynamics from public information change to non-public or untruthful information change (also known as *epistemic actions*), such as private or secret announcements to some agents while other agents only partially observe that. Parallel, now lesser known, developments were [79, 134].

A different direction of generalizing PAL is to consider quantification over announcements. Arbitrary public announcement logic APAL [25] contains a construct that can be
paraphrased as 'there is a truthful public announcement after which proposition $\varphi$ is true'. If I, a poor student, am uncertain about the exam result (pass $p$ or fail $\neg p$) but you, the examiner, know that I passed, there is a truthful announcement after which I know that $p$, namely you informing me that $p$ is true. You can, so to speak, consider in your mind all possible true announcements and pick the one that ensures that I know $p$ afterwards. That is then to be announced: the announcement 'the examiner knows that $p$' results in (realizes) the epistemic goal 'the student knows whether $p$'. This is a very simple example. But as one cannot always make a proposition true by announcing it (we recall Moorean phenomena, such as announcing 'p is true and you do not know it'), much more complex settings are conceivable.

*To be announced* is what you have to say in order to achieve an epistemic goal. It is the question whether there is an announcement in order to realize that goal formula. In modal logics, this announcement may be very different from that goal. This is therefore a non-trivial problem, and the quantification involved seems worthy of investigation.

The logic APAL was rooted in various traditions, both in philosophy and in computer science. It has roots in knowability [66], by way of [124], but also in propositional quantification [63], by way of [90, 67]. All of these involve quantifying over information change, however not in a dynamic epistemic setting of which the public announcement is the typical example, as we will explain later. However, even in that setting there are many other ways to quantify over information change than in APAL, both over public and over non-public information change, and that can still be seen as announcing something, even when not publicly. Let us contrast the APAL quantifier with two other quantifiers among many presented in this survey (where $\varphi$ is a formula and $G$ a subset of the set of all agents).

1. There is a public announcement after which $\varphi$ [25].

2. There is a public announcement by the agents in group $G$ after which $\varphi$ [3].

3. There is an epistemic action (such as a private announcement) after which $\varphi$ [83];

*Item 1 is the APAL quantifier.*

*Item 2 is a restriction of the APAL quantifier.* Quantifying over announcements involving a group of agents facilitates the formalization of notions of ability and agency in dynamic epistemic logic. For example, the group $G$ may consist of the principals in a security protocol sending and receiving messages to and from each other, in the presence of one or multiple eavesdroppers possibly intercepting all messages, so that such messages should be considered public announcements. Correctly modelling messages *known* by agents requires to carefully distinguish true announcements from truthful announcements, to which we will later pay detailed attention.

*Item 3 generalizes the APAL quantifier.* By epistemic or informative action we mean some event that changes the knowledge of beliefs of agents. A public announcement is an epistemic action, but epistemic actions also include private announcements: also then, there is something to be announced, but the announcement is not observed by all agents in the same way. A typical example is that of a player showing a card to another player
while the remaining players observe the interaction but cannot see which card has been shown [135]. Which is another example of an ‘announcement’ in the technical sense of this paper that does not involve anything being said.<fnref n="1" /> It involves other agents observing the informative event in different ways. Epistemic actions can be represented as the already mentioned action models, but also in other ways presented in this survey: as *arrow updates* [95, 96, 156], and as the *refinements* of [83, 45]. In all such cases, quantifying over epistemic actions comes with different properties.

To determine what is to be announced in order to make $\varphi$ true, is to synthesize a plan to realize goal $\varphi$. There is therefore a strong relation between having quantifiers over information change in the logical language on one side, and performing epistemic planning [40] on the other side, which is done in an off-line, meta-level way: there is a plan to realize an epistemic goal $\varphi$ if the search tree that connects information states by permitted actions has a leaf satisfying the goal formula. There are also differences. The goal $\varphi$ in epistemic planning is typically an epistemic formula without quantifiers. But a formula $\varphi$ in a logical language with quantifiers may contain many such quantifiers, each posing a planning problem. We can expect a difference in complexities of decision problems.

For all dynamic epistemic logics in this survey we focus on complete axiomatizations, decidability of satisfiability, expressivity, to a lesser extent also on the complexity of model checking and (decidable) satisfiability, and last but not least we focus on applications. Applications can be found in multi-agent system analysis, in security protocols, in gossip protocols, and in epistemic planning on specific domains. All these and more will be discussed in detail. We list many open problems but also completely new directions for research.

In this survey we wish to address both the informed reader in modal logics, such as a master or doctoral student in logic, computer science, or artificial intelligence, as well as the expert in dynamic epistemic logic. For the benefit of the former we start the survey with a self-contained introduction in public announcement logic and action model logic. For the benefit of the latter we carefully list the open problems within well-defined subjects and that build on foundations of established results. Either way, we wish to share with the readers of all backgrounds our enthusiasm for the topic and its further development, and thank them for any moment of their time they choose to spend on the survey.

**Outline** We close the introductory section with an outline of the content. Section 2 provides the technical background on public announcement logic and on action model logic. Section 3 is on arbitrary public announcement logic and its variations. Section 4 is on group announcement logic and coalition announcement logic. These are variations of arbitrary public announcement logic modelling aspects of agency, ability or strategy. Section 5 is on quantification in action model logic, Section 6 is on quantification in arrow update logics, and Section 7 is on refinement modal logics. The logics in the Sections 5,

<footnote n="1">¹If we replace ‘showing a card’ such that the others cannot see, by ‘whispering the name of the card’ such that the others cannot hear, after first having publicly announced to all ‘I am now going to whisper the name of a card I have to my neighbour’, it is again an announcement wherein something is said.</footnote>
6, and 7 all quantify over arbitrary, not necessarily public, information change. Sections 8 and 9 are more exploratory in character than the other sections in this survey: they point towards directions for novel research and are less a survey of work already done. Section 8 is on iterated information change, factual change, group epistemic notions, and epistemic planning. These topics are normally considered in dynamic epistemic logics, but play a minor role in this survey on quantification. Section 9 is on so-called relation-changing modal logics. Such logics are not normally considered dynamic epistemic logics, but there are most relevant relations to quantification.

## 2 Dynamic epistemic logic

In this section we present the technical prerequisites of certain basic dynamic epistemic logics before plunging into extensions of such logics with quantifiers over information change. We will also include intuitive motivations and examples, in order to make the material more accessible and to keep it lightweight. Readers familiar with such basics may wish to skip the section. We present multi-agent epistemic logic, on the general level of a multi-modal logic [89], as well as public announcement logic [114] and action model logic [30]. Prerequisites for arrow update logic [95] are in Section 6.

The language, structures, and semantics are as follows.

**Languages** Given a non-empty countable (finite or infinite) set of propositional variables (atoms) P and a non-empty finite set of agents A, we consider four different basic logical languages that we will later expand with quantifiers. The elements of the language are the formulas.

$$ 
\begin{align*}
\mathcal{L}(\emptyset) &\ni \varphi ::= p \mid \neg\varphi \mid (\varphi \land \varphi) \\
\mathcal{L}(\diamond) &\ni \varphi ::= p \mid \neg\varphi \mid (\varphi \land \varphi) \mid \diamond_a \varphi \\
\mathcal{L}(\diamond, !) &\ni \varphi ::= p \mid \neg\varphi \mid (\varphi \land \varphi) \mid \diamond_a \varphi \mid \langle\varphi\rangle\varphi \\
\mathcal{L}(\diamond, \otimes) &\ni \varphi ::= p \mid \neg\varphi \mid (\varphi \land \varphi) \mid \diamond_a \varphi \mid \langle E_e \rangle\varphi
\end{align*}
$$

where $p \in P$, $a \in A$, and where $E_e$ is a finite pointed action model only explained and defined further below. Other propositional connectives are defined by abbreviation and we also define $\Box_a\varphi$ by abbreviation as $\neg\Diamond_a\neg\varphi$ and similarly $[\varphi]\psi$ and $[E_e]\psi$. For $\Diamond_a\varphi$ we read ‘agent a considers $\varphi$ possible’ and for $\Box_a\varphi$, ‘agent a knows $\varphi$’ (in other epistemic settings this may mean ‘agent a believes $\varphi$’). If $|A| = 1$ we may write $\Box\varphi$ and $\Diamond\varphi$ instead of $\Box_a\varphi$ and $\Diamond_a\varphi$. For $\langle\varphi\rangle\psi$ we read ‘$(\varphi$ is true and) after (truthful) public announcement of $\varphi$, $\psi$ (is true)’’. In the literature, formulas $[\varphi]\psi$ and $\langle\varphi\rangle\psi$ are often written as $[!\varphi]\psi$ and $\langle!\varphi\rangle\psi$. This explains the ! in the language definition (and later, in the language extended with quantification over announcements).

Given a formula $\varphi$, $v(\varphi)$ is the set of propositional variables occurring in $\varphi$, and $d(\varphi)$ is the modal depth or $\Box$-depth of $\varphi$ (the maximum stack of modalities in a formula). The definition of $\Box$-depth is: $d(p) = 0$, $d(\neg\varphi) = d(\varphi)$, $d(\varphi \land \psi) = \max\{d(\varphi), d(\psi)\}$, $d(\Diamond_a\varphi) = d(\varphi) + 1$, $d(\langle\varphi\rangle\psi) = d(\varphi) + d(\psi)$. The clause for $\langle E_e \rangle\varphi$ will be given later. The possibly surprising difference between the clause for conjunction, which takes the maximum
of the modal depth of both arguments, and the clause for announcement, which takes their sum, is that the latter is equivalent to a formula with a stack of modalities of the length of that sum (see e.g. [143]).

**Structures** An epistemic model (or ‘Kripke model’, or just ‘model’) $M = (S, R, V)$ consists of a non-empty domain $S$ of states (or ‘worlds’; the domain is also denoted $\mathcal{D}(M)$), an accessibility function $R : A \to \mathcal{P}(S \times S)$, where each $R(a)$ is an accessibility relation, and a valuation $V : P \to \mathcal{P}(S)$, where each $V(p)$ represents the set of states where $p$ is true. For $R(a)$ we write $R_a$, and for $(s, t) \in R_a$ we may write $R_a(s, t)$ or $R_{ast}$. A pair $(S, R)$ is called a *frame*. For $s \in S$, a pair $(M, s)$, for which we write $M_s$, is a *pointed (epistemic) model* (often also simply called model — the context should disambiguate usage). We will occasionally employ *multi-pointed models* $M_T$ where $T \subseteq S$. The model class without any restrictions is $\mathcal{K}$. The class of models where all accessibility relations are equivalence relations is $\mathcal{S}$. If $R_a$ is an equivalence relation we write $s \sim_a t$ instead of $R_{ast}$, and the relation is then called *indistinguishability relation*.

Let models $M = (S, R, V)$ and $M' = (S', R', V')$ be given. A non-empty relation $Z \subseteq S \times S'$ is a *bisimulation* between $M$ and $M'$, notation $Z : M \simeq M'$, if for all pairs $(s, s') \in Z$ ($Zss'$) and $a \in A$:

**atoms** $s \in V(p)$ iff $s' \in V'(p)$ for all $p \in P$;

**forth** if $R_{ast}$, then there is a $t' \in S'$ such that $R'_a s' t'$ and $Ztt'$;

**back** if $R'_a s' t'$, then there is a $t \in S$ such that $R_{ast}$ and $Ztt'$.

We write $M \simeq M'$ if there is a bisimulation between $M$ and $M'$, and we write $M_s \simeq M_{s'}$ if there is a bisimulation between $M$ and $M'$ containing pair $(s, s')$.

Similarly, a *simulation* satisfies **atoms** and **forth**, where we write $M \preceq M'$ if there is a simulation between $M$ and $M'$, and $M_s \preceq M_{s'}$ if it contains pair $(s, s')$; whereas its dual, the *refinement*, satisfies **atoms** and **back**, and where we write $M \succeq M'$ if there exists a refinement between $M$ and $M'$, and $M_s \succeq M_{s'}$ if it contains pair $(s, s')$. Further, if $M \succeq M'$ the model $M'$ is called a *refinement* of $M$ as well. It is sometimes confusing that in the literature the term ‘refinement’ denotes both the refinement relation linking $M$ and $M'$, and the refined model $M'$.

A (to $Q$) *restricted bisimulation* $Z^Q$ is a bisimulation that satisfies **atoms** for all variables $Q \subseteq P$, in notation $M \simeq^Q M'$. A (by $n$) *bounded bisimulation* $Z^n$ satisfies **forth** and **back** up to depth $n \in \mathbb{N}$. Formally we define this as a set $Z^0 \supseteq Z^1 \supseteq \dots \supseteq Z^n$ of $i$-bisimulations for $0 \le i \le n$ as follows (see also [38]). Relation $Z^0$ merely satisfies **atoms**, and for all $Z^{n+1}ss'$ and $a \in A$:

**atoms** $s \in V(p)$ iff $s' \in V'(p)$ for all $p \in P$;

**forth**-$(n+1)$ if $R_{ast}$, then there is a $t' \in S'$ such that $R'_a s' t'$ and $Z^{n}tt'$;

**back**-$(n+1)$ if $R'_a s' t'$, then there is a $t \in S$ such that $R_{ast}$ and $Z^{n}tt'$.
We write $M_s \simeq^n M'_{s'}$ for $n$-bisimilar models $M_s$ and $M'_{s'}$. Bounded bisimulations are used to compare models $M_s$ and $M'_{s'}$ up to a depth $n$ from the respective points $s$ and $s'$.

**Semantics of PAL** We first give the semantics for truthful public announcement logic (PAL) [114]. Assume an epistemic model $M = (S, R, V)$, and let $s \in S$. We define $M_s \models \varphi$ (for: $M_s$ satisfies $\varphi$, or $\varphi$ is true in $M_s$) by induction.

$$
\begin{array}{lcll}
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 \wedge \psi & \text{iff} & M_s \models \varphi \text{ and } M_s \models \psi \\
M_s \models \Diamond_a \varphi & \text{iff} & \text{there is a } t \in S \text{ such that } R_{ast} \text{ and } M_t \models \varphi \\
M_s \models \langle \psi \rangle \varphi & \text{iff} & M_s \models \psi \text{ and } (M|\psi)_s \models \varphi
\end{array}
$$

where $M|\psi := (S', R', V')$ such that $S' := \{s \in S \mid M_s \models \psi\}$, $R'_a := R_a \cap (S' \times S')$, and $V'(p) := V(p) \cap S'$. A formula $\varphi$ is valid on $M$, notation $M \models \varphi$, if for all states $s$ in the domain of $M$, $M_s \models \varphi$, and a formula is valid, notation $\models \varphi$, if it is valid on all models $M$. Expression $M_T \models \varphi$, where $M_T$ is a multi-pointed model, abbreviates that $M_t \models \varphi$ for all $t \in T$.

The set $S' := \{s \in S \mid M_s \models \psi\}$ above is called the *extension* or *denotation* of $\psi$ in model $M$, and the model $M|\psi$ is called the *restriction* of $M$ to $\psi$, or, alternatively, we call $M|S'$ the restriction of $M$ to $S'$.

Given $M = (S, R, V)$, formula $\varphi$ is distinguishing between $T \subseteq S$ and $S \setminus T$ (or: $\varphi$ is distinguishing for $T$) if for all $t \in T$, $M_t \models \varphi$, and for all $t \notin T$, $M_t \not\models \varphi$. A distinguishing formula for $s \in S$ is therefore distinguishing between $\{s\}$ and $S \setminus \{s\}$.

**Example 1** Agent $a$ is uncertain about $p$. After announcement $p$, she knows that $p$. Consider a two-state model $M$ wherein she cannot distinguish a state 1 where $p$ is true from a state 0 where $p$ is false. We have that $M_1 \models \langle p \rangle \Box_a p$ because $M_1 \models p$ and $(M|p)_1 \models \Box_a p$, where the latter is true because $(M|p)_1 \models p$, and because 1 is the only accessible state.

We can visualize such models in different ways. As this will happen regularly in this survey we had better be very explicit on our visual conventions. Either we depict it with all pairs in the relation as arrows, as below on the left, or, for $S^5$ models with equivalence relations, we only link ('relate') indistinguishable states, as below on the right. When linking states we assume reflexivity, symmetry and transitivity of the relation. The assumption of transitivity is not used in the example below but in other examples in this survey. We underline the actual state, that is, state 1 in this example. States where $p$ is true are typically named 1 and states where $p$ is false are typically named 0. The update relation between the respective models is visualized by $\Rightarrow$. It is labelled with the formula of the announcement inducing the update.

$$ a \underset{a}{\rightleftarrows} 0 \underset{a}{\rightleftarrows} 1 \underset{p}{\rightleftarrows} 1 \underset{a}{\rightleftarrows} 0 $$
Note that we also have $M_1 \models p \wedge \neg \Box_a p$. Announcing this, results in the same model restriction to the 1-state. As $\Box_a p$ implies $\neg p \vee \Box_a p$, which is equivalent to $\neg (p \wedge \neg \Box_a p)$, we therefore have that $M_1 \models \langle p \wedge \neg \Box_a p \rangle \neg (p \wedge \neg \Box_a p)$: after the announcement $p \wedge \neg \Box_a p$ this formula has become false. This is an example of a Moorean phenomenon.

**Axiomatization of PAL** The axiomatization of minimal modal logic K contains axiom $\Box_a(\varphi \rightarrow \psi) \rightarrow \Box_a\varphi \rightarrow \Box_a\psi$ and derivation rule 'From $\varphi$ infer $\Box_a\varphi$' (apart from propositional features). The modal logic S5 additionally contains, for all agents $a$, axioms $\Box_a\varphi \rightarrow \varphi$, $\Box_a\varphi \rightarrow \Box_a\Box_a\varphi$, and $\neg\Box_a\varphi \rightarrow \Box_a\neg\Box_a\varphi$. There are no multi-agent interaction axioms.

The axiomatization of PAL extends that of K or S5 (or yet other modal logics) with so-called reduction axioms for the announcement. It follows a pattern that is common in dynamic epistemic logics and that we therefore explain in some detail. The reduction axioms for the announcement are validities that have the shape of equivalences. There is one for each main logical connective of the formula bound by the announcement.

$$ \begin{array}{lcl} [\psi]p & \leftrightarrow & (\psi \rightarrow p) \\ [\psi]\neg\varphi & \leftrightarrow & (\psi \rightarrow \neg[\psi]\varphi) \\ [\psi](\varphi \wedge \chi) & \leftrightarrow & ([\psi]\varphi \wedge [\psi]\chi) \\ [\psi]\Box_a\varphi & \leftrightarrow & (\psi \rightarrow \Box_a[\psi]\varphi) \\ [\psi][\varphi]\chi & \leftrightarrow & [\psi \wedge [\psi]\varphi]\chi \end{array} $$

Strictly, expressions such as $[\psi](\varphi \wedge \chi) \leftrightarrow ([\psi]\varphi \wedge [\psi]\chi)$ are not axioms but are *axiom schemes*, whereas for example the instantiation $[p](q \wedge \Box_a p) \leftrightarrow ([p]q \wedge [p]\Box_a p)$ of that schema is an axiom. The difference is relevant because the logic PAL (as well as most other dynamic epistemic logics in this survey) does not have the *substitution property* that we can replace the occurrence of an atom in a validity by any formula. For example, $[p]p$ is valid but $[p \wedge \neg \Box_a p](p \wedge \neg \Box_a p)$ is invalid. The shape of the axiom $[\psi]p \leftrightarrow (\psi \rightarrow p)$ is a giveaway for this lacking feature: it contains an atom as well as an arbitrary formula. That reduction strictly depends on the bound formula being an atom and not just any formula. Whereas in a logic with the substitution property, such as K and S5, atoms can also be any formula.

In other dynamic epistemic logics, many of these reduction axioms are very similar, except the one for the interaction between the update modality (here the announcement) and knowledge. In the continuation we focus on such interaction between update and knowledge.

Except for the first one, the reduction axioms for the announcement all have the shape $[\psi]\mathbf{this} \leftrightarrow \mathbf{that}$ where this is not a subformula of that, but where that contains a subformula $[\psi]\mathbf{other}$ where other is a subformula of this. Roughly, that feature is what makes it possible to *reduce* (rewrite) a formula with announcements to an equivalent formula without announcements. Let us give an example:

$$ \begin{array}{l@{\qquad}l} [p \wedge \neg \Box_a p] \Box_a p, & \text{iff} \\ (p \wedge \neg \Box_a p) \rightarrow \Box_a [p \wedge \neg \Box_a p] p, & \text{iff} \\ (p \wedge \neg \Box_a p) \rightarrow \Box_a (p \wedge \neg \Box_a p \rightarrow p). & \text{iff} \end{array} $$
Note that the last formula is equivalent to $p \wedge \neg \Box_a p$. In two steps the reduction terminates. The final step is when an announcement binds an atom, as the announcement modality will then have ‘disappeared’ on the righthand side. In general, to show that such a rewrite procedure terminates one needs to associate a weight or measure (often a natural number) to a formula and prove that the weight of $[\psi]$**this** is larger than the weight of **that**. Similar reductions exist for many of the dynamic epistemic logics we present in this survey. Each logic may require a different formula weight in order to prove termination of the reduction.

**Expressivity** Given two logics $L_1$ and $L_2$ defined over the same class of models, $L_1$ is at least as expressive as $L_2$, if for every formula $\varphi_2$ in the language of $L_2$ there is a formula $\varphi_1$ in the language of $L_1$ such that $\varphi_1$ is satisfied by precisely the class of pointed models that satisfy $\varphi_2$. If $L_1$ is at least as expressive as $L_2$ and $L_2$ is at least as expressive as $L_1$ then $L_1$ and $L_2$ are equally expressive (or: $L_1$ is as expressive as $L_2$). If $L_1$ is at least as expressive as $L_2$ and $L_2$ is not at least as expressive as $L_1$ then $L_1$ is more expressive than $L_2$.

By way of reductions as the above example, it can be shown that every formula with announcements is equivalent to a formula without announcements, and therefore public announcement logic PAL is as expressive as multi-agent epistemic logic K (with respect to model class $\mathcal{K}$) and as expressive as the logic S5 (with respect to model class $\mathcal{S}5$). The announcement modality is pushed ever more inward until it gets eliminated by an application of the first axiom $[\psi]p \leftrightarrow (\psi \rightarrow p)$ above, where on the right-hand side of the equation there is one less announcement modality than on the left-hand side. We now proceed to eliminate the next announcement modality by such reductions, and so on, until there are none left. See [94] for a general approach for dynamic modalities.

**Action models** An action model [30] (or event model) is a structure like a Kripke model but with a precondition function instead of a valuation function. An action model $E = (S, \mathbb{R}, \text{pre})$ consists of a domain $S$ of actions, an accessibility function $R : A \to \mathcal{P}(S \times S)$, where each $R_a$ is an accessibility relation, and a precondition function $\text{pre} : S \to \mathcal{L}$, where $\mathcal{L}$ is a logical language — which in our case would typically be the epistemic language $\mathcal{L}(\diamond)$; however, there is also a recursive way to define a language with action model modalities, that we present below. A pointed action model $E_e$, in other words a pair $(E, e)$, where $e \in S$, is an epistemic action. Just as for Kripke models, we also permit multi-pointed action models $E_F$ where $F \subseteq S$. We will also use ‘epistemic action’ to denote any other information changing update.

Performing an epistemic action that is a pointed action model in a pointed epistemic model involves computing the *restricted modal product* of the action model and the epistemic model. This product (also called the update product) encodes the new state of information. It is defined as follows.

Given an epistemic model $M = (S, \mathbb{R}, V)$ and an action model $E = (S, \mathbb{R}, \text{pre})$, the
updated model $(M \otimes E) = (S', R', V')$ is such that

$$ \begin{array}{lclcl} S' & = & \{(t, f) \in S \times S \mid M_t \models \mathbf{pre}(f)\} \\ ((t, f), (t', f')) & \in & R'_a & \text{iff} & R_a tt' \text{ and } R_a ff' \\ (t, f) & \in & V'(p) & \text{iff} & t \in V(p) \end{array} $$

In other words: the domain consists of the product domain, but restricted to (state, action) pairs $(t, f)$ such that $M_t \models \mathbf{pre}(f)$, i.e., such that the action can be executed in that state; an agent considers a pair $(t, f)$ possible in the update model if she considered the previous state $t$ possible and the execution of action $f$ in that state; and the valuations do not change after action execution.

A truthful public announcement $\varphi$ is a singleton action model $(\{e\}, \mathbf{R}, \mathbf{pre})$, with $\mathbf{R}_a = \{(e, e)\}$ for all $a \in A$, and $\mathbf{pre}(e) = \varphi$.

**Example 2** Consider a model wherein two agents $a, b$ are uncertain about the value of an atom $p$, and where $p$ is true. Further, consider the epistemic action representing that agent $a$ learns that $p$ is true, but that agent $b$ is uncertain whether that has happened (that is, agent $b$ considers it possible that $a$ has learnt that $p$ is true and also considers it possible that nothing has happened). The epistemic action consists of two actions that have been named after their preconditions $p$ and $\top$. They can be distinguished by agent $a$ but not by agent $b$.

$$ 0 \xrightarrow{ab} \underline{1} \otimes \underline{p} = \left. \begin{array}{c} \top \\ b \\ \hline \underline{p} \end{array} \right| \begin{array}{c} (0, \top) \xrightarrow{ab} (1, \top) \\ \underline{b} \\ \hline (1, \underline{p}) \end{array} $$

The result of executing the action is depicted on the right. The point of the updated model is the one with precondition $p$. It can only be executed in the state wherein $p$ is true. In fact, $a$ is learning that $p$, but $b$ is uncertain between that action and the 'trivial' action wherein nothing is learnt. The trivial action has precondition $\top$. The trivial action can be executed in both states of the initial model. Therefore, the updated model contains three states. Its accessibility relations are calculated from the initial epistemic model and the action model. For example, $(0, \top) \sim_b (1, p)$ because $0 \sim_b 1$ and $\top \sim_b p$. Whereas $(0, \top) \not\sim_a (1, p)$ because $\top \not\sim_a p$, even though $0 \sim_a 1$. Note that we have $(0, \top) \sim_b (1, p)$ although the $b$-link between $(0, \top)$ and $(1, p)$ is not drawn in the figure: it follows from the $b$-link drawn between $(0, \top)$ and $(1, \top)$, the $b$-link drawn between $(1, \top)$ and $(1, p)$, and the assumption of transitivity.

We have that $(1, p) \models \Box_a p \wedge \neg \Box_b \Box_a p$. Here, $(1, p) \models \neg \Box_b \Box_a p$, because $(1, p) \sim_b (1, \top)$ and $(1, \top) \not\models \Box_a p$; where the latter is because $(1, \top) \sim_a (0, \top)$ and $(0, \top) \not\models p$. Also, $(1, p) \models \Box_a p$, because only $(1, p)$ is $a$-accessible.
The composition of two action models is again an action model. The construction has the same spirit as that of updating epistemic models. Given $E = (S, R, \mathbf{pre})$ and $E' = (S', R', \mathbf{pre}')$, their composition $E'' = (S'', R'', \mathbf{pre}'')$ is defined as

$$ 
\begin{array}{lclcl}
S'' & = & S \times S' & & \\
((e, e'), (f, f')) \in R_a'' & \text{iff} & R_a e f \text{ and } R_a' e' f' & & \\
\mathbf{pre}''(e, e') & = & \mathbf{pre}(e) \wedge [E_e] \mathbf{pre}'(e') & &
\end{array}
$$

**Example 3** Let us give some examples of action model composition. We recall that a sequence of two announcements $\psi$ and $\varphi$ is again an announcement, namely that of $\psi \wedge [\psi] \varphi$. For example, if $\psi = p \wedge \neg \Box_a p$ and $\varphi = \Box_a (p \wedge q)$ we get $(p \wedge \neg \Box_a p) \wedge [p \wedge \neg \Box_a p] \Box_a (p \wedge q)$. This is equivalent to $\langle p \wedge \neg \Box_a p \rangle \Box_a (p \wedge q)$. A sequence of two announcements is typically not equivalent to their conjunction! In this case the conjunction is $(p \wedge \neg \Box_a p) \wedge \Box_a (p \wedge q)$, which is inconsistent, as from $\neg \Box_a p$ and $\Box_a p$ we derive a contradiction. Now, consider that in the presence of another agent $b$, agent $a$ was first privately informed that $p \wedge \neg \Box_a p$ and was then privately informed that $\Box_a (p \wedge q)$, while in both cases agent $b$ considered possible that nothing happened (so that we get the action model as in Example 2, only with preconditions $p \wedge \neg \Box_a p$ and $\Box_a (p \wedge q)$, respectively, instead of $p$). The composition of these two action models is a four-action action model with identity access for $a$ (who knows what it going on) and universal access for $b$ (who considers it possible that no message, one message, or two messages have arrived), and with preconditions: $\top$, $p \wedge \neg \Box_a p$, $\Box_a (p \wedge q)$, and $\langle p \wedge \neg \Box_a p \rangle \Box_a (p \wedge q)$.

**Language and semantics of AML** As already noted, the language $\mathcal{L}(\diamond, \otimes)$ of action model logic AML contains an additional inductive construct

$$ \langle E_e \rangle \varphi $$

standing for ‘there is an execution of (pointed) action model $E_e$ after which $\varphi$ (is true)’, and where it is required that the domain of $E$ is finite. This clause $\langle E_e \rangle \varphi$ is properly recursive in the formal language definition: it says that, given the (finite number) $|\mathcal{D}(E)|$ formulas that are the preconditions of $E$ (although we do not see them) and the formula $\varphi$ (that we see), also $\langle E_e \rangle \varphi$ is a formula. One should see the action model frame as the operator and all those formulas as its arguments. The set of all action model frames should then be seen as an additional parameter of the logical language, apart from the agents $A$ and the atoms $P$. As the finite pointed action model frames can be enumerated, this is a countable set.

The definition of modal depth $d(\varphi)$ should be extended to the case $\varphi = \langle E_e \rangle \psi$, namely as the sum of $d(\psi)$ and the maximum depth of the preconditions in $E$. Formally: $d(\langle E_e \rangle \psi) = d(\psi) + \max\{d(\mathbf{pre}(f)) \mid f \in S\}$, where $E = (S, R, \mathbf{pre})$.

The semantics for epistemic actions is as follows.

$$ M_s \models \langle E_e \rangle \psi \quad \text{iff} \quad M_s \models \mathbf{pre}(e) \text{ and } (M \otimes E)_{(s,e)} \models \psi $$
**Axiomatization** Action model logic has a complete Hilbert-style axiomatization with reduction axioms for the action model modalities. This is just as for public announcement logic, which is now a special case. For completeness' sake, the reduction axioms are as follows, where in the final axiom, $E''$ is the composition of $E$ and $E'$. Please note the similarity with the reductions for PAL, with the exception of the axiom for knowledge after action model execution. The axiom for knowledge after public announcement is the special case where there is only one accessible action.

$$ 
\begin{align*}
[E_e p] &\leftrightarrow (\mathbf{pre}(e) \rightarrow p) \\
[E_e] \neg \varphi &\leftrightarrow (\mathbf{pre}(e) \rightarrow \neg [E_e] \varphi) \\
[E_e](\varphi \wedge \chi) &\leftrightarrow ([E_e] \varphi \wedge [E_e] \chi) \\
[E_e] \Box_a \varphi &\leftrightarrow (\mathbf{pre}(e) \rightarrow \bigwedge_{R_a e f} \Box_a [E_f] \varphi) \\
[E_e][E_{e'}'] \chi &\leftrightarrow [E''_{(e,e')}] \chi
\end{align*}
$$

Similarly to PAL, by way of these reduction axioms, action model logic AML is shown to be as expressive as multi-agent epistemic logic K, given the model class $\mathcal{K}$. Similarly, given epistemic models and action models where all relations are equivalence relations, AML is as expressive as multi-agent S5 (see e.g. [30, 155]).

It is well-known that PAL and AML are bisimulation invariant, by which we mean that bisimilar epistemic models also satisfy the same formulas in the languages $\mathcal{L}(\diamond, !)$ and $\mathcal{L}(\diamond, \otimes)$: if $M_s \simeq M'_{s'}$, then for all formulas $\varphi$ in those languages, $M_s \models \varphi$ iff $M'_{s'} \models \varphi$. This invariance also applies to restricted bisimulation and bounded bisimulation, and the respective linguistic restrictions. All this should be considered elementary variations on the standard results from [38]. But not all this is explicit for dynamic epistemic logics. For that, see [143] for PAL and [145] for AML. A consequence is that $M_s \simeq M'_{s'}$ implies $(M|\varphi)_s \simeq (M'|\varphi)_{s'}$, where $\varphi$ is any formula true in $s$: if two models are bisimilar then also their model restrictions to the same formula. Intuitively it should be clear that this must hold, because whenever $\varphi$ is true in $M$ there must be a bisimilar state wherein it is true in $M'$ — and similarly for precondition formulas of action models.

**Arrow update logic** Another general framework for dynamic epistemic logic is arrow update logic [95], of which a generalized version has also been proposed [96] that is as expressive as action model logic. We will introduce it in Section 6 dedicated to quantification over arrow updates.

**More information** Many standard topics in dynamic epistemic logic are not dealt with in this summary technical preview, such as common knowledge, factual change, and change of belief. Comprehensive introductions to dynamic epistemic logic are [154, 155, 35, 150, 33, 107], as well as internet resources https://iep.utm.edu/dynamic-epistemic-logic/ and https://en.wikipedia.org/wiki/Dynamic_epistemic_logic.
# 3 Arbitrary announcement

## 3.1 Language and semantics

Arbitrary public announcement logic APAL [25] contains a quantifier over announcements. Its language $\mathcal{L}(\diamond, !, \langle ! \rangle)$ is obtained from $\mathcal{L}(\diamond, !)$ by adding an inductive clause $\langle ! \rangle \varphi$, where $\langle ! \rangle$ is a (APAL) quantifier. We call a formula in $\mathcal{L}(\diamond, !)$ a quantifier-free formula. Given model $M_s$ and $\langle ! \rangle \varphi \in \mathcal{L}(\diamond, !, \langle ! \rangle)$, we then define

$$M_s \models \langle ! \rangle \varphi \quad \text{iff} \quad \text{there is a quantifier-free } \psi \text{ such that } M_s \models \langle \psi \rangle \varphi$$

The formula $\psi$ is called a witness for quantifier $\langle ! \rangle$. As PAL and K are equally expressive, we may even assume that witness $\psi$ is in $\mathcal{L}(\diamond)$.

For $\langle ! \rangle \varphi$ we read 'there is an announcement after which $\varphi$ (is true)', and for $[!] \varphi$ we read 'after any/arbitrary announcement, $\varphi$ (is true)'. Implicit in both formulations is that announcements can only be made on condition that they are true. As we see from the above semantics, these paraphrases are slightly imprecise, because the announcements need to be quantifier-free formulas. Without yet other restrictions, the definition would otherwise be circular, as to determine whether $[!] \varphi$, we then would have to check the truth of $[[!] \varphi] \varphi$.

We have to expand the definition of modal depth with a clause for the quantifier: $d(\langle ! \rangle \varphi) := d(\varphi)$.

**Example 4** Given an agent $a$ who is uncertain about the truth of $p$, either a truly informative announcement $p$ or a trivial announcement $\top$ can be made. We have that $M_1 \models \langle ! \rangle \Box_a p$ because $M_1 \models \langle p \rangle \Box_a p$. On the other hand, $M_1 \models \langle ! \rangle \neg \Box_a p$ because $M_1 \models \langle \top \rangle \neg \Box_a p$. Of course we do not have $M_1 \models \langle ! \rangle (\Box_a p \wedge \neg \Box_a p)$.

$$0 \xrightarrow{a} 1 \iff 0 \xrightarrow[M]{\top} 1 \Rightarrow 1$$

## 3.2 Validities

An illustrative validity is: $\langle ! \rangle (\Box_a p \vee \Box_a \neg p)$. This formalizes that the agent $a$ can always learn the value of an atomic proposition. It is easy to see why this is valid: either $p$ is true, in which case the agent knows it after its announcement (or, in case it already knew that $p$, still knows it after its announcement), or it is false, in which case the agent knows that it is false after the announcement that $p$ is false. The argument is given in terms of the intuitions for knowledge, on $S_5$ models, but in fact applies to any $\mathcal{K}$ model. The generalization of this validity from atoms $p$ to any formula $\varphi$ is also valid, this is discussed in the paragraph on knowability, below.

Some schematic APAL validities of interest are as follows. We note that Church-Rosser only holds on class $S_5$ (see also Example 5), and that McKinsey holds on class $S_5$, where it is unclear if it also holds on class $\mathcal{K}$. Proofs of these validities can be found in [25], except
for CR, of which the proof found there is incorrect, and for which a correct proof can be
found in [143].

• $\langle ! \rangle \langle ! \rangle \varphi \rightarrow \langle ! \rangle \varphi$ (4)

This expresses that a sequence of two announcements $\psi$ and $\chi$ is again an announce-
ment, namely $\langle \psi \rangle \chi$ (or $\psi \wedge [\psi] \chi$).

• $[!]\varphi \rightarrow \varphi$ (T)

If $\varphi$ is true after any announcement, it is true after the trivial announcement, and
therefore it was already true.

• $\langle ! \rangle [!] \varphi \rightarrow [!] \langle ! \rangle \varphi$ (Church-Rosser) / CR

Given $M_s$ and announcements $\psi$ and $\chi$, there are, respectively, two consecutive an-
nouncements $\psi'$ and $\chi'$ such that the same (or a bisimilar) pointed epistemic model
results: $(M|\psi|\psi')_s \simeq (M|\chi|\chi')_s$.

• $[!]\langle!\rangle\varphi \rightarrow \langle!\rangle[!]\varphi$ (McKinsey) / MK

MK is not first-order definable, but 4 and MK together are first-order definable by
*atomicity*: $\forall x \exists y (Rxy \& (\forall z Ryz \Rightarrow y = z))$. This is a famous result in correspondence
theory [120], see also [38]. However, in our setting this $R$ is the update relation
between pointed epistemic models, where a pair consisting of $M_s$ and $(M|\psi)_s$ is in
the update relation in case $M_s \models \psi$. Atomicity then says that there is a most
informative announcement given the uncertainty specified in the above $\varphi$ occurring
in MK. In fact, the most informative announcement is that of the value of all atoms
occurring in $\varphi$ [153].

The operator $\langle!\rangle$ seems therefore to behave like the modality of the logic S4. However, this is not the case. We recall that PAL and APAL are not normal modal logics, as they do not satisfy uniform substitution. For another example, $p \rightarrow \langle!\rangle \Box_a p$ is valid but $(p \wedge \neg \Box_a p) \rightarrow \langle!\rangle \Box_a (p \wedge \neg \Box_a p)$ is invalid (see Example 1).

**Example 5** This counterexample to Church-Rosser on $\mathcal{K}$ is by Louwe Kuijer. Given a single agent, consider $M = (S, R, V)$ given by $S = \{s, t, u\}$, $R = \{(s, t), (t, t), (t, u)\}$ and $V(p) = \{s, t\}$. We now have that $M_s \models \langle!\rangle[!]\diamond\top$, with the witness being the announcement $p$ which makes $s$ and $t$ bisimilar. Yet we also have $M_s \not\models [!]\langle!\rangle\diamond\top$, since after the announcement $\Box p$ we are left with only the state $s$. As it has no successors, no further announcement can make $\diamond\top$ true. A depiction is:

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

**Knowability** The schema $\langle!\rangle\Box_a\varphi$, for 'there is an announcement after which the agent knows $\varphi$, can be seen as an interpretation of '$\varphi$ is knowable', a suggestion made by Johan van Benthem in [124]. Thus, APAL provides an actual setting to investigate Fitch's
knowability paradox [66]. Fitch addressed the question whether what is true can become known and in [66] he demonstrated that the existence of unknown truths (there is a $\varphi$ for which $\varphi \wedge \neg \Box_a \varphi$) is inconsistent with the requirement that all truths are knowable (for any $\psi$, $\psi \to \langle ! \rangle \Box_a \psi$). The inconsistency appears by substituting $p \wedge \neg \Box_a p$ for $\psi$, as follows. Let $M_s$ be a (S5) model satisfying $p \wedge \neg \Box_a p$ and towards a contradiction assume that $M_s$ also satisfies $(p \wedge \neg \Box_a p) \to \langle ! \rangle \Box_a (p \wedge \neg \Box_a p)$. Then $M_s \models \langle ! \rangle \Box_a (p \wedge \neg \Box_a p)$. Then there is a formula $\psi$ witnessing this $\langle ! \rangle$ quantifier such that $M_s \models \psi$ and $(M|\psi)_s \models \Box_a (p \wedge \neg \Box_a p)$. Now observe that $\Box_a (p \wedge \neg \Box_a p)$ is inconsistent in S5, as we can derive $\Box_a p$ and $\neg \Box_a p$ from it, and therefore $\perp$. It can therefore not be true in $(M|\psi)_s$.

An interesting APAL validity for the Fitch setting is $\langle ! \rangle (\Box_a \varphi \vee \Box_a \neg \varphi)$ [153]. This states that in APAL 'everything is knowable', meaning that for every formula we can get to know whether it is true or false.

That this is valid, is shown by announcing the value of all variables occurring in $\varphi$, and then showing that in any model $M$ with a constant valuation for those variables, for any $\psi$ only containing those variables, $M \models \psi \to \Box_a \psi$. Therefore, in particular, $M \models \varphi \to \Box_a \varphi$ and $M \models \neg \varphi \to \Box_a \neg \varphi$, from which follows $M \models \Box_a \varphi \vee \Box_a \neg \varphi$.

The result is for S5 models. It is unclear whether the results extends to model class $\mathcal{K}$.

Such knowability comes at a price: the Moore sentence $p \wedge \neg \Box_a p$ is knowable, because after being truthfully announced, agent $a$ knows that it is false, as we saw in Example 1. This seems contrary to the 'spirit' of knowability: the idea is, that you can get to know that something was true, not that it is true now.

## 3.3 Expressivity

On the class of S5 models for a single agent, APAL is as expressive as PAL, whereas for more than one agent, APAL is more expressive than PAL [25]. On class $\mathcal{K}$, single-agent APAL is also more expressive than PAL. However, as so often, the proof of that is similar to the proof of the multi-agent case on class S5.

There are two different proofs of larger expressivity. We present them in some detail, as both kinds of proof have been used to obtain expressivity results for different versions of APAL.

The APAL quantifier $\langle ! \rangle$ implicitly quantifies over *countably many atoms* and also implicitly quantifies over *arbitrarily large modal depth* (we recall that the modal depth is the largest number of stacked $\diamond$-operators — or $\Box$-operators, which does not matter for the count). These properties can be independently used to demonstrate larger expressivity of APAL. Prior to the details, let us first sketch how.

On the assumption that a particular formula $\varphi \in \mathcal{L}(\diamond, !, \langle ! \rangle)$ is equivalent to a formula $\psi \in \mathcal{L}(\diamond, !)$, we use that $\psi$ must contain a finite number of atoms, or that $\psi$ is of finite modal depth. Given that, we can choose two models that have a different value for $\varphi$ but that must have the same value for $\psi$, which is a contradiction, so that therefore such a $\psi$ cannot exist. Therefore, PAL is not at least as expressive as APAL. As $\mathcal{L}(\diamond, !) \subseteq \mathcal{L}(\diamond, !, \langle ! \rangle)$, we also trivially have that APAL is at least as expressive as PAL. Therefore, APAL is (strictly) more expressive than PAL. Such expressivity results are often shown with Ehrenfeucht-
Fraissé games [55]. The method above, however, seems suitable for quantified dynamic epistemic logics because it is succinct. And let us now give the details.

**Implicit quantification over all atoms** First, let us use the argument that $\langle ! \rangle$ quantifies over all atoms, found in [25]. For this argument to work, we need that the set of atoms is countably infinite. Consider the formula $\varphi = \langle ! \rangle (\Box_a p \wedge \neg \Box_b \Box_a p)$. Let us assume that $\varphi \in \mathcal{L}(\diamond, !, \langle ! \rangle)$ is equivalent to $\psi \in \mathcal{L}(\diamond, !)$. As the formula $\psi$ only contains a finite number of atoms, and as the set of atoms is infinite, there is an atom $q \in P$ such that $q \notin v(\psi)$. Consider the following two models for variables $p$ and $q$ (where the value of other variables does not matter, and where in $M$, the value of $q$ does not matter); 10 means that $p$ is true and $q$ is false, etcetera.

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

We now have that

$$M_1 \nvDash \langle ! \rangle (\Box_a p \wedge \neg \Box_b \Box_a p)$$

because there are only two possible model restrictions, the trivial one after which $\Box_a p$ remains false, and the restriction to the $p$-state, after which $\Box_a p$ is true but then also $\Box_b \Box_a p$.

We also have that

$$M'_{10} \models \langle ! \rangle (\Box_a p \wedge \neg \Box_b \Box_a p)$$

because

$$M'_{10} \models \langle p \lor q \rangle (\Box_a p \wedge \neg \Box_b \Box_a p)$$

as $M'| (p \lor q)$, $10 \models \Box_a p \wedge \neg \Box_b \Box_a p$.

On the other hand, $M_1 \simeq_{P \setminus \{q\}} M'_{10}$ and therefore by bisimulation invariance for PAL:

$$M_1 \models \psi \quad \text{iff} \quad M'_{10} \models \psi$$

**Implicit quantification over any finite modal depth** The other proof of the larger expressivity of APAL (originally by Barteld Kooi, but by now also found in, for example, [143]) uses that $\langle ! \rangle$ quantifies over formulas of arbitrarily large epistemic depth. This proof does not need the requirement that there are infinitely many atoms in the logical language.

Again, consider $\varphi = \langle ! \rangle (\Box_a p \wedge \neg \Box_b \Box_a p)$, and again, let us assume that $\varphi \in \mathcal{L}(\diamond, !, \langle ! \rangle)$ is equivalent to $\psi \in \mathcal{L}(\diamond, !)$. Consider the models depicted below. We abuse notation by having multiple states with the same name, namely of the value of the unique atom $p$. However, we will only evaluate formulas in the (underlined) point of any of such models, thus avoiding ambiguity.
$$
\begin{array}{l@{\qquad}l}
M_1: &
  0 \frac{a}{\phantom{0}0} \underline{1} \\
  & \simeq \\
  & 0 \frac{a}{\phantom{0}0} \underline{1} \frac{b}{\phantom{0}1} \frac{a}{\phantom{0}0} \\
  & \simeq \\
  & 0 \frac{a}{\phantom{0}0} \underline{1} \frac{b}{\phantom{0}1} \frac{a}{\phantom{0}0} \frac{b}{\phantom{0}0} \frac{a}{\phantom{0}1} \frac{b}{\phantom{0}1} \frac{a}{\phantom{0}0} \\
  & \simeq \\
M_1'': & 0 \frac{a}{\phantom{0}0} \underline{1} \frac{b}{\phantom{0}1} \frac{a}{\phantom{0}0} \dots > d(\psi) \dots \\
M_1': & 0 \frac{a}{\phantom{0}0} \underline{1} \frac{b}{\phantom{0}1} \frac{a}{\phantom{0}0} \dots > d(\psi) \dots \\
\Rightarrow & \\
(M'|\eta)_1: & \underline{1} \frac{b}{\phantom{0}1} \frac{a}{\phantom{0}0}
\end{array}
$$

First observe that $M_1$ is bisimilar to the model depicted below it, which is obtained from
taking a mirror-image copy of $M$ and pasting that to $M$ with a $b$-link. Similarly, we can
take two copies of that, such that we get the model on the next line, etc., and we get some
$M''$ where the rightmost state is more than $d(\psi)$ steps away from the underlined (actual)
$p$-state. Let now $M'$ be as this $M''$ except that in the right-most state $p$ is true. This is the
only state in $M'$ where $b$ knows that $a$ knows that $p$. Formula $\square_b\square_a p$ is a distinguishing
formula for that state. Using that, we can find a distinguishing formula for any finite subset
of the domain of $M'$ and thus there is an (unspecified but rather complex) announcement
$\eta$ after which the three states as depicted remain, such that $\langle\eta\rangle(\square_a p \wedge \neg\square_b\square_a p)$ is true in
$M'_1$, and thus

$$
M'_{1} \models \langle ! \rangle (\Box_{a} p \wedge \neg \Box_{b} \Box_{a} p)
$$

Also, as before,

$$
M_1 \models \neg\langle!\rangle(\Box_a p \wedge \neg\Box_b \Box_a p)
$$

On the other hand, $M'_1 \simeq^n M''_1$, i.e., if you cut off the part of the model further away
from the actual state 1 than $n$ steps, the models are bisimilar. Models that are $n$-bisimilar
satisfy the same formulas in $\mathcal{L}(\diamond, !)$ of modal depth at most $n$. Therefore, as $d(\psi) \le n$,

$M'_{1} \models \psi \quad \text{iff} \quad M''_{1} \models \psi$

and thus, as $M_1'' \simeq M_1$,

$M'_{1} \models \psi \quad \text{iff} \quad M_{1} \models \psi$

Again, we obtained a contradiction.
## 3.4 Axiomatization and theory

The logic APAL has a complete infinitary axiomatization for the class S5, for which the preferred reference is [26].<fnref n="2" /> The axiomatization is infinitary because it contains a derivation rule with infinitely many premisses in order to draw a conclusion. Axiomatizations like that of PAL and AML that contain finitely many axioms (axiom schemes) and finitely many rules with finitely many premisses are finitary.

The axiomatization of APAL extends the axiomatization of PAL with one axiom and one derivation rule involving the quantifier. The derivation rule is formulated using the so-called necessity forms or admissible forms [80] $\mathcal{L}_\#^*$ defined as $\varphi(\#) := \# | \varphi \to \varphi(\#) | \Box_a\varphi(\#)$ or $[\varphi]\varphi(\#)$, where $\varphi \in \mathcal{L}(\diamond, !, \langle!\rangle)$, and where we used bold-face font to distinguish $\varphi(\#) \in \mathcal{L}_\#^*$ from $\varphi \in \mathcal{L}(\diamond, !, \langle!\rangle)$. Given some $\psi \in \mathcal{L}(\diamond, !, \langle!\rangle)$, to obtain $\varphi(\psi)$ from $\varphi(\#)$ we replace the unique symbol $\#^*$ in $\varphi(\#)$ by $\psi$ and we thus get a formula in $\mathcal{L}(\diamond, !, \langle!\rangle)$.

The axiom and rule are:

$$ \begin{array}{l@{\qquad}l} [!]\varphi \to [\psi]\varphi & \text{where } \psi \in \mathcal{L}(\diamond, !) \\ (\varphi([\psi]\chi) \text{ for all } \psi \in \mathcal{L}(\diamond, !)) \text{ implies } \varphi([!]\chi) & \text{where } \varphi(\#) \in \mathcal{L}_\#^* \end{array} $$

It is unknown whether there is a finitary axiomatization as well for APAL. Further, we conjecture that the axiomatization without the S5 axioms T, 4, and 5 is complete for the class $\mathcal{K}$, by an analogous completeness proof. 'Conjecture' seems a big word, it is merely that such a proof is not on record.

The logic APAL is not compact [25], the satisfiability problem is undecidable [70] (the usual tiling argument applies), and the model checking problem is PSPACE-complete [3], where this is shown in [3] for an APAL variant called GAL that we will present later, but the method also applies to APAL. Also, APAL does not have the finite model property [141]. A logic has the finite model property (FMP) if any satisfiable formula has a model with a finite domain.

Like APAL, the logic APAL is bisimulation invariant, so adding the quantifier does not change that property. A proof is found in [143], and also for a related logic. Note that it is not found in the reference publication [25]. So, if two models are bisimilar, they satisfy the same formulas in $\mathcal{L}(\diamond, !, \langle!\rangle)$. However, unlike PAL, the logic APAL does not preserve restricted bisimulation or bounded bisimulation [143]. Having just seen the expressivity proofs, it is easy to see why. Because the APAL quantifier implicitly quantifies over all atoms, it does not preserve restricted bisimilarity. For example, in the first expressivity proof, the models are p-bisimilar, but the distinguishing formula $\langle!\rangle(\Box_a p \wedge \neg\Box_b\Box_a p)$ only contains atom p: it is in $\mathcal{L}(\diamond, !, \langle!\rangle)|_p$. Because the APAL quantifier implicitly quantifies over arbitrarily large modal depth, it does not preserve bounded bisimilarity. For example, in the second expressivity proof, the models are 2-bisimilar, but the (same) distinguishing formula $\langle!\rangle(\Box_a p \wedge \neg\Box_b\Box_a p)$ has modal depth 2.

<footnote n="2">²This axiomatization is found in [25] as well, but that publication also contains an incorrect finitary axiomatization. The corrections are discussed in [24, 26].</footnote>
## 3.5 Variations

A fair number of variations of APAL have seen the light. Prior to a more detailed presentation, let us see some of this variation.

$$ M_s \models \langle ! \rangle \varphi \quad \text{iff} \quad \text{there is a quantifier-free } \psi \text{ such that } M_s \models \langle \psi \rangle \varphi \quad \text{(APAL) [25]} $$

$$ M_s \models \langle ! \rangle \varphi \quad \text{iff} \quad \text{there is a } \psi \text{ such that } M_s \models \langle \psi \rangle \varphi \quad \text{(full APAL) [158]} $$

$$ M_s \models \langle ! \rangle \varphi \quad \text{iff} \quad \text{there is a positive } \psi \text{ such that } M_s \models \langle \psi \rangle \varphi \quad \text{(APAL$^+$) [143]} $$

$$ M_s \models \langle ! \rangle \varphi \quad \text{iff} \quad \text{there is a Boolean } \psi \text{ such that } M_s \models \langle \psi \rangle \varphi \quad \text{(BAPAL) [140]} $$

But there are many more, that are also reported below. What is the interest? The logic APAL is undecidable, has a high complexity of model checking, and has no known finitary axiomatization. Taming this into decidability, lower complexities, or a finitary axiomatization (or other proof methods such as sequent or tableaux calculi) is a computational advantage for applications such as epistemic planning and security protocols. Although a nice aim, the reality has so far turned out to be fairly tough, as we will see. However, this is, we think, very informative for the reader. Of independent interest is that some variations may provide a better match to address philosophical logical themes such as knowability or AI themes involving agency. Let us proceed.

### 3.5.1 Fully arbitrary announcements

In this variation we really quantify over all announcements, without restriction. It therefore seems to have a large intuitive appeal.

$$ M_s \models \langle ! \rangle \varphi \quad \text{iff} \quad \text{there is a } \psi \text{ such that } M_s \models \langle \psi \rangle \varphi $$

where $\varphi, \psi, \langle ! \rangle \varphi, \langle \psi \rangle \varphi$ are all in the same language, so that in particular $\psi$ is really an arbitrary formula in that language. As already mentioned, if this were a definition, it would be circular, as one of those $\psi$ may be the formula $\langle ! \rangle \varphi$. However, in [158] a logic is proposed with quantification over announcements where the above is a *property* of the logic, instead of the semantics of the quantifier. The language $\mathcal{L}_{Ord}(\diamond, !, \langle ! \rangle)$, where $Ord$ are the ordinals, has additionally to the $\langle ! \rangle$ quantifier also quantifiers $\langle !_\alpha \rangle$ for any ordinal $\alpha$. Let now $\mathcal{L}_\alpha$ be the sublanguage only containing quantifiers $\langle !_\beta \rangle$ for $\beta < \alpha$, then we can define:

$$ M_s \models \langle !_\alpha \rangle \varphi \quad \text{iff} \quad \text{there is } \psi \in \mathcal{L}_\alpha \text{ such that } M_s \models \langle \psi \rangle \varphi $$

$$ M_s \models \langle ! \rangle \varphi \quad \text{iff} \quad \text{there is } \alpha \in Ord \text{ such that } M_s \models \langle !_\alpha \rangle \varphi $$

The axiomatization of the logic is unclear, as the collection of $\langle !_\alpha \rangle$ in the logical language is a proper class. In other words, although it is fun (and maybe even elegant) to have such a logic wherein arbitrary is really arbitrary, it may not be of much practical value and does not help us with pushing down complexities. An open question is whether $\langle ! \rangle \varphi$ is equivalent to $\langle !_\omega \rangle \varphi$, that is, whether the hierarchy stabilizes at $\mathcal{L}_\alpha = \mathcal{L}_\omega$.<fnref n="3" /> If so, we can then simply define that: $M_s \models \langle ! \rangle \varphi$ iff there is a $n \in \mathbb{N}$ such that $M_s \models \langle !_n \rangle \varphi$, and it might bring the axiomatization closer.

<footnote n="3">³Originally suggested by Alexandru Baltag, and also by a reviewer.</footnote>
### 3.5.2 Positive announcements

In this variation we only allow quantification over positive formulas. It is conjectured to bring decidability of satisfiability.

$$M_s \models \langle ! \rangle \varphi \quad \text{iff} \quad \text{there is a positive } \psi \text{ such that } M_s \models \langle \psi \rangle \varphi$$

In a positive formula, an epistemic modality is never bound by a negation. The positive formulas are defined as:

$$\varphi ::= p|\neg p|\varphi \lor \varphi|\varphi \land \varphi|\Box_a\varphi$$

The positive formulas correspond to the universal fragment in the first-order translation (essentially, where negations do not bind universal quantifiers [119]).<fnref n="4" /> They have the property that they are *preserved* after an informative update, such as an announcement. They are therefore also *successful*: they remain true after their announcement. The logic with this quantifier is called APAL⁺, for *positive arbitrary public announcement logic*. All results reported here are for class S5. Note that the language of APAL⁺ contains the usual public announcement, so that any formula may be announced, also formulas that are not positive. The restriction is only for witnesses of the quantifier $\langle ! \rangle$.

From a more semantic perspective we can observe that positive formulas are also preserved after a *refinement* of a given model (see Section 2). Given a model $M = (S, R, V)$ and $T \subseteq S$, $T$ is called *closed under refinements* iff for all $s, t \in S$ such that $M_s \supseteq M_t$, if $s \in T$ then $t \in T$. The denotation of a positive announcement is closed under refinements, and dually, on finite models a subset of the domain that is closed under refinements is the result of a positive announcement. This is a powerful tool to investigate APAL⁺. Refinements also have a much more general use in dynamic epistemic logics. Section 7 is dedicated to refinements.

The logic APAL⁺ is incomparable in expressivity to APAL. This result is not obvious, as we are comparing two logics with different quantifiers. Both directions of the incomparability result have non-trivial proofs that cannot be easily sketched in this survey, and that use closure under refinements as a proof tool. Just as for APAL, the complexity of model checking in APAL⁺ is PSPACE-complete. The (known) axiomatization of APAL⁺ is much like that of APAL: in the axiom and in the derivation rule we merely replace the witness for a positive witness. For details on expressivity, model checking and axiomatization we refer to [143].

$$\varphi ::= p|\neg p|\varphi \lor \varphi|\varphi \land \varphi|\Box_a\varphi[\neg\varphi][!]\varphi$$

that is also known as the positive formulas, and that figure in, for example, [148, 25], where the [!] in the inductive case [!]ϕ is the APAL quantifier. The negation in [¬ϕ]ψ may appear strange at first sight but this is a consequence of the semantics of public announcement: note that $M_s \models [\neg\varphi]\psi$ iff $(M_s \models \neg\varphi \text{ implies } (M|\neg\varphi)_s \models \psi)$ iff $(M_s \models \varphi \text{ or } (M|\neg\varphi)_s \models \psi)$. An interesting question seems whether, if the [!] in the inductive case [!]ϕ were the APAL⁺ quantifier instead of the APAL quantifier, every extended positive formula would be equivalent to a positive formula.

<footnote n="4">⁴The above positive formulas are to be distinguished from their extension</footnote>
We conjecture that the logic APAL⁺ is decidable.<fnref n="5" /> Decidability of APAL⁺ is interesting for potential applications. In many scenarios only positive information change plays a role, given some initial information state containing ignorance, such as security protocols with mutual acknowledgements by principals of messages with factual content, or scenarios with sensing in order to reduce uncertainty and provide diagnostics.

### 3.5.3 Boolean announcements

In this variation we only allow quantification over Booleans. We now get a finitary axiomatization and decidability.

$$M_s \models \langle ! \rangle \varphi \quad \text{iff} \quad \text{there is a Boolean } \psi \text{ such that } M_s \models \langle \psi \rangle \varphi$$

A Boolean or a formula in propositional logic is a formula in $\mathcal{L}(\emptyset)$. Boolean announcements result in model restrictions, and, as public announcements only change the information about the true value of propositional variables but not their actual value, such announced Booleans remain true after (truthful!) announcement: Boolean announcements are successful. Also, Booleans are positive formulas. The resulting logic BAPAL is decidable [142], and has a finitary axiomatization [140]. Still, it does not have the finite model property [142]. The results reported here are for class S5. The relevant axiom and derivation rule are:

$$ \begin{array}{l@{\qquad}l} [!]\varphi \rightarrow [\psi_0]\varphi & \text{where } \psi_0 \in \mathcal{L}(\emptyset) \\ \psi \rightarrow [\chi][p]\varphi \text{ implies } \psi \rightarrow [\chi][!]\varphi & \text{where } p \notin v(\psi), v(\chi), v(\varphi) \end{array} $$

The atom $p$ not occurring in any of the formulas occurring in the derivation rule is called fresh. It has to be fresh in order to avoid that its value depends on occurrences of atoms in these formulas (which would permit invalid rule applications). Note that $\psi \rightarrow [\chi][p]\varphi$ and $\psi \rightarrow [\chi][!]\varphi$ are instantiations of the necessity form $\psi \rightarrow [\chi]_\#$. The APAL derivation rule “$\psi([\eta]\varphi)$ for all quantifier-free $\eta$, implies $\psi([!]\varphi)$”, where $\psi(\#)$ may be any necessity form, has an infinity of premisses, namely one for every formula $\eta$, whereas the BAPAL derivation rule has one premiss only, namely for a fresh variable $p$. This makes the axiomatization finitary.

The logic BAPAL is more expressive than PAL (which is shown as for APAL), and BAPAL is not at least as expressive as APAL [140] (on class S5). However, it is unknown if APAL is not at least as expressive as BAPAL. To prove that, one would somehow have to show that the Boolean quantifier can be ‘simulated’ by an APAL quantifier that is properly entrenched in preconditions and postconditions relative to $\varphi$. This seems quite hard. The proof that BAPAL is not at least as expressive as APAL uses, not surprisingly, that the BAPAL quantifier does not quantify over formulas of arbitrarily large modal depth, as the modal depth of Booleans is zero. The proof is instructive. We therefore sketch it.

<footnote n="5">⁵Work in progress by Tim French et al. employ a technique combining the S5 modalities for knowledge with the KD4-like modalities for public announcements — we can alternatively see the model transformation induced by a public announcement in dynamic epistemic logic as a pair in the accessibility relation associated to that announcement, in a larger model that is constructed from the direct sum of all model restrictions of a given model, as in [164].</footnote>
The proof that BAPAL is not at least as expressive as APAL is very similar to the proof that PAL is less expressive than APAL in Section 3.3. We recall that the proof that PAL is less expressive than APAL cansisted of two parts. One part was that (trivially) APAL is at least as expressive as PAL, because the language of PAL is a fragment of the language of APAL. This part no longer holds for BAPAL. The other part consisted in showing that PAL is not at least as expressive as APAL. We can reuse that part for BAPAL. In the version of the proof for BAPAL we again use bounded bisimilarity, but slightly differently. To emphasize the similarity in method we will use the same epistemic models as in Section 3.3 and not the models used in the proof in [140], that are a bit different.

Consider again the APAL formula $\langle ! \rangle (\Box_a p \wedge \neg \Box_b \Box_a p)$. Let us suppose that there exists an equivalent formula $\psi$ in the same logical language but interpreted according to the BAPAL semantics (the languages of APAL and BAPAL are the same in this survey, so we need to distinguish APAL and BAPAL by their semantics). Note that this is a difference with the previous proof, where $\psi$ was a quantifier-free formula, in the language of PAL. Now recall the models $M_1, M'_1$ and $M''_1$ of the previous proof, and that $M_1 \simeq M''_1$ and $M'_1 \simeq^{d(\psi)} M''_1$.

Unlike APAL, the logic BAPAL has the property that bounded bisimulation implies bounded modal equivalence, i.e., the same truth value for formulas of modal depth up to that bound [140]. Therefore, $M'_1 \simeq^{d(\psi)} M''_1$, so that models $M'_1$ and $M''_1$ both make $\psi$ true or both make $\psi$ false. And as $M_1 \simeq M''_1$, also $M_1$ and $M'_1$ have the same value for $\psi$. On the other hand, as before, $M_1 \models \langle ! \rangle (\Box_a p \wedge \neg \Box_b \Box_a p)$ whereas $M'_1 \models \langle ! \rangle (\Box_a p \wedge \neg \Box_b \Box_a p)$. Contradiction, and end of proof.

Informally, it is also easy to see that Boolean announcements cannot achieve much to distinguish $M'_1$ from $M''_1$. One can either announce $p$ or $\neg p$ (not $p$ is ruled out as this is false in the point 1). The first announcement trivializes $M'_1$ as well as $M''_1$ to a singleton where $p$ is common knowledge, whereas the second announcement is not informative in either model.

### 3.5.4 APAL with memory

In this variation we keep the original value of propositions in memory. We can express that after an announcement a formula was true. It has a finitary axiomatization.

In APAL with memory (APALM) [31, 32], instead of models $M = (S, R, V)$ we have models $M = (S, T, R, V)$, where $T \subseteq S$, and where $(S, S, R, V)$ is an initial model (and where all relations $R_a$ are equivalence relations — the results are for class S5). The domain $S$ is the initial domain, whereas the domain $T$ is the current domain, the current model restriction. This additional structural information makes it possible to refer to what was true in the past, as well as to what is true now. The logical language has additional operators to access this historical information, namely $\varphi^0$ (for ‘$\varphi$ was initially true’), a constant 0 that is true when the model is initial, and the universal modality $U$. The semantics for $\varphi^0$ is (where $s \in T$):

$$ (S, T, R, V)_s \models \varphi^0 \text{ iff } (S, S, R, V)_s \models \varphi $$
The semantics for the quantifier are as in APAL. Namely

$$M_s \models \langle ! \rangle \varphi \quad \text{iff} \quad \text{there is a quantifier-free } \psi \text{ such that } M_s \models \langle \psi \rangle \varphi$$

However, the semantics for public announcement are not as in APAL. Different from APAL, and from PAL, the inductive construct $\langle\varphi\rangle\psi$ now has the restriction that $\varphi$ must be quantifier-free. This restriction on what can be publicly announced makes it harder to compare APAL to APALM. It is unclear whether in the logic APAL, for all $\varphi, \psi \in \mathcal{L}(\diamond, !, \langle!\rangle)$ there is a $\chi \in \mathcal{L}(\diamond, !)$ such that $\langle\varphi\rangle\psi$ is equivalent to $\langle\chi\rangle\psi$. One unanswered question is then whether the set of APAL validities is the same as the set of APALM validities restricted to the language $\mathcal{L}(\diamond, !, \langle!\rangle)$.

There are also relations between APALM and the logic with modalities for what is true before an announcement by [28]. Like APALM, that logic is interpreted on structures where apart from the current model we keep the initial model in memory.

Let us now look into the difference between APAL and APALM. The difference has to do with the phenomenon in PAL that non-bisimilar states may become bisimilar after an announcement, as in the following example. The power of APALM is that it can distinguish between such (standardly) bisimilar states because the model still remembers that that the states were different.

**Example 6** Consider states $t$ and $u$ in the following model $M$, and in its restriction $M|p$.

$$0(s) \quad \frac{b}{1(t)} \quad \frac{a}{1(u)} \quad \Rightarrow \quad \frac{a}{1(t)} \quad \frac{a}{1(u)}$$

In $M$, the states $t$ and $u$ have different knowledge properties, for example, $M_t \models \neg \Box_b p$ whereas $M_u \models \Box_b p$, and they are not bisimilar. However, after the public announcement of $p$ they have become indistinguishable: $(M|p)_t$ and $(M|p)_u$ are bisimilar and therefore satisfy the same formulas. In APALM, we can still distinguish the state $t$ and $u$ in $M|p$, because $(M|p)_t \models (\neg \Box_b p)^0$ whereas $(M|p)_u \models (\Box_b p)^0$.

The logic APALM has a finitary axiomatization. This is possible because of the memory feature of APALM [31, Section 3]. The derivation rule introducing the quantifier is similar to the one in BAPAL. It is not known whether APALM is decidable.

Also, APALM may have an interesting take on knowability. We recall from Section 3.2 that in APAL everything is knowable in the sense that $\langle!\rangle\Box_a\varphi \lor \langle!\rangle\Box_a\neg\varphi$ is valid [153], but at the price of changing the value of propositions. You can formalize that you can get to know that a proposition is true (now), but you cannot formalize that you can get to know that a proposition was true. But in APALM you can, namely as $\varphi \rightarrow \langle!\rangle\Box_a\varphi^0$. And $\langle!\rangle\Box_a\varphi^0 \lor \langle!\rangle\Box_a\neg\varphi^0$ then formalizes that for every proposition you can get to know whether it was true or false. Are these APALM validities?
### 3.5.5 Almost Arbitrary Announcements

In this variation we quantify over propositions that are stronger or weaker than a given formula. This permits a notion of dynamic consequence with novel substructural properties.

$M_s \models \langle \chi^{\downarrow} \rangle \varphi$ iff there is a quantifier-free $\psi$ implying $\chi$ such that $M_s \models \langle \psi \rangle \varphi$

where $\chi$ is also quantifier-free, and where by “$\psi$ implies $\chi$” we mean that $\psi \to \chi$ is valid (in PAL). So we then get:

$M_s \models \langle \chi^{\downarrow} \rangle \varphi$ iff there is a quantifier-free $\psi$ such that $\models \psi \to \chi$ and $M_s \models \langle \psi \rangle \varphi$.

This variation of APAL semantics was initially suggested by Igor Sedlár, for a more general setting of substructural logics. Results have been published in [151] and subsequently in [152] (the expanded journal version of the former). The resulting logic is called IPAL$^{\downarrow}$ (where the I stands for ‘implying’). As in APAL, the quantification in IPAL$^{\downarrow}$ is over quantifier-free formulas, however, only over those formulas $\psi$ that are at least as strong as a given formula $\chi$. Structurally, given some model $M$, we quantify over all restrictions of $M$ that are contained in $M|\chi$. In the semantics, the following are interchangeable (see [151, Prop. 4]):

(i) $\models \psi \to \chi$ and $M_s \models \langle \psi \rangle \varphi$

(ii) $M \models \psi \to \chi$ and $M_s \models \langle \psi \rangle \varphi$

(iii) $M_s \models \langle \psi \wedge \chi \rangle \varphi$

where in formulation (iii) not $\psi$ but $\psi \wedge \chi$ is the formula implying $\chi$.

A dual ‘at most as strong as’ quantifier $\langle \chi^{\uparrow} \rangle$ has semantics

$M_s \models \langle \chi^{\uparrow} \rangle \varphi$ iff there is a quantifier-free $\psi$ implied by $\chi$ such that $M_s \models \langle \psi \rangle \varphi$

In other words, now we quantify over all restrictions of $M$ that contain $M|\chi$. This begets the logic IPAL$^{\downarrow}$; IPAL is the logic containing both operators.

The axiomatization of IPAL$^{\downarrow}$ is straightforward, by replacing the APAL axiom and derivation rule by the following, where $\eta(\#)$ is a necessity form and where we recall the above paraphrase (iii) of the IPAL$^{\downarrow}$ semantics:

$[\chi^{\downarrow}]\varphi \to [\psi \wedge \chi]\varphi$, for all quantifier-free $\psi$
From $\eta([\psi \wedge \chi]\varphi)$ for all quantifier-free $\psi$, infer $\eta([\chi^{\downarrow}]\varphi)$

The logic is also undecidable, where the proof method of [6] applies, as $[\uparrow^{\downarrow}]\varphi$ is equivalent to $[!]\varphi$. So we can build a tiling of the plane as usual.

One can show that IPAL is less expressive than APAL, by a technically involved argument not resembling anything shown so far in this survey and therefore omitted (see [152]).

The relation between IPAL$^{\downarrow}$ and substructural logic is that we can view $\models = [\psi_1^{\downarrow}]...[\psi_n^{\downarrow}]\varphi$ as so-called *dynamic consequence* $\psi_1...\psi_n \Rightarrow \varphi$, as an alternative to Van Benthem's dynamic consequence [126, 19] defined as $\models = [\psi_1]...[\psi_n]\varphi$. This may be of proof theoretical interest as this alternative dynamic consequence relation satisfies more substructural
properties. For example, unlike [126], it satisfies ‘strong weakening’, defined as “from $\psi_1...\psi_n \Rightarrow \varphi$, infer $\psi_1...\psi...\psi_n \Rightarrow \varphi$” (insert $\psi$ anywhere in the sequence $\psi_1...\psi_n$). This novel notion of dynamic consequence clearly deserves closer exploration.

A possibly very different logic seems to result if in $\langle\chi^\downarrow\rangle\varphi$ and $\langle\chi^\uparrow\rangle\varphi$ the formula $\chi$ is not required to be quantifier-free but may also contain quantifiers. The resulting logic QIPAL is also succinctly presented in [152]. It should be noted that these semantics are well-defined. As observed by Saúl Fernández González, this is not immediately clear, as to determine the truth of $\langle\chi^\downarrow\rangle\varphi$ we need to establish the validity of $\psi \to \chi$ in QIPAL. However, in QIPAL the paraphrased semantics (iii) above is also equivalent to the semantics with (i), from which well-definedness easily follows by induction on the number of quantifiers.

### 3.5.6 Knowability logic

In this variation we directly interpret the APAL quantifier on epistemic models and omit the public announcements from the logical language. So let now $\langle!\rangle\varphi \in \mathcal{L}(\diamond, \langle!\rangle)$.

$$M_s \models \langle!\rangle\varphi \text{ iff there is a quantifier-free } \psi \text{ such that } M_s \models \psi \text{ and } (M|\psi)_s \models \varphi$$

We recall that the APAL semantics of $\langle!\rangle\varphi \in \mathcal{L}(\diamond, !, \langle!\rangle)$ use public announcement.

$$M_s \models \langle!\rangle\varphi \text{ iff there is a quantifier-free } \psi \text{ such that } M_s \models \langle\psi\rangle\varphi$$

The semantics are equivalent. But for the former we do not need public announcement in the logical language. Given that formulas of shape $\langle!\rangle\square_a\varphi$ represent “$\varphi$ is knowable”, the logic with language $\mathcal{L}(\diamond, \langle!\rangle)$ without announcements is called *knowability logic* [137]. It is not known what its axiomatization is. Wiebe van der Hoek mentioned that, in some way, we ‘know’ what its axiomatization is, because it consists of the validities of APAL not containing public announcements. But it is unknown how to get these systematically. The axiom and rule for $\langle!\rangle$ in APAL need to be replaced by something not using announcements.

Another such logic for knowability has been proposed in [166], now based on a relation-restricting update, instead of a domain-restricting update.

A logic for knowability called LK (as well as a number of variants) was proposed in [101], of which the logical language is the fragment of $\mathcal{L}(\diamond, !, \langle!\rangle)$ wherein the two modalities $\langle!\rangle$ and $\square_a$ are bundled/packed. The language of this logic is $\varphi := p | \neg\varphi | (\varphi \wedge \varphi) | \diamond_a\varphi | \langle\varphi\rangle\varphi' | \langle!\rangle\square_a\varphi$, where $\langle!\rangle\square_a\varphi$ stands for “$\varphi$ is knowable by $a$.” Such bundled logics often have, obviously, different axiomatizations, complexity (or decidability) of decision problems, etcetera [109, 163]. But not in this case: the axiomatization of the logic LK is again similar to that of APAL, and LK is also undecidable. We conjecture that LK is less expressive than APAL.

### 3.5.7 Arbitrary announcement as effort

In this variation we interpret the APAL quantifier on epistemic models with more, topological, structure.

$$M_s \models \langle!\rangle\varphi \text{ iff there is a quantifier-free observable } \psi \text{ such that } M_s \models \langle\psi\rangle\varphi$$
Here, ‘observable’ is a topological notion defined further below. In this setting an arbitrary announcement quantifier is interpreted as a kind of ‘effort’ modality: if you can get to know a proposition after incorporating the informative consequences of an announcement, this is like getting to know a proposition after making some effort. Instead of quantifying over submodels reached by executing announcements, we can alternatively quantify over submodels of a given model reached by an alternative semantics for such announcements on models that have more structure than the epistemic models central in this survey: only some subsets of the domain that are denotations of formulas are permitted. Examples of such richer structures are the subset spaces in the work by Parikh and collaborators [49], or more topological, or topologically inspired, structures in publications like [108, 36, 147, 37]. In the above semantics of the quantifier, a formula $\psi$ is observable if the topological interior of its denotation is true: in other words, ‘permitted’ then means ‘open’. We refer to the cited works for details.

### 3.5.8 Quantifying over formulas for subsets of atoms

In this variation we only allow quantification over formulas containing a subset of atoms.

$$ M_s \models \langle ! \rangle \varphi \text{ iff there is a } \psi \in \mathcal{L}(\diamond, !) | P(\varphi) \text{ such that } M_s \models \langle \psi \rangle \varphi $$

Here, $P(\varphi) \subseteq P$ is the set of atoms occurring in $\varphi$, and $\mathcal{L}(\diamond, !)|P(\varphi)$ is the language of the quantifier-free formulas only containing atoms in $P(\varphi)$. The logic with this quantifier is called SCAPAL and it is reported in [152]. Barteld Kooi already observed many years before [152] that such a modality does not distribute over disjunction, i.e., $\langle ! \rangle \varphi \lor \langle ! \rangle \psi$ is not equivalent to $\langle ! \rangle (\varphi \lor \psi)$. Dually, $[!] \varphi \land [!] \psi$ is not equivalent to $[!] (\varphi \land \psi)$.

**Example 7** Consider again the formula $\langle ! \rangle (\Box_a p \land \neg \Box_b \Box_a p)$ used in the expressivity proofs for APAL and the same models and announcement (see Section 3.3). Let $M$ be the model on the left.

$$ \begin{array}{ccc} & \begin{array}{c} a \\ \frac{01}{\boxed{b}} \frac{11}{\boxed{a}} \frac{11}} \end{array} & \frac{a}{\boxed{b}} \frac{11}{\boxed{b}} \frac{11}} \\ \frac{a}{\boxed{b}} \frac{11}{\boxed{a}} \frac{11}} & \frac{a}{\boxed{b}} \frac{11}{\boxed{b}} \frac{11}} & \frac{a}{\boxed{b}} \frac{11}{\boxed{b}} \frac{11}} \end{array} \Rightarrow \frac{a}{\boxed{b}} \frac{11}{\boxed{b}} \frac{11}} \end{array} $$

We now have that

$$ M_{10} \models \langle ! \rangle ((\Box_a p \land \neg \Box_b \Box_a p) \lor q) \qquad (i) $$

$$ M_{10} \not\models \langle ! \rangle (\Box_a p \land \neg \Box_b \Box_a p) \qquad (ii) $$

$$ M_{10} \not\models \langle ! \rangle q \qquad (iii) $$

The first is true because, as depicted:

$$ M_{10} \models \langle p \lor q \rangle (\Box_a p \land \neg \Box_b \Box_a p), \text{ so} $$

$$ M_{10} \models \langle p \lor q \rangle ((\Box_a p \land \neg \Box_b \Box_a p) \lor q), \text{ and therefore} $$

$$ M_{10} \models \langle ! \rangle ((\Box_a p \land \neg \Box_b \Box_a p) \lor q) $$
where we note that announcement $p \lor q$ is indeed in the language containing atoms occurring in $P((\Box_a p \land \neg \Box_b \Box_a p) \lor q) = \{p, q\}$. The second is false because the only model restrictions containing 10 that we can obtain with formulas only involving $p$ are {10, 11} (which is $M|p$) and {10, 11, 00, 01} (which is $M$ itself). The third is false because $q$ is false in state 10.

Therefore, $\langle ! \rangle \varphi \lor \langle ! \rangle \psi$ is not equivalent to $\langle ! \rangle (\varphi \lor \psi)$.

A similar yet slightly different version is the logic with, for each $Q \subseteq P$, quantifier

$$M_s \models \langle !_Q \rangle \varphi \text{ iff there is a } \psi \in \mathcal{L}(\diamond, !)|Q \text{ such that } M_s \models \langle \psi \rangle \varphi$$

which results in the logic called SAPAL (S for ‘subset’). If we require $Q$ to be finite we get FSAPAL. These logics are also reported in [152]. Although all these logics have slightly different expressivity, their axiomatizations are not very different from APAL and they are also undecidable.

### 3.5.9 Quantifying over formulas of bounded modal depth

In this variation we only allow quantification over formulas of bounded modal depth. This is a novel proposal. We are unaware of a publication or work in progress.

$$M_s \models \langle !^n \rangle \varphi \text{ iff there is a } \psi \in \mathcal{L}(\diamond, !) \text{ with } d(\psi) \le n \text{ and such that } M_s \models \langle \psi \rangle \varphi$$

This quantification over quantifier-free formulas of bounded modal depth has been suggested by Tim French. We have already seen a bit of this variation: the logic BAPAL has quantifiers $\langle !^0 \rangle$ in this sense. That may not be immediately obvious. The quantifier-free formulas of modal depth 0 may contain announcement modalities but do not contain any epistemic modalities $\diamond$. But from such formulas we can eliminate the announcements. It is easy to see that for $\varphi, \psi \in \mathcal{L}(!)$, $[\varphi]\psi$ is equivalent to $\varphi \rightarrow \psi$. Using that we can prove by induction on the number of announcements in a formula that any $\varphi \in \mathcal{L}(!)$ is equivalent to a $\varphi' \in \mathcal{L}(\emptyset)$, that is, to a Boolean.

It seems interesting to investigate whether, like BAPAL, this logic has a finitary axiomatization and is decidable.

## 3.6 Open problems and further research

There are many more relevant works, that we do not discuss in detail. How logics like APAL can be employed to formalize knowability is currently actively discussed in the formal epistemology community [169, 91]. The tendency is towards more explicit temporal perspectives, as in APALM (Section 3.5.4). A version of APAL to reason about asynchronous information change is presented in [27]. A so-called ‘mental program’ arbitrary public announcement logic is presented in [48]. It is a decidable version of APAL, however, the basic (epistemic-like) modalities and the structures on which such modalities are interpreted, are already very different from the epistemic models in this survey.

Open problems about APAL and its variants include:
* Whether APAL has a finitary axiomatization [26]

* Whether APAL$^+$ is decidable [143]

* Is APAL not at least as expressive as BAPAL [140]?

* Does the Full APAL hierarchy stabilize at $\omega$ [158]?

* The axiomatization of the logic of knowability [153]

* Formalizing knowability in APALM [32]

* Is LK less expressive than APAL [152]?

* The substructural properties of dynamic consequence based on IPAL$^↓$ [152]

# 4 Group announcement and coalition announcement

## 4.1 Announcements by agents

This section is devoted to group announcement logic GAL and coalition announcement logic CAL. These are clearly also variations of APAL, but we deal with them separately in this survey, as they are more targeted towards modeling aspects of agency and therefore have received quite a bit of attention from that community. Extensions of GAL and CAL with common knowledge and distributed knowledge are discussed in Section 8.

**How to model an announcement by an agent** We recall that a truthful public announcement made by an outside observer is a true public announcement. This is information coming into the system from a trusted outside source. A truthful public announcement made by an agent whose knowledge or beliefs are modelled in the system is not necessarily true. Now there is a difference between truthful and true. Announcements made by agents can be truthful but not true, and can be true but not truthful. An announcement made by an agent is truthful if it is believed by that agent. If agent $a$ truthfully says $\varphi$ we therefore model this as the announcement $\Box_a\varphi$.

We now have to distinguish our usual setting in this survey, the treatment of knowledge and of updates preserving $S5$ models, from the treatment of belief and of other updates.

*On $S5$ models, the truthful announcement $\varphi$ by agent $a$ is true.*

This is, because $\Box_a\varphi$ implies $\varphi$. It is standard in dynamic epistemic logics to model 'agent $a$ makes a truthful public announcement $\varphi$' in this way as 'a truthful public announcement $\Box_a\varphi$ is made', where the first occurrence of truthful implies true, and the second occurrence of truthful means true.

It is often said that modelling an announcement $\varphi$ by an agent $a$ as $\Box_a\varphi$ is a way to have a notion of agency in dynamic epistemic logic. This is true to the extent that, for
example, a multi-agent systems modeller can informally let $\Box_a\varphi$ always mean that agent $a$ observes (announces) $\varphi$. Formally we cannot distinguish the announcement by agent $a$ that $\varphi$, modelled in this way, from the announcement by the outside observer that $a$ knows $\varphi$.

*On not-S5 models, the announcement $\varphi$ by agent $a$ may be truthful but not true.*

When agent $a$ says $\varphi$ and $\neg\varphi \wedge \Box_a\varphi$ is true, agent $a$ is truthful because $\Box_a\varphi$ is true. This now represents that agent $a$ believes $\varphi$. This belief is mistaken (incorrect), because $\varphi$ is false. Formula $\neg\varphi \wedge \Box_a\varphi$ formalizes that agent $a$ has an incorrect belief in $\varphi$.

*On not-S5 models, the announcement $\varphi$ by agent $a$ may be true but not truthful.*

There are now two options. When agent $a$ says $\varphi$ and $\varphi \wedge \Box_a\neg\varphi$ is true, agent $a$ is lying because she believes $\varphi$ to be false. But in fact she is mistakenly saying the truth. Whereas when agent $a$ says $\varphi$ and $\varphi \wedge \neg(\Box_a\varphi \vee \Box_a\neg\varphi)$ is true, agent $a$ is bluffing because she is uncertain whether $\varphi$ is true, although confidently announcing $\varphi$. In fact she is unknowingly saying the truth, because $\varphi$ is true. See [102]. Speech acts such as lying and bluffing can easily be modelled as action models [138], and they can also be executed on S5 models, but the updated model is then no longer S5 [155].

Belief, lying, and bluffing are outside our scope. In this section we restrict ourselves to truthful public announcements by agents on models for knowledge.

**What is a simultaneous announcement?** Let us also elaborate on the simultaneity of announcements made by groups of agents. When three agents $a, b, c$ respectively say $\psi_a, \psi_b$, and $\psi_c$ simultaneously, we model this as the announcement $\Box_a\psi_a \wedge \Box_b\psi_b \wedge \Box_c\psi_c$. This is a simultaneous announcement by $a, b$, and $c$ consisting of three conjuncts. We do not model this as three successive announcements. The difference matters, because the truth value of $\Box_b\psi_b$ before the announcement of $\Box_a\psi_a$ may be different from the truth value of $\Box_b\psi_b$ after the announcement of $\Box_a\psi_a$. Just imagine that $a$ says that $p$ is true and that $b$ says that he is uncertain whether $p$; $b$ can say it at the same time as $a$ but not afterwards. We need not imagine simultaneous announcements as everybody talking at the same time. Public announcement is a misnomer for a *public event*, such as ‘the three children who know that they are muddy now step forward’ in the muddy children problem [106, 150]. This can be observed when done simultaneously. Or, back to $a, b, c$ talking, we can instead imagine $a, b, c$ writing, respectively, $\psi_a, \psi_b$, and $\psi_c$ on a piece of paper put into three envelopes after which the external observer or authority publicly opens the envelopes and reads their contents aloud in whatever order. It would be more accurate to say that we model such agents’ actions as *independent events*, as usual in concurrency. And do the three muddy children really step forward simultaneously, within a split microsecond? Of course not. It is rather that their decisions to step forward were made independently, pertaining to the same perceived previous state of information.
## 4.2 Group announcement logic

Group Announcement Logic GAL is a variation of APAL with, instead of quantifiers $\langle ! \rangle$, quantifiers $\langle !_G \rangle$, for any group of agents $G \subseteq A$, meaning ‘$\varphi$ is true after a simultaneous truthful public announcement by the agents in $G'$ [4, 3].

The semantics are as follows, where a set of formulas is quantifier-free if all formulas in the set are quantifier-free (so the members of $\{\psi_a | a \in G\}$ below are in $\mathcal{L}(\diamond, !)$).

$$ M_s \models \langle !_G \rangle \varphi \quad \text{iff} \quad \text{there is a quantifier-free } \{\psi_a | a \in G\} \text{ such that } M_s \models \langle \bigwedge_{a \in G} \Box_a \psi_a \rangle \varphi $$

Given $\langle !_G \rangle \varphi$, we imagine the remaining agents in $A \setminus G$ staying silent. Therefore, $\langle !_\emptyset \rangle \varphi$ is equivalent to $\varphi$. Whatever the $G$ in $\langle !_G \rangle$, all agents in $A$ are always listening: whatever public announcement is made, it is always observed by all agents, and in the same way.

**Example 8** Given are two agents $a, b$ such that $a$ knows whether $p$ and $b$ knows whether $q$ (and this is common knowledge), and let in fact $p$ be true and $q$ be false (the underlined state). Anne ($a$) can achieve that Bill knows whether $p$, namely by informing him of the value of $p$, and Bill ($b$) can similarly achieve that Anne knows whether $q$. Neither agent can achieve both outcomes at the same time, but together they can achieve that.

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

We can evaluate in the square model $M$ in the middle that

* $M_{10} \models \langle !_a \rangle \Box_b p$ but $M_{10} \not\models \langle !_b \rangle \Box_b p$

* $M_{10} \models \langle !_b \rangle \Box_a \neg q$ but $M_{10} \not\models \langle !_a \rangle \Box_a \neg q$

* $M_{10} \models \langle !_{ab} \rangle (\Box_b p \wedge \Box_a \neg q)$ but $M_{10} \not\models \langle !_a \rangle (\Box_b p \wedge \Box_a \neg q)$ and $M_{10} \not\models \langle !_b \rangle (\Box_b p \wedge \Box_a \neg q)$

Whatever the actual state, $a$ and $b$ can get to know it on this model by collaborating in the $\langle !_{ab} \rangle$ sense.

A number of GAL validities are as follows, where $G, H \subseteq A$.

* $\langle !_G \rangle \langle !_H \rangle \varphi \rightarrow \langle !_{G \cup H} \rangle \varphi$
If an announcement by group $G$ is followed by an announcement by group $H$, then $G$ and $H$ could have made a joint announcement with the same informative content.

* $\langle !_G \rangle \langle !_G \rangle \varphi \rightarrow \langle !_G \rangle \varphi$
A corollary of the previous.
The logic GAL shares various properties with APAL. For example, the infinitary axiomatization and the method to prove its completeness are similar, the model checking complexity is also PSPACE-complete, GAL is also undecidable [5, 6], and it also does not have the finite model property [141]. Expressivity is discussed later.

## 4.3 Coalition announcement logic

Another variation on APAL with aspects of agency is *coalition announcement logic* CAL. In group announcement logic GAL we investigate the consequences of the simultaneous announcement by $G$. The agents not in $G$ do not take part in the action. In CAL we quantify over what the agents in $G$ can achieve by their joint announcement, no matter what the other agents simultaneously announce.

In the logical language we replace the GAL quantifier $\langle!_G\rangle$ by the CAL quantifier $\langle!_G\rangle$, where $G \subseteq A$. The notation is supposed to suggest its $\exists\forall$-semantics, and that of the dual $\langle!_G\rangle$ its $\forall\exists$-semantics. The semantics of coalition announcement are then as follows.

$$ M_s \models \langle!_G\rangle\varphi \quad \text{iff} \quad \begin{array}{l} \text{there is a quantifier-free } \{\psi_a \mid a \in G\} \text{ such that} \\ \text{for all quantifier-free } \{\psi_a \mid a \in A \setminus G\} \\ M_s \models \bigwedge_{a \in G} \Box_a \psi_a \text{ and } M_s \models [\bigwedge_{a \in A} \Box_a \psi_a]\varphi \end{array} $$

**Example 9** Consider again the four-state model $M$ of Example 8. Although we have that $M_{10} = \langle!_a\rangle\Diamond_a q$ (namely by $a$ simply doing nothing / announcing $\top$), it is **not** the case that $M_{10} = \langle!_a\rangle\Diamond_a q$: agent $b$ can prevent $a$ from remaining ignorant about $q$ by announcing $\neg q$. It then does not matter whether $a$ announces $p$ or $\top$, either way $a$ will learn $\neg q$.

$$ \begin{array}{ccc} \Box_a p \wedge \Box_b \neg q & \quad & 01 \xrightarrow{b} 11 \\ \underline{10} & \iff & \left| \begin{array}{c} a \\ 00 \xrightarrow{b} \underline{10} \end{array} \right| \quad \Box_a \top \wedge \Box_b \neg q \\ & & \hspace{2em} \Rightarrow \hspace{2em} \Box_a \top \wedge \Box_b \neg q \end{array} $$

We still have that $M_{10} = \langle!_{ab}\rangle(\Box_b p \wedge \Box_a \neg q)$ — but this is trivial, as there are no other agents around to say something to prevent it. The power of group announcements by all agents is the same as that of an announcement by that ‘grand coalition’: $\langle!_A\rangle\varphi \leftrightarrow \langle!_A\rangle\varphi$.

The logic CAL was proposed and summarily discussed in [4]. No axiomatization is given. Publication [4] also succinctly presents an original neighbourhood semantics for the CAL quantifier. Given the $\exists\forall$ character of its semantics this is not surprising — we illustrate this by Example 10, below. Further below we relate CAL to coalition logic [112], that has a similar neighbourhood semantics.

**Example 10** Consider a different representation of the three models featuring in Example 9, namely as a single model $\mathcal{M}$ with point 10 as underlined (without giving details, we can see it as the direct sum of the three models $M, M|(\Box_a p \wedge \Box_b \neg q)$, and $M|(\Box_a \top \wedge \Box_b \neg q)$).
To distinguish states with similar names in different parts of the model we have given them different names.

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

A *neighbourhood* of a state *s* in the domain of *M* is a set of subsets of the domain of *M*. Any such subset in the neighbourhood is a set of *neighbours*. Let the two sets of neighbours of state 10 be *X* = {10*x*} and *Y* = {10, 10*y*}. So the set {*X*, *Y*} is the neighbourhood of 10.

We now define, ad hoc (see [4] for a proper definition), that for $\varphi \in \mathcal{L}(\diamond)$, $M_s \models \varphi$
if $(M_s \models \varphi$ or $(M|(\Box_a p \wedge \Box_b \neg q))_s \models \varphi$ or $(M|(\Box_a \top \wedge \Box_b \neg q))_s \models \varphi)$. We also consider a
novel modality $\langle a \rangle$, that is supposed to be reminiscent of $\langle !_a \rangle$, and for which we define, as
usual in neighbourhood semantics, that $M_s \models \langle a \rangle \psi$ iff there is a set of neighbours of *s* in
$M$ (in other words, a set of states in the neighbourhood of *s*) where $\varphi$ is true in all of its
states.

Let us now replay the previously observed $M_{10} \not\models \langle !_a \rangle \diamond_a q$ in the current setting and show that $M_{10} \not\models \langle a \rangle \diamond_a q$. Then we have that $M_{10} \not\models \langle a \rangle \diamond_a q$ because $\diamond_a q$ is not true in $X$ and $\diamond_a q$ is not true in $Y$, where the latter fails because $\diamond_a q$ is not true in both states of $Y$. In other words it is not the case that there is $(\exists)$ a set of neighbours in the neighbourhood of state 10 such that for all $(\forall)$ states in that set $\diamond_a q$ is true.

Note that the non-monotonic logician would write [*a*]φ for ⟨a⟩φ [86], focussing on the
∀ of ∃∀, not ⟨a⟩φ as we do, focussing on the ∃ of ∃∀ and in that way on our storyline for
CAL.

The logic CAL was a main focus of investigation in various related works involving Rustam Galimullin [71, 68, 76, 74]. They contain an axiomatization for CAL with an additional auxiliary operator bundling an announcement by agents in *G* with a quantification over a announcement by agents not in *G*. This technical device then facilitates proving completeness for the axiomatization.

The axiomatization of CAL with only the coalition quantifiers ⌜!_G⌝ remains an open question.

The undecidability (of satisfiability) of CAL is shown in [6], in an integrated setting also including APAL and GAL (and that simplifies prior proofs of undecidability for APAL [70] and GAL [5]). The PSPACE complexity of model checking is shown in [77], and its lack of the finite model property in [141].

4.4 Expressivity of GAL and CAL

The logics GAL and CAL are related in interesting ways. As mentioned in Example 9, if
all agents *A* together can achieve *φ* in GAL, then obviously as well in CAL, as there are
no remaining agents to counteract it:

$$ \langle !_A \rangle \varphi \rightarrow \langle !_A \rangle \varphi $$

On the other hand, if the empty coalition $\emptyset$ can achieve $\varphi$ in CAL, then $\varphi$ will be true after any GAL announcement:

$$ \langle !_\emptyset \rangle \varphi \rightarrow [!_A] \varphi $$

Continuing along that line, as this is equivalent to $\langle !_\emptyset \rangle \varphi \rightarrow \langle !_\emptyset \rangle [!_A] \varphi$, it was conjectured [137] that the CAL quantifier might be definable in terms of the GAL quantifier as follows.

$$ \langle !_G \rangle \varphi \leftrightarrow \langle !_G \rangle [!_{A \setminus G}] \varphi $$

This schema can be paraphrased as follows:

There is something that the agents in G can say no matter what the agents not in G say simultaneously and after which $\varphi$, iff there is something that the agents in G can say no matter what the agents not in G say subsequently and after which $\varphi$.

If the conjecture had been true, GAL would have been at least as expressive as CAL, because we can then see the language of GAL as a fragment of the language of CAL. Then, showing that GAL is as expressive as CAL would have seemed within reach. However, the conjecture is false [74]. It is false because non-bisimilar states can become bisimilar after an announcement (we recall the discussion on APAL with memory [31] in Section 3.5.4 on page 22). The agents not involved in that announcement are then no longer able to distinguish between those states in a subsequent announcement. However, they might have been able to prevent such states becoming indistinguishable if they could have made a simultaneous announcement, as in the following example.

**Example 11** Consider the models below for a single variable $p$. As before, $p$ is false in the 0 states and true in the 1 states. As usual we assume transitivity of the accessibility relation. Note that in model $M$ formula $\square_a \neg p$ is distinguishing for state $v$.

$$ M: \quad \begin{array}{cccccccccc} u' & ac & t' & a & s & a & t & ac & u & b & v \\ 1 & & 0 & & 1 & & 0 & & 1 & & 0 \end{array} $$

$$ N: \quad \begin{array}{c} 0 \\ \hline a \end{array} \quad \begin{array}{c} 1 \\ \hline a \end{array} \quad \begin{array}{c} 0 \\ \hline ac \end{array} \quad \begin{array}{c} 1 \end{array} $$

$$ M | \diamond_a p: \quad \begin{array}{c} 1 \\ \hline ac \end{array} \quad \begin{array}{c} 0 \\ \hline a \end{array} \quad \begin{array}{c} 1 \\ \hline a \end{array} \quad \begin{array}{c} 0 \\ \hline ac \end{array} \quad \begin{array}{c} 1 \end{array} $$

$$ \begin{array}{c} 1 \\ \hline a \end{array} \quad \begin{array}{c} 0 \\ \hline ac \end{array} \quad \begin{array}{c} 1 \end{array} $$

We will now sketch the proof that

$$ M_s \models [!_a] \langle !_{bc} \rangle \quad (\diamond_a \square_c \neg p \wedge \diamond_a \square_c p \wedge \diamond_a \neg (\square_c p \vee \square_c \neg p)) $$

$$ M_s \models [\langle !_a \rangle] \quad (\diamond_a \square_c \neg p \wedge \diamond_a \square_c p \wedge \diamond_a \neg (\square_c p \vee \square_c \neg p)) $$
from which follows that $\langle !_G \rangle \varphi \leftrightarrow \langle !_G \rangle [!_{A\setminus G}] \varphi$ is not valid for all $\varphi$, A and G.

The first is the case because if a announces ⋄<sub>a</sub>p (as depicted), in model M|∇<sub>a</sub>p states t and t', and u and u', are bisimilar. The bisimulation contraction is shown below it. After that announcement by a, agents b and c can no longer make the formula ⋄<sub>a</sub>□<sub>c</sub>¬p ∧ ∇<sub>a</sub>□<sub>c</sub>p ∧ ∇<sub>a</sub>¬(□<sub>c</sub>p ∨ □<sub>c</sub>¬p) true. That formula describes that a considers possible three c-equivalence classes, including one where c is uncertain and that therefore requires at least two states. Altogether we therefore need a model with at least four states. But the contraction of M|∇<sub>a</sub>p contains three states, which is not enough.

Whereas if they can make their announcement simultaneously with *a*, they can still use that *u* and *u'* are different. If *a* again were to announce ∇<sub>a</sub>p, *b* can simultaneously announce ϕ<sub>b</sub> := ¬□<sub>b</sub>(p ∧ ¬(□<sub>c</sub>p ∨ □<sub>c</sub>¬p)) (*ϕ*<sub>b</sub> is only false in *M*<sub>*u*'</sub>) and *c* can simultaneously announce ⊤ (i.e., □<sub>c</sub>⊤). From this joint announcement by *a*, *b*, *c* model *N* results, in which ∇<sub>a</sub>□<sub>c</sub>¬p ∧ ∇<sub>a</sub>□<sub>c</sub>p ∧ ∇<sub>a</sub>¬(□<sub>c</sub>p ∨ □<sub>c</sub>¬p) is true. The only other announcement *a* can initially make in state *s* is ⊤, and then *b* and *c* can also enforce *N*, by respective announcements ϕ<sub>b</sub> and ¬□<sub>c</sub>□<sub>a</sub>¬p (of which the negation is only true in *M*<sub>*v*</sub>).

Example 11 is a simple demonstration of the differences between GAL and CAL. But it is not an expressivity proof. In [68] it is shown that GAL is not at least as expressive as CAL. That proof is not so simple. It is unknown whether CAL is at least as expressive as GAL. A corollary in [68] is that GAL is not at least as expressive as APAL. In [3] it was already shown that APAL is not at least as expressive as GAL. Therefore, GAL and APAL are incomparable [68, Theorem 5.6].

Finally, we recall the structures with ‘memory’ of the initial information state that
allow to continue to distinguish states that have become bisimilar after announcement.
Section 3.5.4 presented the logic APALM with that memory feature. In the journal version
[32] of [31] and in the journal version [8] of [68] the logics GAL and CAL are extended
with memory as in APALM, resulting in GALM and CALM, and it is then shown that the
CAL quantifier is now after all definable with the GAL quantifier as $\langle !_G \rangle \varphi \leftrightarrow \langle !_G \rangle [!_{A\setminus G}] \varphi$.

**4.5 Applications**

**Agency** The expression $\langle !_G \rangle \varphi$ has the smell of 'group of agents $G$ is able to achieve $\varphi'$, such that, taking a single agent, $\Box_a \langle !_a \rangle \varphi$ (on S5 models) seems to formalize that agent $a$ knows that she is able to achieve $\varphi$, as in logics combining agency and knowledge [93, 2, 133]. These are tricky issues in the setting for group announcements. In dynamic epistemic logics it has been proposed to define 'knowledge de re' as 'there is an announcement which $a$ knows will achieve the goal', and 'knowledge de dicto' as '$a$ knows that there is an announcement which will achieve the goal' [3]. As required for such de re / de dicto distinctions, in the former a specific witness formula is required, whereas in the latter the witness formula may be different for each state that agent $a$ considers possible. The intuitive descriptions match the GAL formalizations $\langle !_a \rangle \Box_a \varphi$ respectively $\Box_a \langle !_a \rangle \varphi$ [3, Prop. 26]. Given this identification the following results can then be obtained (see [4] and [3, Prop. 27]):
• $\Box_a \langle!_a\rangle \varphi \to \langle!_a\rangle \varphi$ is valid.

‘If you know that you can do something, you can do it.’

• $\langle!_a\rangle \Box_a \varphi \to \Box_a \langle!_a\rangle \varphi$ is valid.

‘Knowledge de re implies knowledge de dicto’. Also valid is $\langle!_a\rangle \Box_a \varphi \to \Box_a \langle!_a\rangle \Box_a \varphi$.

• $\Box_a \langle!_a\rangle \varphi \to \langle!_a\rangle \Box_a \varphi$ is not valid.

‘Knowledge de dicto does not imply knowledge de re’.

In different states, different announcements may be required to make $\varphi$ true. As you do not know what the actual state is, you therefore do not know what announcement makes $\varphi$ true in the actual state. You only know that in all states that you consider possible there is an announcement that makes $\varphi$ true. For example, in state s formula $\varphi$ is true after you announce p but not after you announce q; in indistinguishable state t formula $\varphi$ is true after you announce q but not after you announce p. Should you announce p or should you announce q? You are not able to achieve $\varphi$!

**Security** Given that $\langle!_G\rangle \langle!_G\rangle \varphi \to \langle!_G\rangle \varphi$ is valid in GAL (see above), and that we can iterate this result for any finite sequence of announcements by group G, we can formalize communication protocols consisting of finite executions in GAL. This includes communication protocols where agents take turns in saying something. If a announces $\varphi$ and subsequently b announces $\psi$, we can also see this as: a announces $\varphi$ and simultaneously b announces $\top$ (keeps quiet), and subsequently, a announces $\top$ and simultaneously b announces $\psi$. Of particular interest seems the formalization of security protocols executed by two principals Alice a and Bob b in the presence of an eavesdropper Eve e — in such protocols the agents sending each other messages are the principals, and an eavesdropper is, not surprisingly, an agent intercepting (‘hearing’) a message. If $\varphi$ is some epistemic goal (information goal) and $\psi$ is a security constraint that needs to be preserved throughout the execution, a finite protocol for a and b to learn the secret safely should observe

$$ \psi \to \langle!_{ab}\rangle (\varphi \wedge \psi) \qquad (i) $$

A typical example is whether in cards cryptography, given a commonly known deck of cards dealt over three players (where each player can only see her own cards), players Alice and Bob can learn the card deal by sending public messages (announcements) to each other, without Eve learning the card deal [136]. Part of the problem specification would then be, where $0_a$ stands for ‘Alice holds card 0’:

$$ 0_a \to \langle!_{ab}\rangle (\Box_b 0_a \wedge \neg (\Box_c 0_a \vee \Box_c \neg 0_a)) \qquad (ii) $$

As GAL and APAL have incomparable expressivity, we conjecture that (i) is not formalizable in APAL. The shadow of doubt is that the incomparability proof in [68] uses three agents. It therefore holds for more agents, but maybe not for less, and (i) only requires two communicating agents. Then again, what does safety for two agents mean anyway without the presence of a third agent who is the eavesdropper, as in (ii)?
**Coalition logic, and playability** The following axioms of coalition logic [112] are validities of coalition announcement logic CAL [4].

$$ (\langle!_G\rangle\varphi \wedge [\!_H\rangle\varphi') \rightarrow \langle!_{G\cup H}\rangle(\varphi \wedge \varphi') \quad \text{if } G \cap H = \emptyset \\ [\!_\emptyset\rangle\varphi \rightarrow \langle!_A\rangle\varphi $$

The second already featured in this section. The first formalizes that if two disjoint groups can independently bring about $\varphi$ respectively $\varphi'$, then they can jointly bring about $\varphi \wedge \varphi'$. If the groups are not disjoint, that may no longer be the case, as an agent in the intersection may have do $x$ to bring about $\varphi$ but may have to do $y \neq x$ to bring about $\varphi'$.

There are also relations to game logic [110, 113] and also to the forcing operator $\{G\}$ proposed in [123] that quantifies over strategies in extensive games (where a strategy is a sequence of moves); see also [128]. For a single agent $i$, $\{i\}\varphi$ is true if “player $i$ has a strategy for playing [the] game which forces a set of outcomes all of which satisfy $\varphi$” [123]. As $\langle!_G\rangle$ models what coalition $G$ can achieve/force in any finite sequence of moves, this is akin to the extensive game setting in [123]. However, there are issues. The schema $\{G\}\{G\}\varphi \rightarrow \{G\}\varphi$ is valid for the forcing operator. But although $\langle!_G\rangle\langle!_G\rangle\varphi \rightarrow \langle!_G\rangle\varphi$ is valid in GAL, it is unknown whether $\langle!_G\rangle\langle!_G\rangle\varphi \rightarrow \langle!_G\rangle\varphi$ is valid in CAL [71, page 45].

## 4.6 Open problems and further research

The relation of GAL and CAL to (epistemic extensions of) logics of agency such as ATL [9] and STIT [92] seems worth investigating. A logic much like CAL but in an ATL-setting with therefore an explicit notion of agency, including a complete axiomatization, was proposed by de Lima in [51, 52, 53].

More recent investigations building forth upon the logics GAL and CAL, in areas as diverse as abstract argumentation and strategic voting, include [72, 111, 168, 118, 56]. A group announcement logic for ignorance (with ignorance modalities instead of knowledge modalities as epistemic primitives) is presented in [60].

For comparisons with logics as STIT and ATL we should keep in mind that GAL and CAL do not have factual change, which makes such a comparison restricted. Then again, also in dynamic epistemic logics one can model factual change and quantify over that, which we will address in Section 8 on epistemic planning.

Open problems about GAL and CAL include:

* What is the complete axiomatization of CAL? [76]

* Is GAL at least as expressive as CAL? [68, 8]

* How does CAL with public factual change relate to epistemic extensions of logics of agency?
# 5 Quantifying over action models

In this section we are moving from quantifying over public announcements to quantifying over arbitrary epistemic actions, such as private announcements. We recall that already for PAL the term ‘announcement’ is somewhat questionable. And even more so for non-public information change. However, a constant throughout dynamic epistemic logics is that a model update is induced by an epistemic action, and that an epistemic action needs to satisfy a precondition formula. We simply continue to call this formula the announcement. But it can then be private instead of public. Whether there is an epistemic action after which a proposition is true, is then still the same as what is to be announced in order to make that proposition true.

## 5.1 Arbitrary action model logic

In the logic APAL we quantify over announcements, i.e., public events. We can also quantify over events that may not be public, where the obvious suspect is to quantify over action models. This was observed in [25, Section 5], including the obvious semantics, but only truly realized in various works involving James Hales [83, 69, 84], where our presentation follows [83].

We expand the language $\mathcal{L}(\diamond, \otimes)$ of action model logic with a quantifier $\langle \otimes \rangle$ with the following semantics, where $E_e$ is an epistemic action, and where $M$ is a $\mathcal{K}$ model (the results in this section are typically not for $\mathcal{S5}$ models).

$$M_s \models \langle \otimes \rangle \varphi \quad \text{iff} \quad \text{there is a } E_e \text{ with quantifier-free preconditions such that } M_s \models \langle E_e \rangle \varphi$$

We call the resulting logic AAML, for arbitrary action model logic. We recall that in APAL the quantifier over announcements adds expressivity and causes undecidability of satisfiability. It may therefore come as a surprise that in AAML the quantifier does not add expressivity and does not cause undecidability. The logic AAML is as expressive as action model logic AML (and therefore as expressive as the logic K), because the quantifier $\langle \otimes \rangle$ can be eliminated by reduction axioms. We recall from Section 2 that such a reduction axiom has the shape of an equivalence between two formulas $\varphi_1$ and $\varphi_2$ such that a subformula of $\varphi_1$ bound by a quantifier is (strictly) more complex than any subformula of $\varphi_2$ bound by that quantifier, or such that that quantifier no longer occurs in $\varphi_2$. Every formula with quantifiers can then be reduced (rewritten) to an equivalent formula without quantifiers. The technique to reduce AAML is borrowed from another logic, refinement modal logic, and therefore we will only discuss it section 7 devoted to that logic.

Because AAML is as expressive as AML by way of a reduction, this logic AAML also allows synthesis. This we will now discuss.

**Synthesis** Logics with quantifiers over information change sometimes allow synthesis. There are (at least) two kinds of synthesis in a dynamic epistemic logic. The logic need not have quantifiers over information change. In the local synthesis problem, given an
epistemic model $M_s$ and a formula $\varphi$, the problem is whether there exists an epistemic action $\alpha$ (such as a pointed action model $E_e$, but we will later also consider other epistemic actions) such that $M_s \models \langle\alpha\rangle\varphi$. In the global synthesis problem, given a formula $\varphi$, the problem is whether there exists an epistemic action $\alpha$ such that whenever $M_s \models \langle\beta\rangle\varphi$ for some epistemic action $\beta$, then also $M_s \models \langle\alpha\rangle\varphi$. In a logic with a quantifier $\langle\bullet\rangle$ for information change due to such $\beta$s, global synthesis amounts to the validity of the schema $\langle\bullet\rangle\varphi \leftrightarrow \langle\alpha\rangle\varphi$. From here on, by synthesis we mean global synthesis. Not all dynamic epistemic logics allow synthesis, for example, PAL does not. The somewhat trivial reason for this failure is that we cannot make a typical disjunction of epistemic parts, such as $\Box_a p \vee \Box_a \neg p$, always true: we would have to choose between the announcement $p$ and the announcement $\neg p$. Although correct, this is somewhat trivial, because allowing the ‘test’ of the value of $p$, that is, non-deterministic choice between the announcements $p$ and $\neg p$, would solve the problem for this example. Such a program would amount to a two-pointed action model, with preconditions $p$ respectively $\neg p$, and where all agents can distinguish the two actions.

Clearly, a dynamic epistemic logic with quantifiers can only allow synthesis if the quantifier can be eliminated by a reduction, so that any formula with quantifiers is equivalent to a formula without. So for APAL, we need not even think about synthesis, as APAL is (strictly) more expressive than PAL (Section 3).

The logic AAML allows synthesis [83]. More specifically, given $\langle\otimes\rangle\varphi$, where $\varphi$ is quantifier-free, there is a multi-pointed action model $E_T$ (where $T \subseteq \mathcal{D}(E)$) such that $\langle\otimes\rangle\varphi \leftrightarrow (E_T)\varphi$ is valid: given any formula $\varphi \in \mathcal{L}(\diamond, \otimes)$ we can synthesize an action model $E_T$, that is finite, and with quantifier-free preconditions, such that, whenever there is an action model such that after its execution $\varphi$ is true, then $E_T$ can also be executed to make $\varphi$ true. We cannot always synthesize a single-pointed action model $E_t$. It may have to be multi-pointed, as for the disjunctive epistemic goal $\varphi = \Box_a p \vee \Box_a \neg p$ above. By an easy induction over the number of quantifiers in a formula we can also lift the restriction that $\varphi$ be quantifier-free. It can be any formula in $\mathcal{L}(\diamond, \otimes, \langle\otimes\rangle)$.

Because there is synthesis for AAML, and because in an actual state $s$ some $e \in T$ of the synthesized $E_T$ will execute, the logic satisfies that

$$ M_s \models \langle\otimes\rangle\varphi \quad \text{iff} \quad \text{there is a } E_e \text{ such that } M_s \models \langle E_e\rangle\varphi \quad (i) $$

without any language restriction. Note that (i) is a property of the semantics and does not define the semantics of $\langle\otimes\rangle$, as in the beginning of this subsection. We cannot have (i) be the semantics of the quantifier, as $\langle\otimes\rangle\varphi$ itself can then be a precondition formula of action model $E$. We recall from Section 3.5 a similar result for fully arbitrary public announcement logic [158].

**Axiomatization** The axiomatization of AAML in [83] is somewhat indirect, as it uses a translation into refinement modal logic [45]. This translation involves replacing the AAML quantifier by the refinement quantifier, and some additional arguments around action models. Also, the [83] presentation has parameterized quantifiers $\langle\otimes_G\rangle$ for $G \subseteq A$
instead of a single quantifier $\langle \otimes \rangle$, for technical reasons to make the translation work. We therefore do not give the axiomatization in this section but only in Section 7 on refinement modal logic. We do not know any results on the complexity of satisfiability of AAML.

## 5.2 Variations

We describe two variations on arbitrary action model logic. They outline ideas for future research rather than survey published work.

**Quantifying over actions with a fixed precondition** A public announcement $\varphi$ is an event identically observed by all agents, corresponding to a singleton action model with precondition $\varphi$ and with the single action accessible for all agents (so the relation is reflexive, and the action model in class S5). Now consider any epistemic action with precondition $\varphi$. For example, any way that Anne can inform Bill of p, no matter whether this is private or public, whether a third agent Cath learns about it or not, and so on. Consider an additional inductive language construct $\langle \varphi^{\otimes} \rangle \psi$ for ‘after any action informing the agents of $\varphi$, $\psi$ (is true)’. Its semantics therefore are

$$M_s \models \langle \varphi^{\otimes} \rangle \psi \quad \text{iff} \quad M_s \models \varphi \wedge \langle \otimes \rangle \psi$$

or, alternatively but equivalently,

$$M_s \models \langle \varphi^{\otimes} \rangle \psi \quad \text{iff} \quad \text{there is a } E_e \text{ with quantifier-free preconditions such that} \\ \qquad \mathbf{pre}(e) = \varphi \text{ and } M_s \models \langle E_e \rangle \psi$$

Such a quantification was suggested in [18]. This was based on the similar [17], that proposed instead of action models an *action language*, on a par with the static language. Another somewhat similar quantification is found in [52], but for coalitional actions. The settings of [18, 17, 52] use a different language than here, but inspired this presentation.

We now show that $\langle \otimes \rangle$ and $\langle \varphi^{\otimes} \rangle$ are interdefinable.

It is clear that $\langle \varphi^{\otimes} \rangle$ is definable in the language $\mathcal{L}(\diamond, \otimes, \langle \otimes \rangle)$. Its semantics provide the definition:

$$\langle \varphi^{\otimes} \rangle \psi := \varphi \wedge \langle \otimes \rangle \psi$$

It is not so clear that $\langle \otimes \rangle$ is also definable in the language $\mathcal{L}(\diamond, \otimes)$ expanded with the $\langle \varphi^{\otimes} \rangle$ modalities, as these modalities appear to have an aspect of bundling/packing [163]. Semantically, we now want that: $\langle \otimes \rangle \psi$ iff (there is a $\varphi$ such that $\langle \varphi^{\otimes} \rangle \psi$). This is where (global) synthesis comes in handy: the AAML validity $\langle \otimes \rangle \psi \leftrightarrow \langle E_T \rangle \psi$, wherein multi-pointed action model $E_T$ is synthesized from the given formula $\psi$. Consider the following argument:

If $M_s \models \langle \otimes \rangle \psi$, then by global synthesis $M_s \models \langle E_T \rangle \psi$, so that there is a $t \in T$ for which $M_s \models \langle E_t \rangle \psi$. From this we obtain that $M_s \models \mathbf{pre}(e)$ and also that $M_s \models \langle \otimes \rangle \psi$, and from both we obtain $M_s \models \mathbf{pre}(t) \wedge \langle \otimes \rangle \psi$, that is, $M_s \models \langle \mathbf{pre}(t)^{\otimes} \rangle \psi$. Therefore $M_s \models \bigvee_{t \in T} \langle \mathbf{pre}(t)^{\otimes} \rangle \psi$.
Vice versa, if $M_s \models \bigvee_{t \in T} \langle \mathbf{pre}(t)^{\otimes} \rangle \psi$, then there is a $t \in T$ such that $M_s \models \langle \mathbf{pre}(t)^{\otimes} \rangle \psi$, and therefore, by the definability of $\langle \varphi^{\otimes} \rangle \psi$, we get $M_s \models \mathbf{pre}(t) \wedge \langle \otimes \rangle \psi$, from which it follows that $M_s \models \langle \otimes \rangle \psi$.

We can therefore define $\langle \otimes \rangle \psi$ as

$$ \langle \otimes \rangle \psi := \bigvee_{t \in T} \langle \mathbf{pre}(t)^{\otimes} \rangle \psi $$

It might be worthwhile to explore in depth such an action model logic for epistemic actions with given precondition.

**Quantifying over private group announcements** We recall group announcement logic GAL where we quantify over known announcements simultaneously made by the agents in group $G \subseteq A$, and coalition announcement logic CAL where we quantify over known announcements simultaneously made by the agents in group $G \subseteq A$ no matter what (known) announcements are also simultaneously made by the agents not in $G$. We can also consider such quantifications over any informative action 'involving agents in $G'$. That is, announcements only made by the agents in $G$ and that may not be public. Under such conditions of partial observability we require that agents make the same announcement in for them indistinguishable actions. This then represents that they know what they say. Analogously to the GAL and CAL quantifiers over joint public announcements by agents, we could then consider quantifiers over $S_5$ action models satisfying that constraint. Let us merely give an example of such an epistemic action.

**Example 12** Consider four agents Anne, Bill, Cath, and Dave. Anne and Bill have joint access to a bank account (or a nuclear storage facility, whatever ...) by a secret code. Anne's secret code $p$ is only known to her and Bill's secret code $q$ is only known to him. They want to transfer their codes to Cath and Dave, respectively, without making them public. Clearly, the way to do this is that Anne privately informs Cath, and Bill privately informs Dave, and such that these actions are commonly known to all. Let $Kw_i\varphi$ (for 'agent $i$ knows whether $\varphi'$) abbreviate $\Box_i\varphi \vee \Box_i\neg\varphi$. Then the specification of the problem is that

$$ (Kw_a p \wedge \neg Kw_b p \wedge Kw_b q \wedge \neg Kw_a q) \rightarrow \langle \otimes_{ab} \rangle (Kw_c p \wedge Kw_d q \wedge \neg Kw_a q \wedge \neg Kw_c q \wedge \neg Kw_b p \wedge \neg Kw_d p) $$

The $\langle \otimes_{ab} \rangle$ quantifier informally represents that $a, b$ can simultaneously (that is, independently) make a private announcement, similarly to the $\langle !_{ab} \rangle$ quantifier in GAL wherein $a, b$ simultaneously make a public announcement. An epistemic action witnessing this $\langle \otimes_{ab} \rangle$ quantifier, that satisfies that Anne and Bill know what they say, is:

$$ \begin{array}{c} \Box_a \neg p \wedge \Box_b q \quad \frac{bd}{ac} \quad \Box_a p \wedge \Box_b q \\ \Box_a \neg p \wedge \Box_b \neg q \quad \frac{bd}{ac} \quad \Box_a p \wedge \Box_b \neg q \end{array} $$
We omit the semantics for such action models and quantifiers from the survey. We conjecture that such logics with quantifiers over possibly private actions by groups of agents have complete axiomatizations with reduction axioms eliminating all dynamic features.<fnref n="6" />

## 5.3 Open problems and further research

The list of open problems for APAL and its variations, and for GAL and CAL, is longer and much more specific than the list below. This is more a feature than a problem: the logics in this section all permit reduction, so that they are decidable and as expressive as the base logic (K or S5). However, they presumably have widely varying complexities for satisfiability, model checking, synthesis, or planning. It may also be that the intuitions for action model dynamics are harder to grasp than for announcements, despite quantifying over the former being easier than quantifying over the latter.

* Synthesis for action model logic, for S5 epistemic models and S5 action models [83].

* The axiomatization of the logic with quantification over private group announcements.

# 6 Arrow updates

In public announcement logic an updated model has a restricted domain, and this is not different in action model logic, where the update is a domain-restricted modal product. Instead of domain restrictions we can also consider updating models by restricting accessibility relations. Already in the 1990s, relational restrictions have been the basis for dynamic epistemic logics [79]. We focus on the more recent arrow update logic AUL [95] (see also [98, 97]) and arrow update model logic AUML [96], for both of which versions with quantification over information change have been proposed [156, 159, 157].

Such relation-changing logics are more focussed on belief and belief change than on knowledge and knowledge change (you believe what holds in all accessible states, which may exclude the actual state). But we will see that arrow update logics also model knowledge change. Arrow updates may then be more succinct than action models with the same update effect [95].

For domain as well as relational restrictions we principally have those in mind that are with respect to modally definable subsets, i.e., denotations of formulas in $\mathcal{L}(\diamond)$. Other restrictions are addressed in Section 9.

## 6.1 Arrow update logics

A pair in the accessibility relation of an epistemic model is also called an arrow. Indeed it is common to denote $(s, t) \in R$ (or $Rst$) as $s \to t$, where the ‘$\to$’ symbol resembles an arrow.

<footnote n="6">⁶Namely by combining features of the axiomatizations of refinement epistemic logic [85] (see Section 7, later), of AAML (see above), and of certain arrow update logics [157] (see Section 6, next).</footnote>
State *s* is the *source* of the arrow and *t* is the *target* of the arrow. In *arrow update logic* (AUL) [95] one specifies which arrows are preserved, by way of specifying what formulas should be satisfied at the source (state) of the arrow and the target (state) of the arrow. This determines the model transformation. It is called an *arrow update*. The logic AUL contains modalities for arrow updates.

While restricting the relations, in AUL the domain remains the same. There is also a version of arrow update logic wherein updated models can have larger modal complexity and in particular larger domains (representing higher-order uncertainty among the agents over the information change): just as action model logic is a generalization of public announcement logic, generalized arrow update logic or arrow update model logic AUML has been proposed in [96] as a generalization of AUL. It contains modalities for arrow update models.

We will present both logics simultaneously by way of presenting arrow update model logic and defining arrow update logic as a special case.

**Arrow update model** Given a logical language $\mathcal{L}$, an arrow update model $U$ is a pair $(O, RR)$ where $O$ is a non-empty domain (set) of outcomes (also denoted $\mathcal{D}(U)$) and where $RR$ is an arrow relation $RR: A \to \mathcal{P}((O \times \mathcal{L}) \times (O \times \mathcal{L}))$.

For each agent $a$, the arrow relation links (outcome, formula) pairs to each other. We write $RR_a$ for $RR(a)$, and we write $(o, \varphi) \to_a (o', \varphi')$ for $((o, \varphi), (o', \varphi')) \in RR_a$, or even, if the outcomes are unambiguous, $\varphi \to_a \varphi'$. Formula $\varphi$ is the *source condition* and formula $\varphi'$ is the *target condition* of the $a$-labelled arrow from *source o* to *target o'*. The arrow updates of AUL [95] correspond to singleton pointed arrow update models. So in that case we can indeed write $\varphi \to_a \varphi'$, as there is just one outcome.

Given an epistemic model $M = (S, R, V)$ and an arrow update model $(O, RR)$, the updated model $M * U = (S', R', V')$ is defined as follows, where $p \in P$, $a \in A$, $s, s' \in S$, and $o, o' \in O$:

$$ 
\begin{array}{lclcl}
S' & = & S \times O & & \\
((s, o), (s', o')) \in R'_{a} & \text{iff there are } \varphi, \varphi' \in \mathcal{L} \text{ such that:} & & & \\
& & (s, s') \in R_{a}, (o, \varphi) \to_{a} (o', \varphi'), M_{s} \models \varphi, \text{ and } M_{s'} \models \varphi' & & \\
V'(p) & = & V(p) \times O & &
\end{array}
$$

Example 13 demonstrates how to execute an arrow update for a singleton arrow update model with three arrows.

**Example 13** Given initial uncertainty about *p* for two agents Anne and Bill, a typical arrow update is the action wherein Anne (*a*) opens an envelope containing the truth about *p* while Bill (*b*) observes Anne reading the contents of the letter. We preserve all arrows satisfying one of $p \to_a p, \neg p \to_a \neg p$, and $\top \to_b \top$.<fnref n="7" /> Therefore, only two arrows disappear, $\neg p \to_a p$ and $p \to_a \neg p$. It is depicted below, including the equivalent simplified visualization, for which it is harder to determine the update as the arrows are not explicit.

<footnote n="7">⁷Formally, given arrow update model $\{\{o\}, RR\}$, we have that $RR(a) = \{( (o, p), (o, p)), ((o, \neg p), (o, \neg p)) \}$ and $RR(b) = \{( (o, \top), (o, \top)) \}$.</footnote>
<figure><img src="image_6.png" /></figure>

Just as in action model logic, we wish to have a logical language and semantics with modalities for arrow updates, which requires their inclusion in an inductive definition of the logical language, subject to certain constraints in order to keep the language well-defined.

**Syntax and semantics** The language $\mathcal{L}(\diamond, \uparrow)$ of arrow update model logic AUML has an additional inductive construct $\langle U_o \rangle \varphi$ where $U = (O, RR)$ with $o \in O$ is an arrow update model with $O$ finite and with $RR_a$ finite for all $a \in A$, and with source and target conditions that have already inductively been defined as formulas. We read $\langle U_o \rangle \varphi$ as ‘after executing arrow update $U_o$, $\varphi$ (is true)’.

In order to distinguish arrow update logic AUL from arrow update model logic AUML the language for singleton arrow update models is called $\mathcal{L}(\diamond, \uparrow_1)$.

Given a pointed epistemic model $M_s$ and a pointed arrow update $U_o$, the semantics for the arrow update modality are as follows.

$$M_s \models \langle U_o \rangle \varphi \quad \text{iff} \quad (M * U)_{(s,o)} \models \varphi \quad \text{where } M * U \text{ is defined as above}$$

The arrow update modality is self-dual: $\langle U_o \rangle \varphi \leftrightarrow [U_o] \varphi$. AUML is as expressive as the base modal logic K, because every formula in $\mathcal{L}(\diamond, \uparrow)$ is equivalent to a formula in $\mathcal{L}(\diamond)$, by a reduction. The crucial reduction axiom is as follows. The conjunction is over all ‘arrows’ for agent $a$ between outcomes $o$ and $o'$ in the domain of $U$. We recall that there can be multiple arrows for each agent, such as the two arrows for agent $a$ in Example 13.

$$[U_o] \Box_a \varphi \leftrightarrow \bigwedge_{(o, \psi) \to_a (o', \psi')} (\psi \to \Box_a (\psi' \to [U_{o'}] \varphi))$$

As an arrow update is a singleton arrow update model, this is also the reduction axiom for AUL. And just like AUML, also AUL is as expressive as K. A relevant detail concerning the respective reductions showing this, is that the composition of two arrow update models is again an arrow update model, which is fairly obvious ([96], details omitted), and that the composition of two arrow updates (singleton arrow update models) is again an arrow update, which is less obvious ([95, Def. 3.1]). Let us at least sketch the idea: if $\varphi \to_a \psi$ is in the first arrow update, called $U_o$, and $\varphi' \to_a \psi'$ is in the second arrow update, then $\varphi \wedge [U_o] \varphi' \to_a \psi' \wedge [U_o] \psi'$ is an arrow in their composition. We note that the arrow in the composition is again with respect to the same, unique, outcome $o$.

Results for arrow update logics are for class $\mathcal{K}$ and not for class $\mathcal{S}5$. It is unknown how to obtain complete axiomatizations when restricting oneself to updates between models with equivalence relations. However, the $\mathcal{S}5$ version of refinement modal logic, called refinement epistemic logic, that will be presented in Section 7.2, gives reason for optimism. Arrow update logic AUL is more succinct than action model logic AML in the somewhat
informal sense that certain arrow updates are exponentially smaller than action models with the same update effect [95]. We call it informal because a (typically technically quite involved) proof of the result is lacking, although we conjecture that it holds.

Intuitively, AUML and AML come close, they are interchangeable formalisms for modelling multi-agent system dynamics, where it is hard to say where one ‘should be’ preferred over the other. When restricted to S5 models, the arrow updates of the logic AUL come intuitively very close to what are known as semi-public announcements (also known as semi-private — is a glass half empty or is it half full?), such as when Alice shows her card to Bob only, with Cath watching [135].

## 6.2 Arbitrary arrow update logics

A quantifier-free arrow update model is an arrow update model with all source and target conditions in $\mathcal{L}(\diamond, \uparrow)$. We obtain arbitrary arrow update logic AAUL by adding an additional inductive construct $\langle\uparrow_1\rangle$ to language $\mathcal{L}(\diamond, \uparrow)$, thus obtaining language $\mathcal{L}(\diamond, \uparrow, \langle\uparrow_1\rangle)$, and with semantics

$$M_s \models \langle\uparrow_1\rangle\varphi \quad \text{iff} \quad \text{there is a quantifier-free singleton } U_o \text{ such that } M_s \models \langle U_o\rangle\varphi$$

Similarly, we obtain arbitrary arrow update model logic AAUML by adding an additional inductive construct $\langle\uparrow\rangle$ to language $\mathcal{L}(\diamond, \uparrow)$, thus obtaining language $\mathcal{L}(\diamond, \uparrow, \langle\uparrow\rangle)$, and with semantics

$$M_s \models \langle\uparrow\rangle\varphi \quad \text{iff} \quad \text{there is a quantifier-free } U_o \text{ such that } M_s \models \langle U_o\rangle\varphi$$

The logic AAUL has a complete axiomatization, is more expressive than the logic K, is incomparable in expressivity to APAL [156], and it is undecidable [159]. Also, the model checking problem is PSPACE-complete, as for APAL.

The logic AAUML also has a complete axiomatization, is as expressive as the logic K (by a reduction), and it is therefore decidable [157]. The complexity of satisfiability and of model checking are unknown. The crucial reduction axiom of AAUML is as follows, where for each agent $a$, $\Phi_a$ is a set of formulas in $\mathcal{L}(\diamond, !, \langle\uparrow\rangle)$ with typical members $\varphi_a$.<fnref n="8" />

$$\langle\uparrow\rangle \bigwedge_{a \in A} \left( \bigwedge_{\varphi_a \in \Phi_a} \Diamond_a \varphi_a \wedge \Box_a \psi_a \right) \leftrightarrow \bigwedge_{a \in A} \bigwedge_{\varphi_a \in \Phi_a} \Diamond_a \langle\uparrow\rangle (\varphi_a \wedge \psi_a) \quad (*)$$

If the quantifier binds a conjunction containing a Boolean formula, one uses that facts do not change in this logic, that is, that $\langle\uparrow\rangle\varphi_0 \leftrightarrow \varphi_0$ is valid for Booleans $\varphi_0$. Altogether we can treat any conjunction bound by a quantifier and again we have a reduction. A different incarnation of axiom (*) will feature in the next Section 7 on refinement modal logic.

<footnote n="8">⁸These formulas are also required to be in a particular form called ‘disjunctive negation normal form’, DNNF, such that negations are only binding atoms. It can be shown that each formula in $\mathcal{L}(\diamond, !, \langle\uparrow\rangle)$ is equivalent to a formula in DNNF, so this is not restrictive. See [157] for details.</footnote>
**Synthesis** The logic AAUML permits (global) synthesis: given $\varphi \in \mathcal{L}(\diamond, \uparrow)$, there is an arrow update model $U_o$ (with a single point) such that $\langle\uparrow\rangle\varphi \leftrightarrow \langle U_o \rangle\varphi$ is valid. We recall from the previous section that AAML permits synthesis as well, with the difference that one can only synthesize a multi-pointed action model from a given formula, not necessarily a single-pointed one.

**Other arrow updates** A precursor of arbitrary arrow update logic AAUL is the logical semantics for knowability logic of [166]. The quantification in [166] is also over (equivalence) relational restrictions in a given model with constant domain. However, their quantifier is not bisimulation invariant, as the restriction is not parameterized by logical conditions such as the source and target formulas of arrow update logic. The authors discuss alternative solutions to the knowability paradox in their semantics.

Finally, the dual of arrow preservation in arrow update logics is arrow removal, as in sabotage logic [125] and various other relation-changing logics [16] presented in Section 9.

## 6.3 Open problems and further research

Arrow updates often compare well intuitively with action models, and seem to permit suc-
cinct descriptions of knowledge dynamics. We merely list some topics for further research.

* Axiomatization of arrow update logic on $S5$ models [156]

• Axiomatization of arrow update model logic on $S5$ models [96, 157]

• Synthesis for arrow update model logic on $S5$ models [157]

7 Refinement modal logics

Refinement modal logic (RML) [45]<fnref n="9" /> is a stranger in our midst, unless you get to know her better. Please allow us to make the proper introductions. Refinement modal logic does not contain announcements, nor (modalities for) action models or similar, but it contains quantifiers over information change. We recall knowability logic, wherein you can say ‘there is an announcement after which $\varphi'$ but without announcements in the logical language (Section 3.2). That is intuitively appealing but theoretically problematic, as no axiomatization is known. In refinement modal logic you can (intuitively but not formally) say ‘there is an action model after which $\varphi'$, but without modalities for action models in the logical language. So this is as in arbitrary action model logic (Section 5.1), but without action models in the logical language. How to get rid of those? This is not problematic, but we need a detour through modal logic. Please read on.

<footnote n="9">⁹But also [139, 144, 85, 82] predating the focal publication [45], as well as [84, 46, 1, 167] coming later.</footnote>
## 7.1 Refinement modal logic

**Refinement** In arbitrary public announcement logic we quantify over announcements, in arbitrary action model logic we quantify over action models, and in arbitrary arrow update (model) logic we quantify over arrow updates. All these quantifications have in common that the logical language contains modal operators for specific model transformations corresponding to the execution of epistemic actions, and the quantification is defined in terms of these modalities. In *refinement modal logic* RML [45] we quantify over the refinements of a given model. We recall (from Section 2) that, from the requirements **atoms**, **forth** and **back** of a bisimulation, a refinement relation only needs to satisfy **atoms** and **back**; and that $M \supseteq M'$ means that model $M'$ is a refinement of model $M$ (that is, that there is a refinement relation between the models $M$ and $M'$). The semantics of the refinement quantifier directly use this refinement relation. The language of refinement modal logic does not have modalities for the execution of epistemic actions. Although the refinement quantifier therefore does not quantify over epistemic actions, the relation to other quantifiers is so close that this warrants detailed discussion of RML in this survey.

We start with some elementary examples illustrating the refinement relation.

**Example 14** Given the properties of the refinement relation, a refinement can be seen as a restriction of a bisimilar copy of a given model. Consider the models depicted below.

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

We note that:

* $M'$ is a submodel (model restriction) of $M$.

* $M''$ is a refinement of $M$ (arrows in bold font).

* $M'''$ is a bisimilar copy of $M$.

Model $M''$ is a submodel of $M'''$ that is a bisimilar copy of $M$. Model $M''$ is not a submodel of $M$. A refinement is a model restriction of a bisimilar copy of a model.

In fact, all of $M'$, $M''$, $M'''$ are refinements of $M$. Let us give the refinement relations linking $M$ to its respective refinements. Consider the numbers below the three models. Let the names of the states be those numbers, possibly primed, or doubly or triply primed. Assume that all states in all models have the same valuation of atoms. Let $R^\sharp$ be the accessibility relation in a model $M^\sharp$, where $\sharp$ is one of '$', "', "''$, and consider the relation $Z^\sharp$ between $M$ and $M^\sharp$ that relates any state $i$ to $i^\sharp$ in case $i^\sharp$ exists and also to $-i^\sharp$ in case it exists. Then all such $Z^\sharp$ are refinement relations. Relation $Z'''$ is also a bisimulation. We
merely illustrate why the relation $Z''$ between $M$ and $M''$ defined as above is a refinement relation. Note that $Z'' = \{(0,0''), (1,1''), (1,-1''), (2,2'')\}$. This relation is a refinement, because it satisfies the requirements **atoms** and **back**. Crucially, $Z''$ it is not a bisimulation, because it does not satisfy **forth**: observe that $(2,2'') \in Z''$ and $(2,3) \in R$, but there is no state $t$ in $M''$ such that $(3,t) \in Z''$ and $(2'',t) \in R''$.

**Example 15** Two models can be each other's refinement, but not bisimilar. Consider the models $M$ and $N$ depicted below. The dashed relation is a refinement between $N$ and $M$, where we recall the notation $N \succeq M$, and the dotted relation is a refinement between $M$ and $N$, that is, $M \succeq N$. Still, $M$ and $N$ are not bisimilar.

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

In [45] and most related works on refinement modal logic, instead of the refinement relation as above (for the set of all agents) the refinement relation has a parameter $G \subseteq A$, and apart from **atoms** and **back** (for all agents), additionally, **forth** is required for the agents in $A \setminus G$. As this was partly for technical reasons, in this survey we only consider refinement for the set $A$ of all agents, which simplifies the presentation.

**Language and semantics of refinement modal logic** The language $\mathcal{L}(\diamond, \langle\succeq\rangle)$ of refinement modal logic is the language $\mathcal{L}(\diamond)$ of multi-agent modal logic extended with an inductive construct $\langle\succeq\rangle\varphi$, representing 'there is a refinement after which $\varphi$'. It has the following semantics.

$$M_s \models \langle\succeq\rangle\varphi \text{ iff there is } M_{s'} \text{ such that } M_s \succeq M_{s'} \text{ and } M_{s'} \models \varphi$$

As the refinement relation is transitive, reflexive, and confluent (for all $x, y, z$, if $x \succeq y$ and $x \succeq z$, there is $w$ such that $y \succeq w$ and $z \succeq w$), we have for the refinement modality the corresponding validities:

* $[\succeq]\varphi \rightarrow \varphi$ (T)

* $\langle\succeq\rangle\langle\succeq\rangle\varphi \rightarrow \langle\succeq\rangle\varphi$ (4)

* $\langle\succeq\rangle[\succeq]\varphi \rightarrow [\succeq]\langle\succeq\rangle\varphi$ (Church-Rosser) / CR

The refinement quantifier also satisfies:

* $[\succeq]\langle\succeq\rangle\varphi \rightarrow \langle\succeq\rangle[\succeq]\varphi$ (McKinsey) / MK
As this has not been observed in the literature, it requires proof. We recall the relational property of *atomicity* corresponding to **4** plus MK, and that it is valid in APAL (Section 3.2). The proof that MK is valid for RML is simpler.

Towards a contradiction assume that MK does not hold. Then there is an epistemic model $M_s$ and a $\varphi$ such that $M_s \models [\succeq]\langle\succeq\rangle\varphi$ as well as $M_s \models [\succeq]\langle\succeq\rangle\neg\varphi$, where $M = (S, R, V)$ and $s \in S$. Now consider $M^\emptyset = (S, R^\emptyset, V)$ that is as $M$ except that for all $a \in A$, $R_a^\emptyset = \emptyset$: we remove all pairs from all accessibility relations. We note that $M \succeq M^\emptyset$ and in particular $M_s \succeq M_s^\emptyset$. As all relations are empty, $M_s^\emptyset = \langle\succeq\rangle\varphi$ iff $M_s^\emptyset = \varphi$: the unique refinement of an empty relation is the empty relation. Now $M_s \models [\succeq]\langle\succeq\rangle\varphi$ and $M_s \succeq M_s^\emptyset$ imply $M_s^\emptyset \models \langle\succeq\rangle\varphi$, and in view of the above, $M_s^\emptyset \models \varphi$. Also, $M_s \models [\succeq]\langle\succeq\rangle\neg\varphi$ and $M_s \succeq M_s^\emptyset$ imply $M_s^\emptyset \models \langle\succeq\rangle\neg\varphi$, and therefore $M_s^\emptyset \models \neg\varphi$. We have obtained a contradiction.

Just as a refinement of a given model is a restriction of a bisimilar copy of that model, refinement quantification is bisimulation quantification followed by relativization. In *bisimulation quantified logics* we have explicit quantifiers $\forall p$ over propositional variables $p$ [67, 162]. *Relativization* $\varphi^p$ of a formula $\varphi$ to an atomic proposition $p$ is a syntactic way to describe model restrictions, such as the consequences of a public announcement: $(M|p)_s \models \varphi$ iff $M_s \models \varphi^p$, which of course in PAL is the same as $M_s \models \langle p \rangle\varphi$, see [104, 127]. In refinement modal logic, given $\varphi \in \mathcal{L}(\diamond)$, we have [45, Sect. 4.3]:

$$ \langle\succeq\rangle\varphi \text{ is equivalent to } \exists p \langle p \rangle\varphi $$

Example 14 was an illustration: given $M$, we first take its bisimilar copy $M'''$ and make an atom $p \in P$ true (only) in states $-1'''$, $0'''$, $1'''$, $2'''$. Then announce $p$. Model $M'$ now results.

This equivalence is a non-trivial result, because announcing an atom is far more restrictive than announcing an arbitrary formula, which in its turn is far more restrictive than executing an arbitrary epistemic action, such as a pointed action model. We will now discuss that.

## Relation between action models and refinement

*Executing an action model produces a refinement of the initial model, and for every refinement of a finite model there is an action model producing it.*

We sketch the proof found in [45].

Given pointed model $M_s$ and epistemic action $E_e$, the resulting $(M \otimes E)_{(s,e)}$ is a refinement of $M_s$ by way of the relation $Z$ consisting of all pairs $(t, (t, f))$ such that $M_t \models \text{pre}(f)$. Some states of the original model may get lost in the modal product, namely if there is no action whose precondition can be executed there. But all ‘surviving’ (state,action)-pairs simply can be traced back to their first argument: clearly a refinement.

For the other direction, let refinement $N_t$ of a finite model $M_s$ be given, and let $Z$ be the refinement relation. Consider action model $E$ that is isomorphic to $N$ (for convenience of the presentation we let the names of actions and states correspond), and wherein the valuation of propositional variables in a state $t'$ of model $N$ is replaced by a precondition
pre(t') ∈ L(◇) of action t' that is the distinguishing formula of the set of states s' in M such that (s', t') ∈ Z. As M is finite, this distinguishing formula exists [47, 122]. We now have that $M_{s'} \models$ pre(t') iff (s', t') ∈ Z, and that $(M \otimes E)_{(s,t)}$ is bisimilar to $N_t$.

**Example 16** Recalling Example 2 on page 10, the picture below shows once more the execution of an action model, now including the refinement relation (visualized as dashed arrows) between the initial model and the updated model.

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

The restriction to finite models is important and the result does not hold on all models. For a counterexample, consider the model $M$ consisting of all (infinitely many) valuations of a countably infinite set of atoms $P$ and that are all indistinguishable by a single agent $a$. The accessibility relation for $a$ is the universal relation on that domain. Now consider model $M^-$ that is like $M$ except that the accessibility relation for $a$ is the identity relation. Note that $M^-$ is a refinement of the model $M$. You can get from $M$ to $M^-$ by the epistemic action of announcing the valuation, in whatever state you are. But for that you have to announce the value of infinitely many atoms, and an infinite conjunction is not a formula. It cannot be a precondition of an action. There is no action model producing $M^-$. This appears to make the relation with action model logic problematic. But in fact it is rather straightforward once you take the perspective of a given formula. A given $\varphi \in L(◇)$ bound by the refinement modality only contains a finite number of atoms. Therefore you can announce the values of all the atoms occurring in $\varphi$, in the form of an action model or an arrow update. With additional manipulations similar to those above one can then prove that [157, Theorem 28]:

$\langle\succeq\rangle\varphi$ is equivalent to $\langle\otimes\rangle\varphi;$

$\langle\succeq\rangle\varphi$ is equivalent to $\langle\uparrow\rangle\varphi;$

$\langle\uparrow\rangle\varphi$ is equivalent to $\langle\otimes\rangle\varphi.$

It is also reported there that this result generalizes to arbitrary formulas $\varphi$ in the respective languages, by a proper inductively defined translation. Therefore, these three quantifiers are interchangeable in any formula, by an argument involving natural induction over quantifier occurrence, and reduction axioms. It is interesting to observe that, even though the three logics AAML, AAUML, and RML are all as expressive as the logic K, they differ in so-called *update expressivity*. Given the model class of interpretation, this is the relation between pointed models induced by the respective updates (a typical update that can only be expressed in RML is the one producing $M \succeq M^-$ above). For such matters see [98] and [157, Section 5].
**Axiomatization** The axiomatization of RML reported in [45] is in terms of parametrized refinement quantifiers $\langle \succeq_a \rangle$ for $a \in A$ (interpreting a-refinement relations $\succeq_a$, where we recall that in this survey we only consider $\succeq$). There is an alternative axiomatization for RML with only refinement quantifiers $\succeq$ for the set $A$ of all agents. It consists of the axiomatization of arbitrary arrow update model logic in [157, Section 4, Theorem 19] (see the previous Section 6.2), wherein we replace all $\langle \uparrow \rangle$ quantifiers by $\langle \succeq \rangle$ quantifiers, and remove all reduction axioms involving arrow update models. This is justified by recalling the above-mentioned equivalence of $\langle \uparrow \rangle \varphi$ and $\langle \succeq \rangle \varphi$ and its generalization to arbitrary formulas. It is simpler than the axiomatization in [45]. We only give the crucial reduction axiom for the $\langle \succeq \rangle$ quantifier. It is obtained as indicated above from the axiom (*) of AAUML in Section 6.2.

$$ \langle \succeq \rangle \bigwedge_{a \in A} \left( \bigwedge_{\varphi_a \in \Phi_a} \diamond_a \varphi_a \wedge \Box_a \psi_a \right) \leftrightarrow \bigwedge_{a \in A} \bigwedge_{\varphi_a \in \Phi_a} \diamond_a \langle \succeq \rangle (\varphi_a \wedge \psi_a) \quad (**) $$

Given such reductions, the logic RML is therefore as expressive as the multi-agent modal logic K, and it is therefore also decidable, unlike APAL.

The complexity of RML is $AEXP_{pol}$ for single-agent version [46]. $AEXP_{pol}$ is the class of problems solvable by alternating Turing machines running in single exponential time but only with a polynomial number of alternations. The complexity is conjectured to be non-elementary for multi-agent RML. In [1] a PSPACE upper bound is given for complexity of the existential fragment of (single-agent) RML: this is a negation normal form except that only $\langle \succeq \rangle$ and not $[\succeq]$ may occur. Apart from refinement modal logic RML, there is also refinement $\mu$-calculus, for various results on this $\mu$-RML see [45]. For example, the complexity of satisfiability of $\mu$-RML is non-elementary.

## 7.2 Refinement epistemic logic

The semantics of the refinement quantifier depend on the class of models it quantifies over. In particular, quantifying over models from the class $\mathcal{K}$ is different from quantifying over models from the class $\mathcal{S}5$, a class of interest as the $\Box_a$ modalities then represent knowledge. The semantics are straightforward. Let $M$ be an $\mathcal{S}5$ model, $s \in \mathcal{D}(M)$ and $\varphi \in \mathcal{L}(\diamond, \succeq)$, then

$$ M_s \models \langle \succeq \rangle \varphi \quad \text{iff} \quad \text{there is an } \mathcal{S}5 \text{ model } M_{s'} \text{ such that } M_s \succeq M_{s'} \text{ and } M_{s'} \models \varphi $$

But the axiomatization is not straightforward. The axiomatization of refinement modal logic on models with particular frame properties does not extend the axiomatization with respect to $\mathcal{K}$. Indeed, the axiom (*) above is unsound on class $\mathcal{S}5$.

**Example 17** In axiom (**), let $\Phi_a = \{\Box_a p, \neg \Box_a p\}$ and $\psi_a = \top$, and consider a two-state model $N$ wherein agent $a$ does not know $p$ and $p$ is actually true. Then

$$ \diamond_a \langle \succeq \rangle \Box_a p \wedge \diamond_a \langle \succeq \rangle \neg \Box_a p \text{ is true:} $$
Agent *a* considers it possible that after having been informed of *p* she knows that *p*, and she also considers it possible that after not having been informed of anything she still does not know *p*. But

$\langle\succeq\rangle(\Diamond_a\Box_a p \wedge \Diamond_a\neg\Box_a p)$ is false:

Consider towards a contradiction a hypothetical model that is a refinement of *N* and wherein $\Diamond_a\Box_a p \wedge \Diamond_a\neg\Box_a p$ is true. The S5 validity $\Box_a\neg\Box_a\varphi \leftrightarrow \neg\Box_a\varphi$, that is, $\Box_a\varphi \leftrightarrow \Diamond_a\Box_a\varphi$, tells us that whenever you see $\Diamond_a\Box_a$ you can delete $\Diamond_a$. The S5 validity $\Box_a\Box_a\varphi \leftrightarrow \Box_a\varphi$ tells us that whenever you see $\Box_a\Box_a$ you can delete a $\Box_a$. Further note that $\Diamond_a\neg\Box_a p$ is equivalent to $\neg\Box_a\Box_a p$. Because of all that, $\Diamond_a\Box_a p \wedge \Diamond_a\neg\Box_a p$ is equivalent to $\Box_a p \wedge \neg\Box_a p$, which is inconsistent.

However, refinement epistemic logic has been axiomatized, and the axiomatization is again a reduction system, namely to the logic S5. Axiomatizations for refinement modal logic on a large variety of model classes, such as the above for S5, can be found in [85, 84]. A welcome member there, called *refinement doxastic logic*, is an axiomatization for RML on class *KD45*, the serial, transitive, and Euclidean frames, that are typically used to model belief. There are some surprises and open questions: *transitive refinement modal logic* (RML on class *K4*, the transitive frames) is (strictly) more expressive than the modal logic K4 that it extends, and its axiomatization is an open question. This can be found in an unpublished manuscript by Tim French.

## 7.3 Simulation modal logic

Instead of the language $\mathcal{L}(\diamond, \langle\succeq\rangle)$ of refinement modal logic with the semantics

$M_s \models \langle\succeq\rangle\varphi \text{ iff there is } M_{s'} \text{ such that } M_s \succeq M_{s'} \text{ and } M_{s'} \models \varphi$

now consider the language $\mathcal{L}(\diamond, \langle\preceq\rangle)$ of *simulation modal logic* with the semantics

$M_s \models \langle\preceq\rangle\varphi \text{ iff there is } M_{s'} \text{ such that } M_s \preceq M_{s'} \text{ and } M_{s'} \models \varphi$

This operator quantifies over the simulations of a given model instead of over its refinements. This logic has been investigated and axiomatized in [167], in a language and semantics with quantifiers that combine refinement and simulation for subsets of the set of all agents. To highlight how their results compare to RML we only consider simulation for the set of all agents. We now recall the (**) axiom of RML (and the (*) axiom of AAUML), juxtaposed to the corresponding reduction (*** ) for simulation that is extrapolated from [167, Axiom CCRKco2] to emphasize their resemblance.

$$ \langle\succeq\rangle \bigwedge_{a \in A} \left( \bigwedge_{\varphi_a \in \Phi_a} \Diamond_a \varphi_a \wedge \Box_a \psi_a \right) \leftrightarrow \bigwedge_{a \in A} \bigwedge_{\varphi_a \in \Phi_a} \Diamond_a \langle\succeq\rangle (\varphi_a \wedge \psi_a) \quad (**) $$

$$ \langle\preceq\rangle \bigwedge_{a \in A} \left( \bigwedge_{\varphi_a \in \Phi_a} \Diamond_a \varphi_a \wedge \Box_a \psi_a \right) \leftrightarrow \bigwedge_{a \in A} \Box_a \bigvee_{\varphi_a \in \Phi_a} \langle\preceq\rangle (\varphi_a \wedge \psi_a) \quad (***) $$
Simulation modal logic quantifies over models with more uncertainty than the current one. Refinement preserves the positive formulas: hard knowledge. Whereas simulation preserves ignorance. It seems worthwhile to investigate simulation modal logic in depth, in particular on the class S5: *simulation epistemic logic*, and to obtain synthesis for that.

## 7.4 Open problems and further research

Refinement modal logic and its variations have not received as much attention from the research community as APAL and its variations, despite theoretical properties that compare well (decidability, reduction, ...). We recall the similar story about arbitrary action model logic spelled out in Section 5.3. There, we conjectured that this has to do with non-public dynamics being harder to grasp than public dynamics, despite quantifying over non-public dynamics being so much more elegant than quantifying over public dynamics. Maybe this gap can be closed for RML by considering yet other variations, or applications: dynamic modalities that are interpreted as pruning tree-representations of models might be suitable for various other structures than epistemic models and for extending various other logics. Given refinement modal $\mu$-calculus (μ-RML) presented in [46], two such candidates for extension with refinement modalities are CTL [57, 58], where a relation with QCTL, quantified CTL, is to be expected [100], and PDL [65, 87].

Open problems and further research include:

* Investigating refinement CTL and refinement PDL, and their expressivity [46]

* The axiomatization of simulation modal logic for a single simulation quantifier for all agents [167, 46]

* The axiomatization of simulation epistemic logic on class S5 [167, 46]

* Synthesis for different refinement and simulation modal logics [83, 157]

# 8 Iteration, factual change, group epistemics, and planning

The final two sections of this survey are more exploratory in nature. They are less a survey on work done, and more about further research, because little work has been done in dynamic epistemic logic on those subjects involving quantification over information change. In Section 8 we focus on topics central in dynamic epistemic logic but for which extensions with quantifiers have not or rarely been considered. In Section 9 we focus on update logics (model changing logics) with quantifiers but that are not dynamic epistemic logics.
## 8.1 Iterated updates

**Standard program operations on updates** So far, we always considered dynamic modalities $\langle\pi\rangle$, where $\pi$ is an *update*, inducing transformation of ('updating') an epistemic model, not necessarily deterministically. We can see the update as a program. In public announcement logic the programs are the announcements, in action model logic the programs are the pointed finite action models, and so on. We can then wonder about standard program operations, as in PDL: test, choice, sequential execution, and arbitrary iteration ('Kleene star') [87]. Except for the arbitrary iteration, the main topic of this section, such program operations are syntactically definable in dynamic epistemic logics, and (maybe therefore) not commonly considered.

$$ 
\begin{align*}
\langle?\psi\rangle\varphi &\leftrightarrow \psi \wedge \varphi \\
\langle\pi \cup \pi'\rangle\varphi &\leftrightarrow \langle\pi\rangle\varphi \vee \langle\pi'\rangle\varphi \\
\langle\pi; \pi'\rangle\varphi &\leftrightarrow \langle\pi\rangle\langle\pi'\rangle\varphi
\end{align*}
$$

**Test** The semantics for the modality for a test $?\psi$ contrasts well with the semantics for public announcement of $\psi$ that we already know:

$$ 
\begin{align*}
M_s \models \langle?\psi\rangle\varphi \quad \text{iff} \quad M_s \models \psi \quad \text{and} \quad M_s \models \varphi \\
M_s \models \langle\psi\rangle\varphi \quad \text{iff} \quad M_s \models \psi \quad \text{and} \quad (M|\psi)_s \models \varphi
\end{align*}
$$

If a test $?\psi$ can be executed, $\psi$ must have been true, and as the resulting model is the same as the original one, any postcondition $\varphi$ is true if $\varphi$ already was true. This explains that $\langle?\psi\rangle\varphi \leftrightarrow (\psi \wedge \varphi)$ is valid, and that a test is definable in dynamic epistemic logic. A public announcement is a test on $\psi$ that is observed by all agents and thus resulting in a different model in which to interpret $\varphi$, whereas the test $?\psi$ is not observed by any agent, and thus resulting in the same model in which to interpret $\varphi$.

**Choice** Non-deterministic choice between programs does not commonly feature in dynamic epistemic logics because it is definable as $\langle\pi \cup \pi'\rangle\varphi \leftrightarrow \langle\pi\rangle\varphi \vee \langle\pi'\rangle\varphi$. The box-version of that equivalence, $[\pi \cup \pi']\varphi \leftrightarrow [\pi]\varphi \wedge [\pi']\varphi$, is considered less intuitive because the choice $\cup$ becomes a conjunction $\wedge$. For a finite set $\Pi$ of programs we thus get that $\langle\cup_{\Pi}\pi\rangle\varphi \leftrightarrow \bigvee_{\Pi}\langle\pi\rangle\varphi$. Indirectly we have already seen this with the multi-pointed action models: $[E_F]\varphi \leftrightarrow \bigwedge_{e \in F}[E_e]\varphi$ and in particular $[E]\varphi \leftrightarrow \bigwedge_{e \in D(E)}[E_e]\varphi$. For an infinite set $\Pi$ of programs, such as 'all announcements' ($\Pi = \mathcal{L}(\diamond, !)$) or 'all finite pointed action models', we can still consider $\cup_{\Pi}\pi$ as a semantic object, but $\bigvee_{\Pi}\langle\pi\rangle$ would be an infinite disjunction, which is not in the logical language. However, for both finite and countably infinite $\Pi$ we can consider $\langle\cup_{\Pi}\pi\rangle\varphi$ as a quantification $\langle\bullet\rangle\varphi$. If $\Pi = \mathcal{L}(\diamond, !)$ we get $\langle\bullet\rangle = \langle!\rangle$ and if $\Pi$ is the set of all finite pointed action models we get $\langle\bullet\rangle = \langle\otimes\rangle$.

**Sequential update** Given that $\langle\pi; \pi'\rangle\varphi \leftrightarrow \langle\pi\rangle\langle\pi'\rangle\varphi$, if $\pi = \pi'$ we get $\langle\pi; \pi'\rangle\varphi \leftrightarrow \langle\pi\rangle\langle\pi\rangle\varphi$, in other words, $\langle\pi^2\rangle\varphi \leftrightarrow \langle\pi\rangle^2\varphi$. Similarly, for any $n \in \mathbb{N}$, $\langle\pi^n\rangle\varphi \leftrightarrow \langle\pi\rangle^n\varphi$, where $\langle\pi^0\rangle\varphi = \langle\pi\rangle^0\varphi := \varphi$. In particular, for iteration of public announcements we have
$\langle\varphi\rangle^n\psi \leftrightarrow \langle\varphi^n\rangle\psi$, and for iteration of epistemic actions $E_e$ we get that $\langle E_e\rangle^n\psi \leftrightarrow \langle E_e^n\rangle\psi$. This brings us to arbitrary iteration.

**Arbitrary iteration** Let us now define

$$ \langle\pi^*\rangle\varphi \quad \text{iff} \quad \text{there is } n \in \mathbb{N} \text{ such that } \langle\pi^n\rangle\varphi. $$

In view of the above we write $\langle\pi^*\rangle\varphi$ and $\langle\pi\rangle^*\varphi$ interchangeably. We get a very different form of quantification over information change if we merely consider arbitrary iteration of a given update $\pi$, and dynamic epistemic languages with so-called infinitary (dynamic) modalities for such arbitrary iteration. Such iterated updates have rarely been investigated as part of the dynamic epistemic logical language. The exception is [104], wherein it is shown that already for very simple settings ($\mathcal{K}$ models, single-agent) the logic becomes undecidable. Axiomatizations of such logics are also unknown. Possibly for such reasons, the dynamic epistemic logic community has stayed away from arbitrarily iterated updates in the language.<fnref n="10" />

On the other hand, iterated updates have received much attention in dynamic epistemic logics in purely semantic investigations. These are ‘off-line’ (meta-level) analyses of the consequences of iterated dynamics on given epistemic models described with the language $\mathcal{L}(\diamond)$. The more interesting of such proposals involve Moorean phenomena wherein the truth value of knowledge or ignorance propositions keeps flipping back and forth. Let us name a few.

* A most publishable unpublished work is [117], wherein updated epistemic models that are the result of executing arbitrarily iterated finite action models display fascinating oscillations between stable points reached during such iterations.

* In [34], belief dynamics under iterated revision is explored (belief revision is modelled as a particular form of update on enriched epistemic models). This developed further into, or rather merged with, learning theory investigating ‘asymptotic’ knowledge properties of epistemic models after arbitrary iteration of action models [29, 44].

* Iterated sincere and insincere updates (lying) are modelled in [7], and it is shown that you can keep changing your opinion on some matter of interest in arbitrarily haphazard and irregular ways up to infinity (not very encouraging for everyday politics).

* In gossip protocols the informative updates represent telephone calls, where the denotation of such a protocol is a set of possibly infinite call sequences. However, given the restricted setting, the informative consequences of call sequences are bounded: stable

<footnote n="10">¹⁰Note that the arbitrary iteration in epistemic PDL of [132], often presented as a dynamic epistemic logic dialect, is not over the updates. The iteration is over tests $?\varphi$ and epistemically interpreted modalities, in order to formalize relativized common knowledge. Whereas the extension of that language with updates, that begets the Logic of Communication and Change of [132], does not allow iteration of updates.</footnote>
information points again, in execution trees generated by such protocols [10, 160]. Such analysis are PDL-style analyses, and although such calls can be modelled as action models [78], it is not entirely clear how to associate a gossip protocol with a ‘dynamic epistemic logic style’ update modality, except in the case of protocols where all executions are finite.

* Meta-level iterated updates are also a main focus of epistemic planning in dynamic epistemic logic, to which a separate discussion is devoted later in this section.

**Iterated arbitrary updates** Let now $\langle\bullet\rangle$ be any quantifier.

Most of our quantifiers satisfy $\varphi \to \langle\bullet\rangle\varphi$, as there is a trivial, non-informative, update. This is the announcement of the always true formula $\top$, for which there also is a corresponding action model, arrow update, group announcement, etcetera. For this trivial $\pi$ the equivalence $\varphi \leftrightarrow \langle\pi\rangle\varphi$ is valid. With implication $\langle\pi\rangle\varphi \to \langle\bullet\rangle\varphi$ that gives us $\varphi \to \langle\bullet\rangle\varphi$.

Most of our quantifiers also satisfy $\langle\bullet\rangle\varphi \to \langle\bullet\rangle\langle\bullet\rangle\varphi$, which can be obtained from $\varphi \to \langle\bullet\rangle\varphi$ by elementary further manipulations.

And most quantifiers also satisfy $\langle\bullet\rangle\langle\bullet\rangle\varphi \to \langle\bullet\rangle\varphi$. This holds when the composition of two updates is again an update (of the same kind). For most of the quantifiers we have seen, this is indeed the case:

A sequence of two announcements $\varphi$ and $\psi$ is again an announcement, namely that of $\langle\varphi\rangle\psi$. We recall that a PAL validity is $\langle\varphi\rangle\langle\psi\rangle\chi \leftrightarrow \langle\langle\varphi\rangle\psi\rangle\chi$ [155]. A sequence of two action models is again an action model, namely the composition of those two action models [30] (see Section 2). A sequence of two arrow updates is an arrow update [96], and the relational composition of two refinements or of two simulations is again a refinement respectively a simulation [45] (pruning a tree, and pruning it again, is still pruning a tree; similarly, growing a tree and letting it grow more, is still growing a tree).

From $\langle\bullet\rangle\varphi \to \langle\bullet\rangle\langle\bullet\rangle\varphi$ and $\langle\bullet\rangle\langle\bullet\rangle\varphi \to \langle\bullet\rangle\varphi$ follows $\langle\bullet\rangle\varphi \leftrightarrow \langle\bullet\rangle\langle\bullet\rangle\varphi$, and therefore $\langle\bullet\rangle\varphi \leftrightarrow \langle\bullet\rangle^n\varphi$ for any positive $n \in \mathbb{N}$. This gets us $\langle\bullet\rangle\varphi \leftrightarrow \langle\bullet\rangle\langle\bullet\rangle^*\varphi$, which is written as $\langle\bullet\rangle\varphi \leftrightarrow \langle\bullet\rangle^{+\varphi}$.

We also have that $\langle\bullet\rangle(\varphi \lor \psi) \leftrightarrow \langle\bullet\rangle\varphi \lor \langle\bullet\rangle\psi$.

Considering program operations on modal quantifiers therefore does not have added value. In contrast, the investigation of dynamic epistemic logics with arbitrary iteration of epistemic actions and with additionally quantifiers over such epistemic actions seems worthwhile to pursue.

## 8.2 Factual change

Dynamic epistemic logic is typically a logic wherein, in a given unchanging world, we model changes of knowledge due to observations by agents. There is no factual change (also known as ontic change, literally: change of the world). But there can be. Factual change can be public — when a solar eclipse obscures the sun to all alike — but also private — when you change the pincode of your bankcard. Integrated ontic and epistemic change can be straightforwardly described as action models [132, 149], and extending action model
logic with quantifiers over such epistemic actions is also straightforward. We refrain from details.

However, concerning quantification there is a big ‘if’. Unrestricted quantification over action models with factual change is conceptually problematic, because in that case ‘anything goes’. Given agents A and atoms P, any finite epistemic model $M_s$ can be transformed into any other finite epistemic model $N_t$ by an action model with factual change [149]. The procedure is elementary. First announce the distinguishing formula of $s$ in $M$. Note that an announcement is a singleton action model. The result is the singleton epistemic model with point $s$. Then execute an action model with the shape of $N$, trivial preconditions, and assigning the values to the atoms that they have in model $N_t$. Now take the composition of these two action models. This action model updates $M_s$ into (a model isomorphic to) $N_t$. We merely illustrate this by a three-agent example as below, where $p \wedge \neg q$ is the distinguishing formula of state 10.

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

Let now $\langle\otimes\rangle$ be a modality quantifying over such action models with factual change. Using the above procedure, we can show that on the class of finite S5 models $\langle\otimes\rangle\varphi$ is valid for any consistent $\varphi \in \mathcal{L}(\diamond)$. We merely rephrase the proof in [149] (that holds for a more general class of models): Let $N_t$ be an epistemic model satisfying $\varphi$. Let $M_s$ be arbitrary. Let now $E_e$ be the action model that is the composition of two such as above, so that $(M \otimes E)_{(s,e)}$ is bisimilar to $N_t$. Then $M_s \models \langle E_e \rangle \varphi$. Therefore $M_s \models \langle\otimes\rangle \varphi$. End of proof.

We conjecture that the restriction to finite models is not necessary to obtain the validity of $\langle\otimes\rangle\varphi$, by using the synthesis results for action model logic reported in [83] and Section 5.1. Which brings us to the morale of this story: a logic wherein we can realize every consistent formula $\varphi$ by an update may not be of much practical interest. However, much more restricted quantification over epistemic and ontic actions is the common way to proceed in epistemic planning. This will be discussed in Section 8.4.

## 8.3 Group epistemic operators

Let us now consider logics with group epistemic operators, for a group $G \subseteq A$ of agents. The three best known types of group epistemic operators are mutual, common, and distributed knowledge. ‘It is mutual knowledge between the agents in $G$ that $\varphi$’ (‘everybody in $G$ knows $\varphi$’), notation $E_G\varphi$, is defined as the conjunction of $\Box_a\varphi$ for all $a \in G$. ‘It is common knowledge between the agents in $G$ that $\varphi$’, notation $C_G\varphi$, is syntactically defined as the arbitrary iteration of everybody knows $\varphi$, or semantically defined as the truth of $\varphi$ in all states reachable from a given state by the relation $(\bigcup_{a \in G} R_a)^*$ (the finite $G$-paths). ‘It is distributed knowledge between the agents in $G$ that $\varphi$’, notation $D_G\varphi$, is defined as truth
of $\varphi$ in all states reachable from a given state by the intersection relation $\bigcap_{a \in G} R_a$. For references, see [59, 146].

When adding common knowledge to public announcement logic, the public announcement modality can no longer be eliminated from the language by reduction axioms, and the axiomatization is non-trivial [30, 155], which has led to the proposal of relativized common knowledge [132]. Adding distributed knowledge to public announcement logic is also non-trivial for the axiomatization, because proving completeness requires adjusting the standard canonical model technique [165], and it also needs a different notion of bisimulation [116]. Given the often surprising and unexpected expressivity results for logics wherein epistemic and dynamic modalities interact, and also for logics wherein these interact with quantifiers over dynamic modalities, the expressivity landscape is more complex in the presence of group epistemic operators. Few proposals have been made to extend such logics with group epistemic modalities. We can roughly distinguish contributions adding group epistemic modalities to quantifying over public change, to quantifying over semi-public change, and to quantifying over private change (or yet other epistemic actions).

**Group epistemics and quantifying over public change** GAL with distributed knowledge is investigated in [74] and the extended journal version [75], with results on axiomatization and expressivity.

APAL and GAL with common knowledge are investigated in [73]. Different semantics for the APAL quantifier $\langle!\rangle\varphi$ are proposed, and similarly for the CAL and GAL quantifiers. Let $\mathcal{L}(\dots, C)$ be the extension with common knowledge of a language $\mathcal{L}(\dots)$. The three investigated APAL variants are as follows, where $\langle!\rangle\varphi \in \mathcal{L}(\diamond, !, \langle!\rangle, C)$. Note that in all cases the quantification is over quantifier-free formulas.

$$M_s \models \langle!\rangle\varphi \quad \text{iff} \quad \text{there is a } \psi \in \mathcal{L}(\diamond) \text{ such that } M_s \models \langle\psi\rangle\varphi$$

$$M_s \models \langle!\rangle\varphi \quad \text{iff} \quad \text{there is a } \psi \in \mathcal{L}(\diamond, C) \text{ such that } M_s \models \langle\psi\rangle\varphi$$

$$M_s \models \langle!\rangle\varphi \quad \text{iff} \quad \text{there is a } \psi \in \mathcal{L}(\diamond, !, C) \text{ such that } M_s \models \langle\psi\rangle\varphi$$

There are results on expressivity and on axiomatization.

**Group epistemics and quantifying over semi-public change** In [156, Section 4.3] arbitrary arrow update logic (without common knowledge) is shown to be incomparable in expressivity to epistemic logic with common knowledge, on class $\mathcal{S}5$.

In [99] it is shown that arbitrary arrow update logic with common knowledge does not have a finitary axiomatization. This could in principle throw further light on the open question whether APAL (without common knowledge) has a finitary axiomatization.

**Group epistemics and quantifying over private change** Extensions of arbitrary action model logic AAML and refinement modal logic RML with common knowledge or with distributed knowledge seem more manageable than extensions of APAL, GAL and AAUL with common knowledge, because the quantifiers can be eliminated from AAML and RML. It seems worth investigating if they can still be eliminated from such extensions.
Such extensions would be relevant for epistemic planning and for information-based security protocols (Section 4.5), wherein distributedly known initial problem configurations and commonly known epistemic goals are important. We do not know of any publications.

## 8.4 Epistemic planning

Let us assume multi-agent S5 models. An epistemic planning problem consists of an initial state s (where we should think of this as a pointed epistemic model $M_s$) or a set of initial states, a finite set $\Sigma$ of epistemic actions $\sigma$, and a goal formula $\gamma \in \mathcal{L}(\diamond) [40, 39, 43]$. Instead of an initial state we may have a property of the initial state, a formula $\delta \in \mathcal{L}(\diamond)$. In that case, we wish to find plans for any state satisfying $\delta$ (any configuration where block C is on block B, any model wherein agent a is ignorant of p, ...). Solving an epistemic planning problem then becomes the question whether

$$ \delta \wedge \langle (\bigcup_{\Sigma} \sigma)^* \rangle \gamma $$

is satisfiable. If all $\sigma \in \Sigma$ are deterministic (that is, if the updates are partial functions), some sequence $\sigma_1...\sigma_n$ in $(\bigcup_{\Sigma} \sigma)^*$ such that $M_s \models \delta$ and $M_s \models \langle \sigma_1 \rangle...\langle \sigma_n \rangle \gamma$, is called a plan to achieve the goal $\gamma$ in $M_s$.<fnref n="11" /> As the set of epistemic actions $\Sigma$ for the given planning problem is finite, we can view $\bigcup_{\Sigma} \sigma$ as a single non-deterministic program $\pi$. The problem whether $\delta \wedge \langle \pi^* \rangle \gamma$ is satisfiable is often undecidable [21], and the target in the epistemic planning community is to find decidable planning problems. The undecidability resides in the part $\langle \pi^* \rangle$. In cases where $\langle \pi^* \rangle$ can be seen as a quantifier $\langle \bullet \rangle$ (such as APAL or AAML, see Section 8.1), this epistemic planning problem is decidable if the logic with language $\mathcal{L}(\diamond, \bullet, \langle \bullet \rangle)$ is decidable. The search for decidable logics with quantification over information change is therefore related to the search for decidable planning problems and to epistemic synthesis.

The complexities may still be different. Expression $\delta \wedge \langle \bullet \rangle \gamma$ contains a single quantifier, but an arbitrary formula in $\mathcal{L}(\diamond, \bullet, \langle \bullet \rangle)$ may contain multiple quantifiers. So, even when decidable, the complexity of the problem whether any formula $\varphi$ is satisfiable may be higher than the complexity of the problem whether the particular formula $\delta \wedge \langle \bullet \rangle \gamma$ is satisfiable.

There is also a difference in focus. Planning is typically about factual change (put block B on top of block C), and epistemic planning in dynamic epistemic logic is about combinations of epistemic and factual change [39, 41]. The quantification is then over a larger set of epistemic actions (see Section 8.2). Epistemic planning is an excellent vehicle to bring applications of dynamic epistemic logic within reach, such as robot planning [42] (in a language with common knowledge, factual change, and action models) and cognitive planning [50] (involving modalities for intentions and attitudes).

<footnote n="11">¹¹For non-deterministic epistemic actions it is common in the planning community to define by abbreviation $(\sigma)\varphi = \langle\sigma\rangle\varphi \wedge [\sigma]\varphi$ [43]. We then require $M_s \models (\sigma_1)...(\sigma_n)\gamma$.</footnote>
## 8.5 Open problems and further research

This is clearly a list of topics for further research and not a list of open problems:

* Decidable dynamic epistemic logics with arbitrary iteration of updates [104]

* Axiomatization of RML with common knowledge

* A dynamic epistemic logic of gossip [78]

* Quantifying over epistemic and ontic actions

# 9 Changing models with modalities

## 9.1 Sabotage logic and relation-changing logics

We have dwelled a long time within the confinement of dynamic epistemic logics, considering the various ways to quantify over epistemic actions interpreted as model updates with corresponding dynamic modalities, with the intention to model arbitrary information change. There is a different tradition in modal logic with update modalities that are quantifiers and that affect the domain of a model or change the relations of the model, including investigations involving modal $\mu$-calculus and determination of first-order definability of modal logical fragments [115, 129]. Such logics are not intended to model change of knowledge and are not considered dynamic epistemic logics. Let us call them *modal update logics*. We do not present such modal update logics in detail, but point out how dynamic epistemic logics can benefit from results obtained in modal update logics.

Modal update logics, with dynamic modalities for updates, are all very different and display a far greater variety than dynamic epistemic logics, but we can still roughly compare them with dynamic epistemic logics on a number of features. These features are not necessarily independent. Note that these features are informal, tentative, and (unless cited) not presented elsewhere.

* modal update logics permit local updates unlike the global updates in dynamic epistemic logics

* modal update logics permit semantic updates unlike the syntactic updates in dynamic epistemic logics

* modal update logics permit particular updates unlike the universal updates in dynamic epistemic logics

**Local versus global** The update in a dynamic epistemic logic is a model transformer and not a pointed model transformer. It is a function transforming a model into another model. We call this *global*. This induces a relation between points in the initial model and points in the updated model.
But the update is not a function of a pointed model. If it is, we call it *local*.

For example, a public announcement $\varphi$ induces a relation between a model $M$ and the restriction $M|\varphi$ of that model. This induces a relation between *pointed* epistemic models, for example, between $M_s$ and $(M|\varphi)_s$. But although $s$ plays a role in the relation, because after all $\varphi$ needs to be satisfied there, the state $s$ that is the point of $M$ does not determine the relation: any state $t$ in the domain of $M$ that also satisfies $\varphi$ and that is not the designated point is treated the same as $s$.

An update of $M_s$ removing a state $t$ different from $s$, or removing a pair $(s, t)$ from the accessibility relation, would be local.

This distinction between local and global was proposed in [20].

**Semantic versus syntactic** The model transformations in dynamic epistemic logic are almost always with respect to the extension of *formulas* evaluated in the initial model, such as the announcement $\varphi$ (or the preconditions of an action model, or the source and target conditions of an arrow update). In that sense the update is *syntactic* (formula dependent).

If instead of a restricted model $M|\varphi$ we were to consider a restricted model $M|T$ where $T$ is a subset of the domain of $M$, that may not be the extension of a formula, we call the update *semantic*.

Syntactic updates are typically less expressive than semantic updates, because the updated model is then a function of logical properties of the initial model. Indeed, public announcement logic is as expressive as epistemic logic.

**Particular versus universal** Instead of restricting the model to *all* states satisfying $\varphi$, or to *all* arrows (pairs in the accessibility relation) satisfying $\varphi$ at the source and $\psi$ at the target, as in dynamic epistemic logics, we now restrict the model by removing a state (that is, one state) in the domain, or a pair in the relation, as in sabotage logic [125].

Let us see a few of such model transforming logics [115, 125, 129, 20, 11, 61, 15, 14, 22, 81].

**Sabotage, bridge and swap** In Johan van Benthem's *sabotage games* [125] a network with multiple connections between nodes (representing travel destinations) is given, a player called Runner attempts to travel between two given nodes in the network and a player called Blocker attempts to sabotage the first player by removing nodes in the network after every move of Runner. If Runner cannot reach his destination, Blocker wins. Otherwise, Runner wins. The focus of [125] is on the complexities of solving such games (determine the winner). The modal semantics proposed in [125, p. 271] models removing a connection between destinations as removing a state in a corresponding Kripke model:

$$M_s \models \langle - \rangle \varphi \quad \text{iff} \quad \text{there is a } t \neq s \text{ such that } (M-t)_s \models \varphi$$

where $M-t$ is the model restriction of $M$ to $D(M) \setminus \{t\}$. The inequality requirement indicates a relation to the difference operator proposed in [54]. We can also see this as