\boldsymbol{an $\mathcal{S}5$ model} }M^{\prime}_{s^{\prime}}\text{ such that
}M_{s}\succeq M^{\prime}_{s^{\prime}}\text{ and
}M^{\prime}_{s^{\prime}}\models\varphi$

But the axiomatization is not straightforward. The axiomatization of
refinement modal logic on models with particular frame properties is not a
conservative extension of the axiomatization with respect to $\mathcal{K}$.
The axiom A4 above is unsound on class $\mathcal{S}5$.

###### Example 14

Consider axiom A4, with $\Phi_{a}=\\{\Box_{a}p,\neg\Box_{a}p\\}$ and
$\psi_{a}=\top$, and consider a two-state model wherein agent $a$ does not
know $p$. Then

$\Diamond_{a}\langle\succeq\rangle\Box_{a}p\wedge\Diamond_{a}\langle\succeq\rangle\neg\Box_{a}p$

is true: agent $a$ considers it possible that after having been informed of
$p$ she knows that $p$, and she also consider it possible that after having
been informed of $\top$ (after not having been informed), she still does not
know $p$. But

$\langle\succeq\rangle(\Diamond_{a}\Box_{a}p\wedge\Diamond_{a}\neg\Box_{a}p)$

is false: in a hypothetical model that is a refinement and wherein
$\Diamond_{a}\Box_{a}p\wedge\Diamond_{a}\neg\Box_{a}p$ is true, because of the
S5 validities $\Box_{a}\neg\Box_{a}\varphi\leftrightarrow\neg\Box_{a}\varphi$
and $\Box_{a}\Box_{a}\varphi\leftrightarrow\Box_{a}\varphi$ respectively, also
$\Box_{a}p\wedge\neg\Box_{a}p$ is true, which is inconsistent.

However, refinement epistemic logic _has_ been axiomatizated, 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, including $\mathcal{S}5$ and $\mathcal{K}D45$ (consistent belief) can
be found in [70, 69]. There are some surprises and open questions: transitive
refinement modal logic (RML on class $\mathcal{K}4$) is (strictly) more
expressive than K (an unpublished manuscript by French) and its axiomatization
is an open question.

###  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\quad\mbox{iff}\quad\text{there is
}M^{\prime}_{s^{\prime}}\text{ such that }M_{s}\succeq
M^{\prime}_{s^{\prime}}\text{ and }M^{\prime}_{s^{\prime}}\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\quad\mbox{iff}\quad\text{there is
}M^{\prime}_{s^{\prime}}\text{ such that }M_{s}\preceq
M^{\prime}_{s^{\prime}}\text{ and }M^{\prime}_{s^{\prime}}\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 [132], in
a language and semantics combining refinement and simulation in quantifiers.
We recall the A4 axiom of RML.

$\langle\succeq\rangle\bigwedge_{a\in
A}(\bigwedge_{\varphi_{a}\in\Phi_{a}}\Diamond_{a}\varphi_{a}\wedge\square_{a}\psi_{a})\leftrightarrow\bigwedge_{a\in
A}\bigwedge_{\varphi_{a}\in\Phi_{a}}\Diamond_{a}\langle\succeq\rangle(\varphi_{a}\wedge\psi_{a})$

The corresponding reduction for simulation is extrapolated from [132, Axiom
CCRKco2].

$\langle\preceq\rangle\bigwedge_{a\in
A}(\bigwedge_{\varphi_{a}\in\Phi_{a}}\Diamond_{a}\varphi_{a}\wedge\square_{a}\psi_{a})\leftrightarrow\bigwedge_{a\in
A}\Box_{a}\bigvee_{\varphi_{a}\in\Phi_{a}}\langle\preceq\rangle(\varphi_{a}\wedge\psi_{a})$

Simulation modal logic seems less of interest than refinement modal logic, as
it quantifies over models with even more uncertainty than the current one.
Refinement preserves ‘hard knowledge’, factual knowledge, and in general the
positive formulas. Whereas simulation ‘preserves’ ignorance of facts (and one
could define such ‘negative’ formulas in general). There are very many even
less informed states that could have resulted in the current state … Still, it
seems worthwhile to investigate simulation modal logic in depth, and in
particular on the class $\mathcal{S}5$: _simulation epistemic logic_ , and to
obtain synthesis for that.

###  7.4 Open problems

  * •

Given refinement modal $\mu$-calculus, what are refinement CTL and refinement
PDL and in particular their expressivity relative to CTL respectively PDL?

  * •

The axiomatization of simulation modal logic for a single simulation
quantifier $\langle\succeq\rangle$ (for all agents).

  * •

The axiomatization of simulation epistemic logic (on class $\mathcal{S}5$).

  * •

Synthese for different refinement and simulation modal logics.

##  8 Iterated updates, planning and group epistemics

The final two sections of this survey are more exploratory in nature.

###  8.1 Iterated updates

So far, we always considered dynamic modalities $\langle\pi\rangle$, where
$\pi$ is an _update_ , some kind of program inducing transformation of an
epistemic model, not necessarily deterministically, and where $\pi$ is one out
of a parameter set $\Pi$, that is possibly very large but almost always
enumerable. And we then considered a modality $\langle\bullet\rangle$, a
quantifier, for there is a $\pi\in\Pi$ such that $\langle\pi\rangle\varphi$.
Considering $\pi$ as a program, $\bullet$ represents non-deterministic choice
between all $\pi$, such that $\langle\bullet\rangle\varphi$ is equivalent to
$\langle\bigcup_{\Pi}\pi\rangle\varphi$ (where we abbreviate
$\bigcup_{\pi\in\Pi}\pi$ as $\bigcup_{\Pi}\pi$) and therefore also to
$\bigvee_{\Pi}\langle\pi\rangle\varphi$.

##### Iterated arbitrary updates

Most of our quantifiers satisfy
$\varphi\rightarrow\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, an arrow update,
a group announcement, etc. For this trivial $\pi$ the equivalence
$\varphi\leftrightarrow\langle\pi\rangle\varphi$ is valid. With implication
$\langle\pi\rangle\varphi\rightarrow\langle\bullet\rangle\varphi$ that gives
us $\varphi\rightarrow\langle\bullet\rangle\varphi$.

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

And also, most quantifiers satisfy
$\langle\bullet\rangle\langle\bullet\rangle\varphi\rightarrow\langle\bullet\rangle\varphi$.
This is not obvious. Let us investigate that for some of the quantifiers we
have seen. 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$
[120]. A sequence of two action models is again an action model, namely the
composition of those two action models (see Section 2). Also, a sequence of
two arrow updates is an arrow update, the relational composition of two
refinements is again a refinement, and the relational composition of two
simulations is again a simulation. A group announcement by $G$ followed by a
group announcement by $H$ is again a group announcement, namely by $G\cup H$,
where we recall that
$\langle!_{G}\rangle\langle!_{H}\rangle\varphi\rightarrow\langle!_{G\cup
H}\rangle\varphi$ is a validity of GAL.

From
$\langle\bullet\rangle\varphi\rightarrow\langle\bullet\rangle\langle\bullet\rangle\varphi$
and
$\langle\bullet\rangle\langle\bullet\rangle\varphi\rightarrow\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}$, and also using
$\varphi\rightarrow\langle\bullet\rangle\varphi$ this gets us
$\langle\bullet\rangle\varphi\leftrightarrow\langle\bullet\rangle^{*}\varphi$
(where $*$ is the Kleene-$*$). Differently said, the set $\Pi$ is closed under
composition: $(\bigcup_{\Pi}\pi)^{*}={\bigcup_{\Pi}\pi}$.

##### Iterated updates

What about $\langle\pi^{*}\rangle\varphi$ for a given $\pi$? (We may 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\in\Pi$, and dynamic epistemic languages with so-called infinitary
(dynamic) modalities for such arbitrary iteration. Such iterated updates have
to our knowledge rarely been investigated as part of the dynamic epistemic
logical language. The exception is [84], wherein it is shown that already for
very simple settings ($\mathcal{K}$ models, single-agent) the logic become
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. Note that the arbitrary
iteration in epistemic PDL of [106] 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 LCC) does not allow iteration of updates.

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 ‘usual’ languages
${\mathcal{L}}(\Diamond)$, ${\mathcal{L}}(\Diamond,!)$ or
${\mathcal{L}}(\Diamond,\otimes)$. We will not venture an exhaustive survey.
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 [94] 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 [30] 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 ‘asympotic’ knowledge properties of
epistemic models after arbitrary iteration of ‘learning’ input represented as
action models [27, 38]. 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 are ‘telephone calls’, where the denotation of such a
protocol is a set of possibly infinite call sequences. Given the restricted
setting, the informative consequences of call sequences are bounded: stable
information points again, in execution trees generated by such protocols [9,
125]. Such analysis are PDL-style analyses, and although such calls can be
modelled as action models [63], it is not entirely clear yet 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.

##### From arbitrary update to iterated update

The gap between arbitrary information change, modeled as non-deterministic
choice or as quantification, and iterated specific information change, is not
as wide as it may appear on first sight.

On the one hand, information change is not always so arbitrary and may be much
more restricted. We have seen various quantifiers over more restricted
languages, such as arbitrary positive and Boolean announcements, and arbitrary
announcements restricted to formulas with only atoms $Q\subseteq P$. This can
be even more restricted and still arbitrary, for example, quantifying over
Boolean announcements of restricted sets of variables, quantifying over action
models for gossip, etc. In principle this is way towards taming such logics
into decidability, lower complexities, finitary axiomatizations, and so on.
Admittedly, it is more of a slow road than a proper highway, we recall that
most such versions remain undecidable or without known finitary
axiomatizations.

On the other hand, iteration of specific information change is not always so
specific and may be iteration over a much more unrestricted set of epistemic
actions. For example, it may be iteration of non-deterministic choice between
some finite set of actions, such as iteration of (any point in) a given action
model (as in epistemic planning, discussed below), etc.

Let us make this slightly more precise.

As said, given the set $\Pi$ of all programs, quantification means

$\langle\bullet\rangle\varphi\quad\text{iff}\quad\text{there is $\pi\in\Pi$
such that }\langle\pi\rangle\varphi$

If $\Pi^{\prime}\subseteq\Pi$ is some subset (the Booleans, the positive
formulas, …) we get

$\langle\bullet\rangle\varphi\quad\text{iff}\quad\text{there is
$\pi\in\Pi^{\prime}$ such that }\langle\pi\rangle\varphi$

If such a $\Pi^{\prime}$ is a finite set, for example, all valuations of a
finite set of atoms, or a finite set of (finite) action models, there is a
direct representation as a linguistic object. For example, for a finite set
$\Pi^{\prime}$ of finite pointed action models $\pi=E_{e}$ we can take their
direct sum $\sigma:=\oplus_{\Pi^{\prime}}\pi$ (seen as a multi-pointed action
model, where the set of points represents the union of all points $e$ for
$E_{e}\in\Pi$) and we then get

$\langle\bullet\rangle\varphi\quad\text{iff}\quad\langle\sigma\rangle\varphi$

Note that the direct sum of all finite action models is an action model, but
that it is no longer finite, and therefore cannot feature in an action model
modality in the logical language.

We now recall that our quantifiers are typically closed under iteration and
satisfy
$\langle\bullet\rangle\varphi\leftrightarrow\langle\bullet\rangle^{*}\varphi$.
Now if the set of updates represented by $\sigma$ is still closed under
iteration we get (where we recall that $\langle\sigma\rangle^{*}\varphi$ means
$\langle\sigma^{*}\rangle\varphi$):

$\langle\bullet\rangle\varphi\quad\text{iff}\quad\langle\sigma\rangle^{*}\varphi$

and we finally have arbitrary iteration as an alternative to arbitrary choice.
Unfortunately this is a rather big ‘if’. Given a set of epistemic actions that
we quantify over and that is closed under composition (and that is therefore
closed under iteration), its subsets may no longer be closed under iteration.
But some subsets remain closed under iteration: announcements of Booleans for
a finite set of propositional variables, the set of call sequences in gossip
protocols, etc. There is hope. The community wherein this is very actively
investigated to establish decision procedures is that of epistemic planning.

###  8.2 Epistemic planning

Let us assume multi-agent $\mathcal{S}5$ models. An epistemic planning problem
consists of an initial state $s$ (or a set of initial states), a finite set
$\Sigma$ of epistemic actions and a goal formula
$\gamma\in{\mathcal{L}}(\Diamond)$ [35, 34, 37]. Let us assume that we can
describe this initial state $s$ in logic by a formula
$\delta\in{\mathcal{L}}(\Diamond)$. This assumption is not entirely warranted:
assuming the initial state to be in finite model $M$, pointed model $M_{s}$
has characteristic formula $\delta$ in the language of epistemic logic plus
common knowledge, but not necessarily in ${\mathcal{L}}(\Diamond)$. On the
other hand, we are typically interested in finding plans for a whole range of
epistemic models satisfying certain initial conditions (any configuration
where block $C$ is on block $B$, any model wherein agent $a$ is ignorant of
fact $p$, …), and then it is warranted. On this assumption however, solving an
epistemic planning problem becomes the question whether

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

is satisfiable. If all $\sigma\in\Sigma$ are deterministic, some sequence
$\sigma_{1}\dots\sigma_{n}$ in $(\bigcup_{\Sigma}\sigma)^{*}$ and such that if
$M_{s}\models\delta$ also
$M_{s}\models\langle\sigma_{1}\rangle\dots\langle\sigma_{n}\rangle\gamma$, is
called a _plan_ to achieve the goal $\gamma$ in $M_{s}$.444For possibly non-
deterministic epistemic actions it is common in the planning community to
define by abbreviation
$(\pi)\varphi:=\langle\pi\rangle\varphi\wedge[\pi]\varphi$, or, equivalently
but more succinctly,
$(\pi)\varphi:=\langle\sigma\rangle\varphi\wedge[\pi]\varphi$ where $\sigma$
is the trivial action (such as the public announcement of $\top$) [37]. We
then require $M_{s}\models(\sigma_{1})\dots(\sigma_{n})\gamma$. As the set of
epistemic actions $\Sigma$ for the given planning problem is finite, we can
view $\bigcup_{\Sigma}\sigma$ as a single object $\tau$, as above. The problem
whether $\delta\rightarrow\langle\tau^{*}\rangle\gamma$ is satisfiable is
often undecidable [20], and the target in epistemic planning community is to
find decidable (if not tractable) planning problems. The undecidability of
$\delta\rightarrow\langle\tau^{*}\rangle\gamma$ resides in the part
$\langle\tau^{*}\rangle$, not in parts $\delta$ or $\gamma$. Let us now see
this $\langle\tau^{*}\rangle$ as some quantifier $\langle\bullet\rangle$, as
suggested in the previous paragraph. It seems that this epistemic planning
problem is undecidable if and only if the logic with language
${\mathcal{L}}(\Diamond,\langle\bullet\rangle)$ is undecidable. The search for
decidable logics with quantification over information change seems similar to
the search for decidable planning problems, and is related to epistemic
synthesis.

There is a difference in scale. Expression
$\delta\rightarrow\langle\bullet\rangle\gamma$ contains a single quantifier
(we recall that $\delta,\gamma\in{\mathcal{L}}(\Diamond)$, they are
quantifier-free). But an arbitrary
$\varphi\in{\mathcal{L}}(\Diamond,\langle\bullet\rangle)$ may contain multiple
$\langle\bullet\rangle$ quantifiers. So, if decidable, the complexity of such
a logic tends to be higher than the complexity of the planning problem
represented by a single $\langle\bullet\rangle$.

##### Factual change

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 its
incarnation in dynamic epistemic logic is typically about factual change given
partial observability of multiple agents, or about combinations of epistemic
(information) change and factual change. The quantification is then over an
even larger set of epistemic actions. Technically, it is easy and not
problematic at all. Factual change can be straightforwardly handled in action
model logic (see [106, 117]) and thus also in the extension of such logics
with quantifiers over information change. Conceptually however, it is
problematic, and in its unrestricted form rather absurd. For example, if in
arbitrary action model logic AAML we quantify over action models also allowing
factual change, $\langle\otimes\rangle\varphi$ becomes valid for any
consistent $\varphi$. Differently said, any formula $\varphi$ is realizable in
any epistemic model. This is because one can transform any pointed epistemic
model into any other pointed epistemic model by an action model also allowing
factual change.

For more restricted quantifiers, quantification over information change
including factual change makes sense, in particular for sets of epistemic
actions that are closed under composition. Indeed, epistemic planning
involving action models with factual change is standard fare [34, 36].

###  8.3 Group epistemic operators

Let us consider for a while logics with group epistemic operators, for a group
$G\subseteq A$ of agents. ‘Everybody in $G$ knows $\varphi$’, $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$’, $C_{G}\varphi$,
can be defined as the arbitrary iteration of everybody knows $\varphi$, or
semantically 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$’,
$D_{G}\varphi$, is most conveniently defined as truth of $\varphi$ in all
states reachable from a given state by the intersection relation
$\bigcap_{a\in G}R_{a}$.

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 [28, 120], which has
led to the proposal of relativized common knowledge [106]. Adding distributed
knowledge to public announcement logic is also non-trivial for the
axiomatization (proving completeness requires adjusting the standard canonical
model technique), and even more so because it needs a different notion of
bisimulation [130]. And also, 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, this landscape is more complex in the presence of group
epistemic operators. It is therefore not surprising that few proposals have
been made to extend (or compare) such logics with group epistemic modalities.
However, this is beginning to happen.

In [121, Section 4.3] arbitary 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 [59] various expressivity results for group announcement logic with
distributed knowledge are presented. (An extended journal version in press is
[60].)

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

##### APAL and GAL with common knowledge

A full-scale investigation of APAL and GAL with common knowledge is found in
[58]. For any of our languages ${\mathcal{L}}(\dots)$, let
${\mathcal{L}}(\dots,C)$ be the extension of the BNF with inductive construct
$C_{B}\varphi$ (for $B\subseteq A$). Let us focus on the APAL extensions.
Galimullin and Ågotnes consider different semantics for the APAL quantifier
$\langle!\rangle\varphi$. In all cases the quantification is over quantifier-
free formulas. But over formulas from different languages!

$\begin{array}[]{lcll}M_{s}\models\langle!\rangle\varphi&\text{iff}&\text{there
is a $\psi\in{\mathcal{L}}(\Diamond)$ such that
}M_{s}\models\langle\psi\rangle\varphi&\text{APALC}\\\ &&\text{there is a
$\psi\in{\mathcal{L}}(\Diamond,C)$ such that
}M_{s}\models\langle\psi\rangle\varphi&\text{APALC}^{X}\\\ &&\text{there is a
$\psi\in{\mathcal{L}}(\Diamond,!,C)$ such that
}M_{s}\models\langle\psi\rangle\varphi&\text{APALC}^{XX}\end{array}$

The GAL language extensions are defined analogously, we thus obtain GALC,
GALCX and GALCXX, and there are different results for those extensions. (The
notations APALXX and GALCXX are coined by us.) Now in APAL it does not matter
whether we quantify over ${\mathcal{L}}(\Diamond)$ (the language of multi-
agent epistemic logic) or over ${\mathcal{L}}(\Diamond,!)$ (the language of
public announcement logic), because PAL and epistemic logic have the same
expressivity. But, as mentioned, the logic with common knowledge and public
announcement is more expressive than the logic with common knowledge. So the
choice between ${\mathcal{L}}(\Diamond,!,C)$ and ${\mathcal{L}}(\Diamond,C)$
should affect the semantics of the quantifier.

There are results on expressivity and on axiomatization. The main expressivity
result is that APALC is not at least as expressive as APALCX, where the other
direction remains an open question. It is unclear where APALCXX fits in the
expressivity hierarchy. The proposed infinitary axiomatization for APALC
contains an infinitary derivation rule for common knowledge: “from
$E_{B}^{n}\varphi$ for all $n\in\mathbb{N}$, infer $C_{B}\varphi$” (where
$E_{B}\varphi$ abbreviates $\bigwedge_{a\in B}\Box_{a}\varphi$ and where
$E^{n}_{B}\varphi$ means $E_{B}\dots E_{B}\varphi$ for a stack of $n$
$E_{B}$s). This may appear surprising, until we realize that the rule to
introduce the quantifier $[!]$ (Section 3.4) is also infinitary. Having both
derivation rules infinitary simplifies the presentation and the completeness
proof.

##### Group epistemics when quantifying over epistemic actions

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. But we do not know of
any work on that. Such extensions would be relevant for epistemic planning and
for information-based security protocols (we recall Section 4.4), wherein
distributedly known initial problem configurations and commonly known
epistemic goals are important.

###  8.4 Open problems

  * •

Dynamic epistemic logics with arbitrary iteration of updates

  * •

Expressivity of APALCXX

  * •

Axiomatization of RML with common knowledge

  * •

A dynamic epistemic logic of gossip

  * •

Quantifying over information change and factual change

##  9 Changing models with modalities

###  9.1 Model changing logics

We have dwelled a long time within the confinement of dynamic epistemic
logics, considering the various ways to quantify over epistemic actions with
corresponding dynamic modalities, with the intention to model arbitrary
information change. There is a rather different approach to such matters that
is not necessarily intended to model (epistemic) information change, namely
various modal logics (typically not epistemic modal logics) with model
transforming/changing operators in an abstract setting, including
investigations involving modal $\mu$-calculus and determination of first-order
definability of modal logical fragments [93, 103]. We do not wish to present
these modal logics in detail, but to point out some ways in which dynamic
epistemic logics can benefit from results obtained in such investigations.

Why is this a different approach? Explaining this in some detail seems
worthwhile.

The basic update in a dynamic epistemic logic is a model transformer that is
both _global_ in the sense that the transformation does not depend on the
actual state, and also _syntactic_ in the sense that the transformation
depends on denotations of formulas in the logical language.

The model transformer in dynamic epistemic logic defines a partial, functional
relation between epistemic models. For example, this is the relation between a
model $M$ and the restriction $M|\varphi$ of that model, due to the
announcement of $\varphi$. This relation between models induces a relation
between _pointed_ epistemic models. For example, the relation for the public
announcement of $\varphi$ contains all pairs $(M_{s},M^{\prime}_{s^{\prime}})$
such that $M_{s}\models\varphi$ and $M^{\prime}_{s^{\prime}}$ is bisimilar to
$(M|\varphi)_{s}$. Note that the point plays no role in determining the
relation. The relation only depends on the model, and on the point being in
the domain of the updated model. In that sense it is global. The model
transformations are almost always with respect to the denotation of formulas
evaluated in the model that is to be transformed, such as the announcement
$\varphi$ (or such as the set of preconditions of an action model, or the set
of source and target conditions of an arrow update, already much more complex
functional relations). In that sense it is syntactic.

When quantifying over information change, we are investigating relations
containing such relations for specific (deterministic) updates. These
quantifiers do not induce novel model transformations or pointed model
transformations (except for refinements).

The model changing or model transforming logics of this section have
modalities interpreted as updates that are relations between pointed models
that are not pointwise induced from functional relations between non-pointed
models. 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, we now restrict the model by removing
_some_ state in the domain, or _some_ pair in the relation, or some state or
pair satisfying a certain logical condition.

There are obvious connections with dynamic epistemic logics, because if you
remove enough of ‘some’ states, you remove all states, and if you remove
enough of ‘some’ states satisfying $\varphi$, you remove all and we have the
public announcement of $\varphi$ again. Arbitrary iteration seems a way to get
from ‘some’ to ‘all’, but these are slippery slopes.

Another direction in such model changing logics are relations between pointed
models that are not merely induced by a (non-pointed) model change, but that
really depend on the point. For example, remove some state linked (in a pair
of the accessibility relation) to the state that is the point of the given
model; so not just any state.

Overall it seems that such arbitrarily model changing logics allow more
modelling freedom, so that dynamic epistemic logics are a special case, but
even that is not so clear.

Let us see a few of such model transforming logics, as reported in [93, 99,
103, 19, 10, 49, 14, 13, 21, 66].

##### Sabotage, bridge and swap

Van Benthem proposed sabotage games [99] wherein a network with multiple
connections between nodes is given, a player called Runner attempts to travel
between two given nodes in the network and a player 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 [99] is on the complexities of solving such games
(determine the winner). The modal semantics proposed in [99, p. 271] models
removing a link between destination nodes as removing (deleting) 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
${\mathcal{D}}(M)\setminus\\{t\\}$. The inequality requirement indicates a
relation to the difference operator proposed in [47]. We can also see this as
‘poisoning’ or colouring that state, i.e., forbidding passage through it, as
in e.g. [66]. Issues with axiomatizing sabotage modal logic and relations to
other relation changing modal logics are presented in [21].

Another semantics for the sabotage modality, propagated in later works and
also in various works by Areces et al. [10, 49] interprets removing the
sabotage modality as removing a pair from the accessibility relation in a
model. We then get:

$M_{s}\models\langle-\rangle\varphi\quad\text{iff}\quad\text{there is a
}(t,u)\in R\text{ such that }(M|R^{-tu})_{s}\models\varphi$

where $M|R^{-tu}$ is the restriction of $M$ to the relation $R^{-}$ defined as
$R^{\prime}=R\setminus\\{(t,u)\\}$.

Instead of removing a pair from the relation, we can also add a pair to the
relation, also known as making a bridge between states:

$M_{s}\models\langle+\rangle\varphi\quad\text{iff}\quad\text{there is a
}(t,u)\notin R\text{ such that }(M|R^{+tu})_{s}\models\varphi$

where $M|R^{+tu}$ is as $M$ except that $R^{+}=R\cup\\{(t,u)\\}$. Or we can
change the direction of the arrow, known as a swap of the states involved in
the arrow [10, 49]:

$M_{s}\models\langle{\pm}\rangle\varphi\quad\text{iff}\quad\text{there is a
}(t,u)\in R\text{ such that }(M|R^{{\pm}tu})_{s}\models\varphi$

where $M|R^{{\pm}tu}$ is as $M$ except that
$R^{tu}=R\setminus\\{(t,u)\\}\cup\\{(u,t)\\}$.

Sabotage, bridge and swap are all examples of relational change and such model
changing modal logics therefore also go by the name of relation changing modal
logics.

##### Local and global change, and numbers and names

One should distinguish model change independent from the state of evaluation
from model change relative to the state of evaluation. The former is called
global change and the latter is called local change. The original sabotage
semantics from [99] is local in that sense: we remove a state different from
the actual state. So, the local semantics has shape:
$M_{s}\models\langle\bullet\rangle\varphi$ if $\varphi$ is true in
$M^{\prime}_{s}$ where $M^{\prime}$ is different from $M$ with respect to the
set $R(s)$ of states accessible from $s$. Sabotage semantics is local with
respect to the relation for the universal modality. For the sabotage, swap,
and bridge updates of Areces et al. both global and local versions have been
proposed, and see also [19]. All updates in dynamic epistemic logic that we
have seen in prior sections are global.

In such sabotage and related logics we can count. If you remove a state from
the domain, the resulting domain contains one state less, so if you do this
three times it contains three states less. We can therefore count how many
states there are in the (finite) domain, just as in for example the graded
modal logics of [52]. These logics with counting require more refined notions
of bisimulation, because the size of a model is not an invariant for the usual
notion of bisimulation. For example, a model is bisimilar to two copies of it.
Bisimulation for sabotage logic is proposed in [21], and for relation changing
logics in general in [11, 50], including for a variation of the
$\langle-\rangle$ and $\langle+\rangle$ semantics above, namely where the
removal of a pair $(t,u)$ is also defined if the pair was already absent, and
the addition of a pair $(t,u)$ also defined if it was already present.

In such logics we can also give names to the states in domain. If you remove a
state from the domain different from the actual state, this allows you to
refer to the actual state in the logical language, as in hybrid logics. In
[12], relation changing logics are modelled as hybrid logics.

When we can count worlds and give them names, the logics may lack (finitary)
Hilbert-style axiomatizations and may be undecidable, which is indeed the case
[21, 14, 13].

###  9.2 Dynamic epistemic logics and model changing logics

Let us now observe some relations between the model changing modal logics and
the dynamic epistemic logics presented in this survey. We can consider
arbitrary iterations or fixpoints of the structural operations wherein a mere
pair of the accessibility relation is changed [93, 103], and determine to what
extent such transformations correspond to dynamic epistemic updates.

First consider refinement modal logic RML. Removing a pair from the relation
of a model is a refinement of that model. Removing any finite number of pairs
is also a refinement of that model. As is removing any infinite number of
pairs of the relation, or the entire relation, which may be the limit or
fixpoint of this operation (the models on which we perform such operations
need not have countable domains). So refinement modal logic RML is clearly
somehow related to sabotage modal logic. It may be interesting to investigate
on which class of models (all finite models?) we have that

> $\langle\succeq\rangle\varphi$ is equivalent to
> $\langle-\rangle^{*}\varphi$.

Now sabotage modal logic is a fairly difficult modal logic (undecidable, …),
and including infinitary modalities such as going from $\langle-\rangle$ to
$\langle-\rangle^{*}$ often makes life even harder. Whereas RML is a fairly
simple modal logic: we can eliminate the refinement quantifier and it is as
expressive as the logic K. Of course in RML we only have a single
$\langle\succeq\rangle$ modality, which we should compare to a logic with only
the $\langle-\rangle^{*}$ modality as a quantifier, not to a sabotage logic
extension with $\langle-\rangle$ and $\langle-\rangle^{*}$.

Similarly, the quantifier in simulation modal logic can be seen as arbitrary
iteration of the bridge modality, such that it is envisageable for some model
class that

> $\langle\preceq\rangle\varphi$ is equivalent to
> $\langle+\rangle^{*}\varphi$.

Now consider arrow update logics AUL and AUML, wherein pairs of the
accessibility relation come with logical conditions, i.e., they are arrows
with source or target formulas. In sabotage logic we delete pairs, whereas in
AUL we retain pairs, but this is mere perspective. _Retaining_ all pairs
$(s,t)$ with source condition $\varphi$ and target condition $\psi$ in a
relation $R_{a}$ — that is: arrow $(\varphi,a,\psi)$ — is the same as
_deleting_ all pairs that satisfy $\neg\varphi$ at the source or $\neg\psi$ at
the target.

Take public announcement of an atom $p$ as an example, where we assume there
is a single agent $a$ only. First consider an arrow $(\top,a,p)$ satisfying
$p$ at the target. Retaining pairs in the accessibility relation satisfying
that arrow means deleting pairs not satisfying $p$ at the target state.
Iterating the removal (sabotage) of such arrows until a fixpoint leaves us
with all arrows pointing to $p$ states. This corresponds to the ‘arrow
eliminating’ semantics for public announcement [64, 76].

Similarly, as noted in Section 6 on such arrow update logics, removing all
pairs with different values for $p$ at source and target, so preserving all
pairs satisfying $(p,a,p)$ or $(\neg p,a,\neg p)$, corresponds to the standard
public announcement semantics, in the model refinement sense of [104].

What works for propositional variables may not work for arbitrary formulas.
Public announcement of $\varphi$ is not merely iterated sabotage relative to
target formula $\neg\varphi$, because of Moorean phenomena. It can only be
simultaneous sabotage relative to target $\neg\varphi$. Iterated removal of
arrows not satisfying $\varphi$ at the target state need not be a fixpoint
[94, 7], and even if it is, it need not correspond to the public announcement
of $\varphi$. Consider some model $M$ and the model $M^{-st}$ wherein a pair
$(s,t)$ such that $M_{t}\not\models\varphi$ has been removed. Then the
denotation of $\varphi$ in $M^{-st}$ need not be the restriction of the
denotation of $\varphi$ in $M$ to the new domain. Differently said,
$M_{u}\not\models\varphi$ for some state $u$ does not guarantee that
$M^{-st}_{u}\not\models\varphi$.

That public announcement can be viewed as iterated removal of states or arrows
was suggested by Van Benthem (in oral communication), although this seems not
explicitly addressed in any of the relevant publications [103, 21, 105]. A
‘stepwise public announcement’ (one pair in the accessibility relation only)
was proposed in [21] as an alternative for the (usual) ‘global’ public
announcement (see Section 6.2, Stepwise versions of DEL, in [21]); and [105]
interestingly combines public announcement and ‘stepwise removal’ (sabotage)
in a single logic, but does not suggest that one can be defined in terms of
the other.

Alternatively to iterating the procedure of removing pairs $(s,t)$ where
$\varphi$ _is_ false in $t$ we can iterate the procedure of removing pairs
$(s,t)$ where $\varphi$ _was_ (originally) false in $t$, even when $\varphi$
is currently true in $t$ due to Moorean phenomena. But for that we need either
models with memory (we recall [29]) or we need to store the original
denotation of $\varphi$ in a fresh variable $p$ with an assignment [82, 114],
and from then on remove arrows failing to satisfy $p$ in the target. These are
more complex modelling solutions.

How to view updates induced by arrow update models or action models as
iterated sabotage also seems more complex, as this may increase the modal
complexity of the updated domain (it can become bigger). For this it seems
important to have a point-generated tree representation of the model, as in
refinement modal logic.

###  9.3 Open problems

  * •

A decidable and axiomatizable relation changing logic

  * •

Refinement modal logic as sabotage modal logic with infinitary modalities

  * •

Public announcement logic as iterated sabotage on the class of finite models

## Acknowledgements

This investigation is a follow-up of a prior survey of logics with quantifiers
over information change, entitled ‘Quantifying Notes’ [109], that also focused
on open problems. Some open problems in [109] have since then been resolved
and are now presented as results, for example on GAL and CAL expressivity.
Other open problems have come to the fore.

I acknowledge helpful comments and encouragement from: Thomas Ågotnes,
Philippe Balbiani, Johan van Benthem, Stéphane Demri, Raul Fervari, Saúl
Fernández González, Tim French, Rustam Galimullin, Rob van Glabbeek, Davide
Grossi, Wiebe van der Hoek, Sophie Pinchinat, and Igor Sedlár. This survey got
under way while I was under confinement in France in the same apartment
complex as Hao Wu and Jinsheng Chen. Their support was invaluable and
unforgettable.

Together with Thomas Bolander, Jan van Eijck and Ramanujam, in 2015 I
organized a Lorentz Center workshop with the same title as this survey, with a
subtitle ‘for clarity’:
https://www.lorentzcenter.nl/to-be-announced-synthesis-of-epistemic-
protocols.html.
And on various occasions I gave invited seminars entitled ‘To Be Announced’.
The predictable confusion this causes with publishers, supporting staff and
events servers has always been hilarious and I hope it will be never-ending.

## References

  * [1] A. Achilleos and M. Lampis.  Closing a gap in the complexity of refinement modal logic.  URL: http://arxiv.org/abs/1309.5184.
  * [2] T. Ågotnes.  Action and knowledge in alternating-time temporal logic.  Synthese (Special Section on Knowledge, Rationality and Action), 149(2):377–409, 2006.
  * [3] T. Ågotnes, P. Balbiani, H. van Ditmarsch, and P. Seban.  Group announcement logic.  Journal of Applied Logic, 8:62–81, 2010.
  * [4] T. Ågotnes and H. van Ditmarsch.  Coalitions and announcements.  In Proc. of 7th AAMAS, pages 673–680. IFAAMAS, 2008.
  * [5] T. Ågotnes, H. van Ditmarsch, and T. French.  The undecidability of group announcements.  In Proc. of the 13th AAMAS, pages 893–900, 2014.
  * [6] T. Ågotnes, H. van Ditmarsch, and T. French.  The undecidability of quantified announcements.  Studia Logica, 104(4):597–640, 2016.
  * [7] T. Ågotnes, H. van Ditmarsch, and Y. Wang.  True lies.  Synthese, 2017.  URL: http://arxiv.org/abs/1606.08333, doi:10.1007/s11229-017-1423-y.
  * [8] R. Alur, T. A. Henzinger, and O. Kupferman.  Alternating-time temporal logic.  Journal of the ACM, 49:672–713, 2002.
  * [9] K.R. Apt and D. Wojtczak.  Verification of distributed epistemic gossip protocols.  J. Artif. Intell. Res., 62:101–132, 2018.  doi:10.1613/jair.1.11204.
  * [10] C. Areces, R. Fervari, and G. Hoffmann.  Moving arrows and four model checking results.  In Proc. of 19th WoLLIC, LNCS 7456, pages 142–153. Springer, 2012\.
  * [11] C. Areces, R. Fervari, and G. Hoffmann.  Relation-changing modal operators.  Log. J. IGPL, 23(4):601–627, 2015.  doi:10.1093/jigpal/jzv020.
  * [12] C. Areces, R. Fervari, G. Hoffmann, and M. Martel.  Relation-changing logics as fragments of hybrid logics.  In D. Cantone and G. Delzanno, editors, Proc. of the 7th GandALF, volume 226 of EPTCS, pages 16–29, 2016.  doi:10.4204/EPTCS.226.2.
  * [13] C. Areces, R. Fervari, G. Hoffmann, and M. Martel.  Undecidability of relation-changing modal logics.  In A. Madeira and M. Benevides, editors, Proc. of 1st DALI, LNCS 10669, pages 1–16. Springer, 2017.  doi:10.1007/978-3-319-73579-5\\_1.
  * [14] C. Areces, R. Fervari, G. Hoffmann, and M. Martel.  Satisfiability for relation-changing logics.  J. Log. Comput., 28(7):1443–1470, 2018.  doi:10.1093/logcom/exy022.
  * [15] C. Areces, H. van Ditmarsch, R. Fervari, and F. Schwarzentruber.  The modal logic of copy and remove.  Inf. Comput., 255:243–261, 2017.  doi:10.1016/j.ic.2017.01.004.
  * [16] G. Aucher.  Characterizing updates in dynamic epistemic logic.  In Proceedings of Twelfth KR. AAAI Press, 2010.
  * [17] G. Aucher.  DEL-sequents for regression and epistemic planning.  Journal of Applied Non-Classical Logics, 22(4):337–367, 2012.
  * [18] G. Aucher.  Dynamic epistemic logic in update logic.  J. Log. Comput., 26(6):1913–1960, 2016.  doi:10.1093/logcom/exw002.
  * [19] G. Aucher, P. Balbiani, L. Fariñas del Cerro, and A. Herzig.  Global and local graph modifiers.  Electr. Notes Theor. Comput. Sci., 231:293–307, 2009.
  * [20] G. Aucher and T. Bolander.  Undecidability in epistemic planning.  In F. Rossi, editor, Proc. of 23rd IJCAI, pages 27–33, 2013\.
  * [21] G. Aucher, J. van Benthem, and D. Grossi.  Modal logics of sabotage revisited.  J. Log. Comput., 28(2):269–303, 2018.  doi:10.1093/logcom/exx034.
  * [22] R.J. Aumann.  Agreeing to disagree.  Annals of Statistics, 4(6):1236–1239, 1976.
  * [23] P. Balbiani.  Putting right the wording and the proof of the Truth Lemma for APAL.  Journal of Applied Non-Classical Logics, 25(1):2–19, 2015.
  * [24] P. Balbiani, A. Baltag, H. van Ditmarsch, A. Herzig, T. Hoshi, and T. De Lima.  ‘Knowable’ as ‘known after an announcement’.  Review of Symbolic Logic, 1(3):305–334, 2008.
  * [25] P. Balbiani and H. van Ditmarsch.  A simple proof of the completeness of APAL.  Studies in Logic, 8(1):65–78, 2015.
  * [26] P. Balbiani, H. van Ditmarsch, and A. Herzig.  Before announcement.  In L.D. Beklemishev, S. Demri, and A. Maté, editors, Advances in Modal Logic 11, pages 58–77. College Publications, 2016.
  * [27] A. Baltag, N. Gierasimczuk, and S. Smets.  Truth-tracking by belief revision.  Studia Logica, 107(5):917–947, 2019.  doi:10.1007/s11225-018-9812-x.
  * [28] A. Baltag, L.S. Moss, and S. Solecki.  The logic of public announcements, common knowledge, and private suspicions.  In Proc. of 7th TARK, pages 43–56. Morgan Kaufmann, 1998.
  * [29] A. Baltag, A. Özgün, and A.L. Vargas Sandoval.  APAL with memory is better.  In Proc. of 25th WoLLIC, LNCS 10944, pages 106–129, 2018.
  * [30] A. Baltag and S. Smets.  Group belief dynamics under iterated revision: fixed points and cycles of joint upgrades.  In Proc. of 12th TARK, pages 41–50, 2009.
  * [31] A. Bjorndahl.  Topological subset space models for public announcements.  In H. van Ditmarsch and G. Sandu, editors, Jaakko Hintikka on knowledge and game-theoretical semantics, Outstanding contributions to logic 12, pages 165–186. Springer, 2018.
  * [32] A. Bjorndahl and A. Özgün.  Logic and topology for knowledge, knowability, and belief.  The Review of Symbolic Logic, 2019.  Online first on https://doi.org/10.1017/S1755020319000509.  doi:10.1017/S1755020319000509.
  * [33] P. Blackburn, M. de Rijke, and Y. Venema.  Modal Logic.  Cambridge University Press, Cambridge, 2001.
  * [34] T. Bolander.  A gentle introduction to epistemic planning: The DEL approach.  In Proc. of the 9th ICLA, volume 243 of EPTCS, pages 1–22, 2017.
  * [35] T. Bolander and M.B. Andersen.  Epistemic planning for single and multi-agent systems.  Journal of Applied Non-classical Logics, 21(1):9–34, 2011.
  * [36] T. Bolander, T. Charrier, S. Pinchinat, and F. Schwarzentruber.  Del-based epistemic planning: Decidability and complexity.  Artif. Intell., 287:103304, 2020.  doi:10.1016/j.artint.2020.103304.
  * [37] T. Bolander, T. Engesser, A. Herzig, R. Mattmüller, and B. Nebel.  The dynamic logic of policies and contingent planning.  In Proc. of 16th JELIA, volume 11468 of Lecture Notes in Computer Science, pages 659–674. Springer, 2019.  doi:10.1007/978-3-030-19570-0\\_43.
  * [38] T. Bolander and N. Gierasimczuk.  Learning to act: qualitative learning of deterministic action models.  J. Log. Comput., 28(2):337–365, 2018.  doi:10.1093/logcom/exx036.
  * [39] L. Bozzelli, H. van Ditmarsch, T. French, J. Hales, and S. Pinchinat.  Refinement modal logic.  Information and Computation, 239:303–339, 2014.
  * [40] L. Bozzelli, H. van Ditmarsch, and S. Pinchinat.  The complexity of one-agent refinement modal logic.  Theoretical Computer Science, 603:58–83, 2015.  doi:10.1016/j.tcs.2015.07.015.
  * [41] M. Browne, E. Clarke, and O. Grümberg.  Characterizing Kripke structures in temporal logic.  In H. Ehrig, R. Kowalski, G. Levi, and U. Montanari, editors, TAPSOFT ’87, LNCS 249, pages 256–270. Springer, 1987.
  * [42] T. Charrier and F. Schwarzentruber.  Arbitrary public announcement logic with mental programs.  In Proc. of AAMAS, pages 1471–1479. ACM, 2015.
  * [43] A. Dabrowski, L.S. Moss, and R. Parikh.  Topological reasoning and the logic of knowledge.  Ann. Pure Appl. Logic, 78(1-3):73–110, 1996.  doi:10.1016/0168-0072(95)00016-X.
  * [44] T. de Lima.  Alternating-time temporal announcement logic.  In Proceedings of CLIMA XII, LNCS 6814, pages 105–121. Springer, 2011.
  * [45] T. de Lima.  Alternating-time temporal dynamic epistemic logic.  J. Log. Comput., 24(6):1145–1178, 2014.  doi:10.1093/logcom/exs061.
  * [46] T. de Lima.  A Little about Action, Knowledge, Belief and a Lot about Modal Logic.  University of Artois, CRIL, Lens, 2019.  Habilitation Thesis.
  * [47] M. de Rijke.  The modal logic of inequality.  Journal of Symbol Logic, 57:566–584, 1992.
  * [48] A. Ehrenfeucht.  An application of games to the completeness problem for formalized theories.  Fundamenta Mathematicae, 49:129–141, 1961.
  * [49] R. Fervari.  Relation-Changing Modal Logics.  PhD thesis, Universidad Nacional de Córdoba, Argentina, 2014.
  * [50] R. Fervari, F. Trucco, and B. Ziliani.  Verification of dynamic bisimulation theorems in coq.  J. Log. Algebraic Methods Program., 120:100642, 2021.  doi:10.1016/j.jlamp.2021.100642.
  * [51] K. Fine.  Propositional quantifiers in modal logic.  Theoria, 36(3):336–346, 1970.
  * [52] K. Fine.  In so many possible worlds.  Notre Dame Journal of Formal Logic, 13(4):516–520, 1972.
  * [53] F.B. Fitch.  A logical analysis of some value concepts.  The Journal of Symbolic Logic, 28(2):135–142, 1963.
  * [54] T. French.  Bisimulation quantifiers for modal logic.  PhD thesis, University of Western Australia, 2006.
  * [55] T. French, R. Galimullin, H. van Ditmarsch, and N. Alechina.  Groups versus coalitions: On the relative expressivity of GAL and CAL.  In Proc. of 18th AAMAS, pages 953–961, 2019.
  * [56] T. French and H. van Ditmarsch.  Undecidability for arbitrary public announcement logic.  In Advances in Modal Logic 7, pages 23–42. College Publications, 2008.
  * [57] R. Galimullin.  Coalition announcements.  PhD thesis, University of Nottingham, UK, 2019.
  * [58] R. Galimullin and T. Ågotnes.  Quantified announcements and common knowledge.  In Proc. of 20th AAMAS, pages 528–536, 2021.  URL: https://dl.acm.org/doi/10.5555/3463952.3464018.
  * [59] R. Galimullin, T. Ågotnes, and N. Alechina.  Group announcement logic with distributed knowledge.  In P. Blackburn, E. Lorini, and M. Guo, editors, Proc. of 7th LORI, LNCS 11813, pages 98–111, 2019.  doi:10.1007/978-3-662-60292-8\\_8.
  * [60] R. Galimullin, T. Ågotnes, and N. Alechina.  Logics with group announcements and distributed knowledge: Completeness and expressive power.  2021\.  To appear.
  * [61] R. Galimullin and N. Alechina.  Coalition and group announcement logic.  In Proc. of 16th TARK, pages 207–220, 2017.  doi:10.4204/EPTCS.251.15.
  * [62] R. Galimullin, N. Alechina, and H. van Ditmarsch.  Model checking for coalition announcement logic.  In F. Trollmann and A. Turhan, editors, Proc. of 41st German KI, LNCS 11117, pages 11–23, 2018.  doi:10.1007/978-3-030-00111-7\\_2.
  * [63] M. Gattinger.  New Directions in Model Checking Dynamic Epistemic Logic.  PhD thesis, University of Amsterdam, 2018.
  * [64] J.D. Gerbrandy and W. Groeneveld.  Reasoning about information change.  Journal of Logic, Language, and Information, 6:147–169, 1997.
  * [65] R. Goldblatt.  Axiomatising the Logic of Computer Programming.  Springer-Verlag, 1982.
  * [66] D. Grossi and S. Rey.  Credulous acceptability, poison games and modal logic.  In Proc. of the 18th AAMAS, pages 1994–1996. IFAAMAS, 2019.  URL: http://dl.acm.org/citation.cfm?id=3331988.
  * [67] J. Hales.  Refinement quantifiers for logics of belief and knowledge.  Honours Thesis, University of Western Australia, 2011.
  * [68] J. Hales.  Arbitrary action model logic and action model synthesis.  In Proc. of 28th LICS, pages 253–262. IEEE, 2013.
  * [69] J. Hales.  Quantifying over epistemic updates.  PhD thesis, School of Computer Science & Software Engineering, University of Western Australia, 2016.  URL: https://research-repository.uwa.edu.au/en/publications/quantifying-over-epistemic-updates.
  * [70] J. Hales, T. French, and R. Davies.  Refinement quantified logics of knowledge.  Electr. Notes Theor. Comput. Sci., 278:85–98, 2011.
  * [71] R. Hilpinen.  Remarks on personal and impersonal knowledge.  Canadian Journal of Philosophy, 7:1–9, 1977.
  * [72] J. Hintikka.  Knowledge and Belief.  Cornell University Press, 1962.
  * [73] M. Hollenberg.  Logic and bisimulation.  PhD thesis, University of Utrecht, 1998.
  * [74] J.F. Horty.  Agency and deontic logic.  Oxford University Press, 2001.
  * [75] W. Jamroga and W. van der Hoek.  Agents that know how to play.  Fundamenta Informaticae, 63:185–219, 2004.
  * [76] B. Kooi.  Expressivity and completeness for public update logics via reduction axioms.  Journal of Applied Non-Classical Logics, 17(2):231–254, 2007.
  * [77] B. Kooi and B. Renne.  Arrow update logic.  Review of Symbolic Logic, 4(4):536–559, 2011.
  * [78] B. Kooi and B. Renne.  Generalized arrow update logic.  In Proc. of 13th TARK, pages 205–211, 2011.
  * [79] L.B. Kuijer.  An arrow-based dynamic logic of norms.  In 3rd International Workshop on Strategic Reasoning (SR 2015), 2015\.
  * [80] L.B. Kuijer.  The expressivity of update logics.  J. Log. Comput., 25(3):719–742, 2015.  doi:10.1093/logcom/exu047.
  * [81] L.B. Kuijer.  Arbitrary arrow update logic with common knowledge is neither RE nor co-RE.  In Proc. of 16th TARK, volume 251 of EPTCS, pages 373–381, 2017.  doi:10.4204/EPTCS.251.27.
  * [82] C. Lutz.  Complexity and succinctness of public announcement logic.  In Proc. of the 5th AAMAS, pages 137–144, 2006.
  * [83] J. McCarthy.  Formalization of two puzzles involving knowledge.  In V. Lifschitz, editor, Formalizing Common Sense : Papers by John McCarthy. Ablex Publishing Corporation, Norwood, N.J., 1990.
  * [84] J.S. Miller and L.S. Moss.  The undecidability of iterated modal relativization.  Studia Logica, 79(3):373–407, 2005.
  * [85] G.E. Moore.  A reply to my critics.  In P.A. Schilpp, editor, The Philosophy of G.E. Moore, pages 535–677. Northwestern University, Evanston, 1942.
  * [86] Y.O. Moses, D. Dolev, and J.Y. Halpern.  Cheating husbands and other stories: a case study in knowledge, action, and communication.  Distributed Computing, 1(3):167–176, 1986.
  * [87] A. Özgün.  Evidence in Epistemic Logic : A Topological Perspective.  PhD thesis, University of Lorraine & University of Amsterdam, 2017.  URL: https://tel.archives-ouvertes.fr/tel-01682932.
  * [88] A. Padmanabha, R. Ramanujam, and Y. Wang.  Bundled fragments of first-order modal logic: (un)decidability.  In S. Ganguly and P.K. Pandya, editors, Proc. of 38th FSTTCS, volume 122 of LIPIcs, pages 43:1–43:20, 2018.  URL: http://www.dagstuhl.de/dagpub/978-3-95977-093-4.
  * [89] R. Parikh.  The logic of games and its applications.  In M. Karpinski and J. van Leeuwen, editors, Topics in the theory of computation, pages 111–139. North-Holland, 1985.
  * [90] M. Pauly.  A modal logic for coalitional power in games.  Journal of Logic and Computation, 12(1):149–166, 2002.
  * [91] M. Pauly and R. Parikh.  Game logic - an overview.  Studia Logica, 75(2):165–182, 2003.  doi:10.1023/A:1027354826364.
  * [92] J.A. Plaza.  Logics of public communications.  In Proc. of the 4th ISMIS, pages 201–216. Oak Ridge National Laboratory, 1989.
  * [93] G.R. Renardel de Lavalette.  Changing modalities.  J. Log. Comput., 14(2):251–275, 2004.  doi:10.1093/logcom/14.2.251.
  * [94] T. Sadzik.  Exploring the iterated update universe.  ILLC, Amsterdam. Technical report PP-2006-18, 2006.
  * [95] J. van Benthem.  Semantic parallels in natural language and computation.  In Logic Colloquium ’87, Amsterdam, 1989. North-Holland.
  * [96] J. van Benthem.  Dynamic odds and ends.  Technical report, University of Amsterdam, 1998.  ILLC Research Report ML-1998-08.
  * [97] J. van Benthem.  Games in dynamic epistemic logic.  Bulletin of Economic Research, 53(4):219–248, 2001.
  * [98] J. van Benthem.  What one may come to know.  Analysis, 64(2):95–105, 2004.
  * [99] J. van Benthem.  An essay on sabotage and obstruction.  In Mechanizing Mathematical Reasoning, LNCS 2605, pages 268–276. Springer, 2005.
  * [100] J. van Benthem.  Logical dynamics meets logical pluralism?  Australasian Journal of Logic, 6:182–209, 2008.
  * [101] J. van Benthem.  Logical Dynamics of Information and Interaction.  Cambridge University Press, 2011.
  * [102] J. van Benthem.  Logic in Games.  MIT Press, 2014.
  * [103] J. van Benthem and D. Ikegami.  Modal fixed-point logic and changing models.  In A. Avron, N. Dershowitz, and A. Rabinovich, editors, Pillars of Computer Science, Essays Dedicated to Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday, LNCS 4800, pages 146–165. Springer, 2008.  doi:10.1007/978-3-540-78127-1\\_9.
  * [104] J. van Benthem and F. Liu.  Dynamic logic of preference upgrade.  Journal of Applied Non-Classical Logics, 17(2):157–182, 2007.
  * [105] J. van Benthem, K. Mierzewski, and F. Zaffora Blando.  The modal logic of stepwise removal.  The Review of Symbolic Logic, page 1–28, 2020.  doi:10.1017/S1755020320000258.
  * [106] J. van Benthem, J. van Eijck, and B. Kooi.  Logics of communication and change.  Information and Computation, 204(11):1620–1662, 2006.
  * [107] W. van der Hoek and M.J. Wooldridge.  Tractable multiagent planning for epistemic goals.  In Proc. of 1st AAMAS, pages 1167–1174. ACM, 2002.
  * [108] H. van Ditmarsch.  Knowledge games.  PhD thesis, University of Groningen, 2000.  ILLC Dissertation Series DS-2000-06.
  * [109] H. van Ditmarsch.  Quantifying notes.  In Proc. of 19th WoLLIC, LNCS 7456, pages 89–109. Springer, 2012\.
  * [110] H. van Ditmarsch and T. French.  Simulation and information.  In J. Broersen and J.-J. Meyer, editors, Knowledge Representation for Agents and Multi-Agent Systems, LNAI 5605, pages 51–65. Springer, 2009.
  * [111] H. van Ditmarsch and T. French.  Quantifying over Boolean announcements.  2020\.  URL: http://arxiv.org/abs/1712.05310.
  * [112] H. van Ditmarsch, T. French, and J. Hales.  Positive announcements.  Studia Logica, 109(3):639–681, 2021.  doi:10.1007/s11225-020-09922-1.
  * [113] H. van Ditmarsch, T. French, and S. Pinchinat.  Future event logic - axioms and complexity.  In L. Beklemishev, V. Goranko, and V. Shehtman, editors, Advances in Modal Logic 8, pages 77–99. College Publications, 2010.
  * [114] H. van Ditmarsch, A. Herzig, and T. de Lima.  Public announcements, public assignments and the complexity of their logic.  Journal of Applied Non-Classical Logics, 22(3):249–273, 2012.  doi:10.1080/11663081.2012.705964.
  * [115] H. van Ditmarsch, S. Knight, and A. Özgün.  Announcement as effort on topological spaces.  Synthese, 196(7):2927–2969, 2019.  doi:10.1007/s11229-017-1592-8.
  * [116] H. van Ditmarsch and B. Kooi.  The secret of my success.  Synthese, 151:201–232, 2006.
  * [117] H. van Ditmarsch and B. Kooi.  Semantic results for ontic and epistemic change.  In Proc. of 7th LOFT, Texts in Logic and Games 3, pages 87–117. Amsterdam University Press, 2008.
  * [118] H. van Ditmarsch, M. Liu, L.B. Kuijer, and I. Sedlár.  Expressivity of some versions of APAL.  In M.A. Martins and I. Sedlár, editors, Proc. of 3rd DaLí, pages 120–136. Springer, 2020.  LNCS 12569.  doi:10.1007/978-3-030-65840-3\\_8.
  * [119] H. van Ditmarsch, W. van der Hoek, and P. Iliev.  Everything is knowable – how to get to know whether a proposition is true.  Theoria, 78(2):93–114, 2012.
  * [120] H. van Ditmarsch, W. van der Hoek, and B. Kooi.  Dynamic Epistemic Logic, volume 337 of Synthese Library.  Springer, 2008.
  * [121] H. van Ditmarsch, W. van der Hoek, B. Kooi, and L.B. Kuijer.  Arbitrary arrow update logic.  Artif. Intell., 242:80–106, 2017.
  * [122] H. van Ditmarsch, W. van der Hoek, B. Kooi, and L.B. Kuijer.  Arrow update synthesis.  Information and Computation, 2020.  doi:10.1016/j.ic.2020.104544.
  * [123] H. van Ditmarsch, W. van der Hoek, and L.B. Kuijer.  Fully arbitrary public announcements.  In A. Máté, L. Beklemishev, and S. Demri, editors, Advances in Modal Logic, volume 11, page 252 tot 267. College Publications, 2016.
  * [124] H. van Ditmarsch, W. van der Hoek, and L.B. Kuijer.  The undecidability of arbitrary arrow update logic.  Theor. Comput. Sci., 693:1–12, 2017.
  * [125] H. van Ditmarsch, W. van der Hoek, and L.B. Kuijer.  The logic of gossiping.  Artificial Intelligence, 286:103306, 2020.  doi:10.1016/j.artint.2020.103306.
  * [126] P. van Emde Boas, J. Groenendijk, and M. Stokhof.  The Conway paradox: Its solution in an epistemic framework.  In Truth, Interpretation and Information, pages 159–182. Foris Publications, Dordrecht, 1984.
  * [127] A. Visser.  Bisimulations, model descriptions and propositional quantifiers, 1996\.  Logic Group Preprint Series 161, Department of Philosophy, Utrecht University.
  * [128] Y. Wang.  Beyond knowing that: A new generation of epistemic logics.  In H. van Ditmarsch and G. Sandu, editors, Jaakko Hintikka on knowledge and game-theoretical semantics, Outstanding contributions to logic 12\. Springer, 2018.
  * [129] Y. Wang and Q. Cao.  On axiomatizations of public announcement logic.  Synthese, 190(1 supp.):103–134, 2013.
  * [130] Y.N. Wáng and T. Ågotnes.  Public announcement logic with distributed knowledge: expressivity, completeness and complexity.  Synthese, 190(Supplement-1):135–162, 2013.  doi:10.1007/s11229-012-0243-3.
  * [131] X. Wen, H. Liu, and F. Huang.  An alternative logic for knowability.  In Proc. of 3rd LORI, LNCS 6953, pages 342–355. Springer, 2011\.
  * [132] H. Xing, Zh. Zhu, and J. Zhang.  Covariant-contravariant refinement modal logic.  FLAP, 6(1):1–30, 2019.