Ågotnes, van Ditmarsch, FrenchUndecidability of Quantified Announcements

T. Ågotnes
H. van Ditmarsch
T. French

The Undecidability of Quantified Announcements

###### Abstract

This paper demonstrates the undecidability of a number of logics with
quantification over public announcements: arbitrary public announcement logic
(APAL), group announcement logic (GAL), and coalition announcement logic
(CAL). In APAL we consider the informative consequences of any announcement,
in GAL we consider the informative consequences of a group of agents (this
group may be a proper subset of the set of all agents) all of which are
simultaneously (and publicly) making known announcements. So this is more
restrictive than APAL. Finally, CAL is as GAL except that we now quantify over
anything the agents not in that group may announce simultaneously as well. The
logic CAL therefore has some features of game logic and of ATL. We show that
when there are multiple agents in the language, the satisfiability problem is
undecidable for APAL, GAL, and CAL. In the single agent case, the
satisfiability problem is decidable for all three logics.

This paper corrects an error to the submitted version of Undecidability of
Quantified Announcements, [33] identified by Yuta Assami [34]. The nature of
the error was in the definition of the formula $c_{ga}(X)$ (see Subsection
5.2) which is corrected in this version.

Keywords: Dynamic Epistemic Logic, Complexity of modal logics

##  1 Introduction

The runs-and-systems approach [15] and, later, dynamic epistemic logics [32]
have been used to specify multi-agent systems dynamic at a high level of
systems architecture. Such modal logical approaches have some advantages, e.g.
that they are typically decidable, the model checking complexity is fairly low
(even linear for the base modal logic), and satisfiability may also be tamed
quite a bit (public announcement logic and the base modal logic are NP-
complete in the single-agent case and PSPACE-complete in the multi-agent case
[21]). Unfortunately, when combining epistemic (or more basic modal) logics
with logical dynamics, it is highly unpredictable if the resulting logic is
decidable even when the base logics are so. A well-known result achieved by
very minimal (linguistic) means is [22]. Other such results, described below,
were reported in [17, 4]. There are several open problems concerning
decidability of dynamic epistemic logics and in this paper we answer some such
questions negatively: the related logics arbitrary public announcement logic,
group announcement logic, and coalition announcement logic are all
undecidable. For the development of proof tools for such logics we consider
this result relevant to report. Given the frequent claim that such logics are
applicable, for example, for epistemic protocol synthesis [10, 11], such
undecidability results are disappointing. We can keep in mind there that model
checking is still decidable and in the final section we discuss some ways
towards decidable versions of these logics.

#### APAL

Public Announcement Logic (PAL) [24] is an extension of epistemic logic with
dynamic modal operators for the effect of so-called truthful public
announcements. The word ‘announcement’ is a bit of a misnomer, nothing really
needs to be said: in fact these announcements are reliable public
observations, supposedly coming from outside of the modelled system and
incorporated by all agents on the assumption of their correctness. Given a
(Kripke) model consisting of epistemic alternatives, the execution of a public
announcement is the restriction of the model to the submodel satisfying the
announcement formula: $\langle\phi\rangle\psi$ means that the announcement
formula $\phi$ is true and that in the restriction of the model to the $\phi$
states, $\psi$ is true (the part $\langle\phi\rangle$ is the dynamic modality,
in its diamond form). It is well-known that this logic is equally expressive
as epistemic logic: by a reduction technique any formula is equivalent to one
without announcements. In Arbitrary Public Announcement Logic (APAL) [6] we
quantify over such announcements, with the restriction that we only quantify
over quantifier-free announcement formulas. The expression
$\langle\bullet\rangle\phi$ means that for all $\langle\bullet\rangle$-free
formulas $\psi$, $\langle\psi\rangle\phi$ is true, in other words: “there is
an announcement $\psi$ such that $\psi$ is true and after which $\phi$ is
true.” Unlike PAL, this logic APAL is more expressive than epistemic logic,
and it is also undecidable [17].

#### GAL

Group Announcement Logic (GAL) [3, 2] is an extension of public announcement
logic that is very similar to APAL. The difference is that we now do not
quantify over all epistemic formulas but over epistemic formulas known by the
individual agents in a given group, that may be a subgroup of the set of all
agents. In order to see the rationale of this, we need to step back a bit to
the conditions of truthful public announcements. The ‘truthful’ in PAL
actually means ‘true’. It is common to model the truthful (true) public
announcement of a formula $\phi$ made by an agent $a$ that is modelled in the
system, as the announcement by an outsider of the formula $K_{a}\phi$, for
“the agent $a$ knows $\phi$.” Now we have ‘truthful’ in its common sense,
because agent $a$ truthfully saying that $\phi$ implies the truth of
$K_{a}\phi$. In group announcement logic we investigate what can be achieved
by simultaneous truthful announcements by a subset of the set of all agents:
$\langle G\rangle\phi$ means that the agents in $G$ can simultaneously say
something they know, after which $\phi$ is true. Here, ‘simultaneously’ merely
means ‘without interference’. We can for example envisage this as the agents
putting their known information in an envelope, after which the envelopes are
opened in public. The validity $\langle G\rangle\langle
G\rangle\phi\rightarrow\langle G\rangle\phi$ of GAL says that we can always
make two subsequent group announcements into a single one. Because of this
property, such group announcements also quantify over finite (public)
communication protocols between the agents in a group and where agents take
turns in saying something: whenever some $a\in G$ is executing a step in the
protocol, we think of all other agents $b$ as performing the trivial
announcement; they say $K_{b}\top$ (‘I know that true is true’). Therefore,
each step in such a protocol can be seen as a $G$-announcement, after which we
apply the property above to make a single $G$-announcement from any finite
sequence of such steps. The logic GAL shares various properties with APAL,
e.g., the axiomatization is similar, and the model checking complexity is
PSPACE-complete [2]. In [4] the logic GAL has shown to be also undecidable.

The expression $\langle G\rangle\phi$ has the smell of ‘group of agents $G$ is
able to achieve $\phi$’, such that, taking a single agent,
$K_{a}\langle\\{a\\}\rangle\phi$ seems to formalize that agent $a$ knows that
she is able to achieve $\phi$, as in logics combining agency and knowledge [1,
29]. The problem is that in different states, different announcements may be
required to make $\phi$ true, so that we can have $\langle
K_{a}\psi\rangle\phi$ in one state and $\langle K_{a}\chi\rangle\phi$ in an
indistinguishable state, for non-equivalent (and non-dependent) $K_{a}\psi$
and $K_{a}\chi$: the agent knows she ‘can make’ $\phi$ true, but still cannot
choose between announcing $\psi$ or announcing $\chi$. These matters are also
reported on in [2].

#### CAL

A variation on GAL is coalition announcement logic (CAL) [3]. In group
announcement logic we investigate the consequences of the simultaneous
announcement (joint public event) by $G$. The agents not in $G$ do not take
part in the action. In CAL, the expression $\langle\\![G]\\!\rangle\phi$ means
that the agents in $G$ can simultaneously announce something they know, after
which $\phi$ is true, no matter what the remaining agents also simultaneously
announced. Clearly, we get into the domain of game logic [23] and ATL [5], see
also the recent survey [28]; and in fact CAL subsumes game logic (for example
the axiom
$\neg\langle\\![\emptyset]\\!\rangle\neg\phi\rightarrow\langle\\![A]\\!\rangle\phi$,
where $A$ is the set of all agents) [3]. Unlike APAL and GAL, the logic CAL
has no known axiomatization. Up to now it was not known that it is also
undecidable. The $\langle\\![G]\\!\rangle\phi$ operator further comes close to
a playability operator as in [26, 28] (in a setting of information changing
games, not for games with factual change).

#### Example

Before we present some other relevant properties of the presented logics, let
us first give an example. Given are two agents Anne and Bill ($a$ and $b$)
such that Anne knows whether $p$ and Bill knows whether $q$, and this is
common knowledge (Figure 1, leftmost square). The names of the states are
suggestive of the valuation of the atoms, e.g. in state $\overline{p}q$ we
have that $p$ is false and $q$ is true. Let us call the model $\mathcal{S}$.
In the figure we depict a number of executions of announcements in the form of
announcing the value of some proposition $\phi$, i.e., an announcement of
$\phi$ whenever it is true, and otherwise the announcement of $\neg\phi$. In
the explanations we already use the semantic notation that will be introduced
in the next section, i.e., $\mathcal{S}_{s}\models\phi$ means that $\phi$ is
true in state (world) $s$ of model $\mathcal{S}$; $\mathcal{S}\models\phi$
means that $\phi$ is valid on model $\mathcal{S}$; and $\mathcal{S}^{\phi}$ is
the restriction (submodel) of $\mathcal{S}$ to the states where $\phi$ is
true.

APAL In APAL, from any state in this model, any model restriction is definable
by an epistemic formula. We have depicted the result of announcing the value
of $p\vee q$, i.e., the announcement is $p\vee q$ in the states $pq$,
$\overline{p}q$, and $p\overline{q}$, whereas the announcement is $\neg(p\vee
q)$ in the state $\overline{p}\overline{q}$. So, for example,
$\mathcal{S}_{\overline{p}q}\models\neg K_{a}q\land\langle\bullet\rangle
K_{a}q$, because $\mathcal{S}_{\overline{p}q}\models\neg K_{a}q$ and
$\mathcal{S}_{\overline{p}q}\models\langle p\vee q\rangle K_{a}q$; where the
latter is true because $\mathcal{S}^{p\vee q}_{\overline{p}q}\models K_{a}q$.

GAL Anne can achieve that Bill knows whether $p$, namely by informing him of
the value of $p$ (Figure 1, middle transition). In other words, there is an
announcement that $a$ can make and that $a$ knows to be true (namely $K_{a}p$
when $p$ is true, and $K_{a}\neg p$ when $p$ is false) such that after that
announcement, $b$ knows whether $p$. We have that
$\mathcal{S}_{pq}\models\langle a\rangle K_{b}p$ because
$\mathcal{S}_{pq}\models\langle K_{a}p\rangle K_{b}p$. The formalization of
“Anne can achieve that Bill knows whether $p$” is $\mathcal{S}\models\langle
a\rangle(K_{b}p\vee K_{b}\neg p)$. Similarly, Bill can achieve that Anne knows
whether $q$, in a formula, $\mathcal{S}\models\langle b\rangle(K_{a}q\vee
K_{a}\neg q)$ (Figure 1, first bottom transition). Neither agent can achieve
both outcomes at the same time, but together they can achieve that by a joint
announcement of what they know: $\langle{ab}\rangle(K_{a}(p\land q)\land
K_{b}(p\land q))$ (Figure 1, bottom rightmost model). In the figure the
announcement is not jointly by Anne and Bill, but still we can get there. This
is because from $\langle b\rangle(K_{a}q\vee K_{a}\neg q)$ we also get
$\langle{ab}\rangle(K_{a}q\vee K_{a}\neg q)$, by having Anne make the trivial
announcement simultaneously to Bill announcing the value of $q$. Similarly,
from $\langle a\rangle(K_{b}p\vee K_{b}\neg p)$ we also get
$\langle{ab}\rangle(K_{b}p\vee K_{b}\neg p)$. Now Bill is making the trivial
announcement. We thus get $\langle{ab}\rangle\langle{ab}\rangle((K_{b}p\vee
K_{b}\neg p)\land(K_{a}q\vee K_{a}\neg q))$, and as such operators satisfy
transitivity (see above) we get the desired $\langle{ab}\rangle((K_{b}p\vee
K_{b}\neg p)\land(K_{a}q\vee K_{a}\neg q))$. Of course, in the case of this
simple example it suffices to observe that Anne can announce the value of $p$
simultaneously with Bill announcing the value of $q$.

CAL One can easily see that Anne can enforce knowledge of the value of $p$ on
Bill, $\langle\\![a]\\!\rangle(K_{b}p\vee K_{b}\neg p)$, namely by announcing
the value of $p$, as before. This is true when Bill makes the trivial
announcement but also when he announces the value of $q$, and there is nothing
else he can do. But Anne cannot enforce her continued ignorance of $q$ so we
have $\mathcal{S}\not\models\langle\\![a]\\!\rangle\neg(K_{a}q\vee K_{a}\neg
q)$. (Unlike that, we have $\mathcal{S}\models\langle a\rangle\neg(K_{a}q\vee
K_{a}\neg q)$.) Together, they can enforce shared knowledge of the atoms:
$\langle\\![{ab}]\\!\rangle(K_{a}(p\land q)\land K_{b}(p\land q))$. This is
obvious, as the entire group of agents is up against nobody, so
$\mathcal{S}\models\langle
ab\rangle\phi\leftrightarrow\langle\\![ab]\\!\rangle\phi$ for all $\phi$.

$\overline{p}\overline{q}$$\overline{p}q$$p\overline{q}$$pq$$b$$a$$a$$b$
$\overline{p}\overline{q}$$\overline{p}q$$p\overline{q}$$pq$$a$$b$ Outsider
$\overline{p}\overline{q}$$\overline{p}q$$p\overline{q}$$pq$$a$$a$ Anne
$\overline{p}\overline{q}$$\overline{p}q$$p\overline{q}$$pq$$b$$b$ Bill
$\overline{p}\overline{q}$$\overline{p}q$$p\overline{q}$$pq$ Anne

Figure 1: Top transition: An announcement of the value of $p\vee q$ that
cannot be made by Anne or Bill. Middle transition: Anne announces the value of
$p$. Bottom transitions: Bill announces the value of $q$, after which Anne
announces the value of $p$.

#### Relative expressivity of APAL, GAL, and CAL

Single-agent APAL is equally expressive as PAL (and as the base epistemic
logic) [6], and this result also carries over to GAL and CAL, so for this
expressivity survey we assume that there is more than one agent.

It will be clear that a group announcement is an announcement, so that
$\langle G\rangle\phi\rightarrow\langle\bullet\rangle\phi$; but that, as in
the above example, there are announcements that not group announcements. This
can be used to demonstrate that APAL is more expressive than GAL. Whether GAL
is also more expressive than APAL is an open question. It is also unknown what
the relative expressivity is of CAL and GAL. Such matters are discussed in [2,
30]. For example, a GAL validity is $\langle G\rangle\langle
H\rangle\phi\rightarrow\langle G\cup H\rangle\phi$ but it is unknown if
$\langle G\cup H\rangle\phi\rightarrow\langle G\rangle\langle H\rangle\phi$ is
valid in CAL: this involves constructing a later announcement by the agents in
$H$ with the same informative effect as their immediate announcement. On
models with infinite domains it is unclear how this should be done (and even
if it can be done at all); note that the agents in $G$ can efface distinctions
between previously bisimilar states that at the time could have been used by
those in $H$, but not any more after $G$’s announcement. Similar issues
complicate proof of the conjecture that GAL and CAL are equally expressive: we
wish to compare the expression $\langle\\![G]\\!\rangle\phi$ to the expression
$\langle G\rangle[A\setminus{G}]\phi$ (where $A$ is the set of all agents):
one would expect that quantifying over anything the remaining agents can say
at the same time as those in $G$ should be the same as quantifying over what
they can say afterwards. But to our knowledge this is yet another open
question. Answering such questions is also relevant for yet other logics with
quantification. For example, consider the single-agent fragment of GAL where
we only have operators $\langle a\rangle$, for any $a\in A$.111This
interesting fragment was suggested by a reviewer, and independently by Jan van
Eijck in oral communication. Clearly, in view of the above,
$\langle\\{a,b\\}\rangle\phi$ need not be equivalent to $\langle
a\rangle\langle b\rangle\phi$.

#### GAL and security

With GAL one can formalize communication protocols, such as security
protocols. Let Alice be a sender $a$, Bob a receiver $b$, and Eve a spy /
eavesdropper $e$. Let $\phi$ be some information goal. For example, suppose
Alice wishes to inform Bob of the latest transatlantic scandal $p$, then an
information goal could be that “Alice, Bob, and Eve commonly know that either
Alice and Bob have common knowledge (between them) of $p$ or Alice and Bob
have common knowledge of $\neg p$.” This can be more succinctly formalized
with common knowledge operators but we bypass these in this paper. The
requirement that not only Alice and Bob but also they and Eve commonly know
this, is usual in a security setting. It formalizes that the protocol is known
to have terminated: we may assume that everything is public about the protocol
except the message (and private keys). There is also a security goal $\psi$
that needs to be preserved throughout protocol execution, e.g. “Alice, Bob,
and Eve commonly know that Eve is ignorant about $p$” (or some more involved
aspect of $p$, such as the identity of those involved in the scandal). A
finite protocol for $a$ and $b$ to learn the secret safely should observe
missing$$$\psi\rightarrow\langle{ab}\rangle(\phi\land\psi)$$Inviewoftheopenexpressivityproblemsmentionedabove,itisnotknowniftheexistenceofafinitetwo-
agentprotocolspecificationasaboveisformalizableinAPAL.\par
SuchformalizationsofsecurityprotocolsinGALmayberelevanttoobtainresultsoncommunicationcomplexity.Itiswell-
knowthatfor$n$agentstosharetheirknowledge,$n$roundsofcommunicationaresufficient\cite[cite]{[\@@bibref{}{jfak.lonely:2006}{}{}]}.Still,therearemanysecurityprotocolsbetweenasenderandareceiverthatrequiremorethantwocommunications(announcements),evenintheaboveveryrestrictedsetting.AnexampleareRussianCardsprotocolsofthreeormoreannouncements,thatareprovednotbepossibleintwoannouncements,asdescribedin\cite[cite]{[\@@bibref{}{cordonetal.tcs:2013}{}{}]}.Theabove$ψ$\rightarrow$$\langle{ab}\rangle$
(ϕ$\land$ψ)$canberealizedbyasingleannouncementby$a$andasingleannouncementby$b$(andevenbyasinglesimultaneousannouncementby$a$and$b$),bytheprocedureofmergingsuccessiveannouncementsintoasingleannouncement.However,eventhoughwemayhave$$\langle{ab}\rangle$
(ϕ$\land$ψ)$,or,inamorerestrictedprotocolsetting,thatthereisaprotocolexecutionby$a$and$b$afterwhich$ϕ$\land$ψ$istrue,thatdoesnotimplythat{\em
agent$a$knowsthat},orthat{\em$b$knowsthat}.Typically,inasecuritysetting,anagentwillonlymakeanannouncementifshe{\em
knows}thattheeavesdropperremainsignorantafterwards.Merelyconsideringthispossibleisnotenough.Thisexplainstheneedforprotocolsconsistingofmorethantwosteps.Assuch,GALorCALformalizationsareratherepistemicprotocolspecifications(withthegroupandcoalitionoperatorsperformingtheroleoftemporalmodalitiesinthebetterknowntemporalepistemicspecifications)thatwethenwishtosynthesizefromsuchdescriptions.Inotherwords,suchGALandCALspecifications(and,similarlyAPALspecifications)canbearoleinthealreadymentionedepistemicplanning\cite[cite]{[\@@bibref{}{bolanderetal:2011}{}{}]}.\par$

#### Results in the paper

APAL was shown to be undecidable in [17]. GAL was shown to be undecidable in
[4]. The satisfiability problem for APAL and GAL is not recursively
enumerable. Also, based on the complete axiomatization of APAL, so that APAL
validity is recursively enumerable, we may conclude that satisfiability for
APAL is co-RE complete, and similarly for GAL. We further show that CAL is
also undecidable. This result is new in this paper. The undecidability proofs
for APAL, GAL, and CAL are all sufficiently different to warrant a integrated
treatment that points out their different proofs in detail, and the
presentation of the undecidability proofs of APAL and GAL in this paper is
therefore substantially different from those in [17, 4]. Whilst the previous
undecidability results used a construction that required five agents, here we
present an improved construction that only requires two agents. As the
satisfiability for the single agent fragment of these logics is trivially
decidable, this gives us a complete picture of decidability for these logics.

#### Overview of the paper

Section 2 introduces the logics APAL, GAL, and CAL. Sections 3 and 4 present
the background on how to prove undecidability from a tiling argument. The core
of the paper is then Section 5 wherein the grid-like structure is defined in
order to enforce a tiling argument, for the three respective logics APAL
(Subsection 5.1), GAL (Subsection 5.2), and CAL (Subsection 5.3). Based on
this groundwork, Section 6 then establishes the undecidability results in a
uniform way for the three respective logics. The final Section 7 discusses
possible generalizations and restrictions, namely to non-public
communications, positive announcements, and group epistemic operators.

##  2 Syntax and semantics

Given is a scenario with a finite group of agents $A$ and a countable set of
atomic (Boolean) propositions $P$. The agents consider different worlds
possible where different sets of propositions may be true, and where different
agents may have different states of knowledge. Our interest is in providing a
formal language for reasoning about what agents know of the propositions, what
agents know about what other agents know, and what agents can find out through
informative events (such as public announcements).

The base language we work with is epistemic logic EL:

$\phi::=\ p\ |\ \lnot\phi\ |\ (\phi\land\phi)\ |\ K_{a}\phi$

where $p\in P$ and $a\in A$. As usual, we take $K_{a}\phi$ to mean agent $a$
knows $\phi$, and let $\widehat{K}_{a}\phi$ abbreviate $\lnot K_{a}\lnot\phi$
(agent $a$ considers $\phi$ to be possible). We consider extensions of this
logic with

  1. 1.

public announcements $[\psi]\phi$;

  2. 2.

arbitrary public announcements $[\bullet]\phi$;

  3. 3.

group announcements $[G]\phi$;

  4. 4.

coalition announcements $[\\!\langle G\rangle\\!]\phi$;

where $G\subseteq A$ and $\psi$ and $\phi$ may be any formula of the
(extended) logic. The dual operators are, respectively,
$\langle\psi\rangle\phi$, $\langle\bullet\rangle\phi$, $\langle G\rangle\phi$
and $\langle\\![G]\\!\rangle\phi$. When talking about a specific group of
agents (say $i$ and $j$) we will typically write $[i,j]$ and $[\\!\langle
i,j\rangle\\!]$ rather than $[\\{i,j\\}]$ and
$[\\!\langle\\{i,j\\}\rangle\\!]$, respectively.

We let PAL refer to EL augmented with public announcements, APAL refer to EL
augmented with arbitrary public announcements, GAL refer to EL augmented with
arbitrary group announcements, and CAL refer to EL augmented with coalition
announcements.

In order to elegantly present the semantics of these logics, later, we further
define the sublanguage ${EL}^{G}$ to be the set of formulas of the type
$\bigwedge_{a\in G}K_{a}\phi_{a}$, where for each $a\in G$, $\phi_{a}\in{EL}$.

Formulas of these logics are interpreted over structures $M=(S,\sim,V)$, where
$S$ is a non-empty set of worlds, $\sim:A\longrightarrow\wp(S\times S)$
assigns a reflexive, transitive and symmetric accessibility relation
$\sim_{a}$ to each agent $a$ (in other words, an equivalence relation), and
$V:P\longrightarrow\wp(S)$ maps each proposition to the set of worlds where it
is true. For each $a\in A$ and each $s\in S$, the set of worlds $\\{t\ |\
s\sim_{a}t\\}$, for which we write $[s]_{a}$, is an equivalence class. A pair
$M_{s}$, where $s$ is a world in the domain of $M$, is called a pointed model.

Let $M=(S,\sim,V)$ and suppose that $s\in S$. The semantics of EL and the
operators above are given recursively for a pointed model $M_{s}$:

$\begin{array}[]{ll}M_{s}\models p&{\rm iff}\ s\in V(p)\\\
M_{s}\models\lnot\phi&{\rm iff}\ M_{s}\not\models\phi\\\
M_{s}\models\phi_{1}\land\phi_{2}&{\rm iff}\ M_{s}\models\phi_{1}\ {\rm and}\
M_{s}\models\phi_{2}\\\ M_{s}\models K_{a}\phi&{\rm iff}\ \forall t\in S\ {\rm
where}\ s\sim_{a}t,\ M_{t}\models\phi\\\ M_{s}\models[\psi]\phi&{\rm iff}\
M_{s}\models\psi\ {\rm implies}\ M^{\psi}_{s}\models\phi\\\
M_{s}\models[\bullet]\phi&{\rm iff}\ \forall\psi\in{EL},\
M_{s}\models[\psi]\phi\\\ M_{s}\models[G]\phi&{\rm iff}\
\forall\psi\in{EL}^{G},\ M_{s}\models[\psi]\phi\\\ M_{s}\models[\\!\langle
G\rangle\\!]\phi&{\rm iff}\ \forall\psi\in{EL}^{G},\
\exists\psi^{\prime}\in{EL}^{A\backslash G},\textrm{ s.t.
}M_{s}\models[\psi\land\psi^{\prime}]\phi\end{array}$

where $M^{\psi}=(S^{\prime},\sim^{\prime},V^{\prime})$ is such that:
$S^{\prime}=\\{s\in S\ |\ M_{s}\models\psi\\}$; for all $a\in A$,
$\sim^{\prime}_{a}\ =\ \sim_{a}\cap(S^{\prime}\times S^{\prime})$; and for all
$p\in P$, $V^{\prime}(p)=V(p)\cap S^{\prime}$.

We say that a formula $\phi$ is satisfiable if there exists some model
$M=(S,\sim,V)$ and some world $s\in S$ such that $M_{s}\models\phi$, and if
$M_{s}\models\phi$ for all model-world pairs $M_{s}$ we say $\phi$ is valid.

The formula $[\psi]\phi$ expresses the property that after the true
announcement of $\psi$, $\phi$ will hold. If $\psi$ is not true (in a given
world) then the world is not consistent with the announcement of $\psi$, so
$[\psi]\phi$ is deemed to be vacuously true in such a world. We note that
$\langle\psi\rangle\phi$ abbreviates $\neg[\psi]\neg\phi$, which has the same
interpretation except that when $\psi$ is not true in a given world, its
interpretation defaults to false. It is known that epistemic logic extended
with public announcements is expressively equivalent to the base epistemic
logic, and as such it is decidable [32].

The formula $[\bullet]\phi$ expresses the statement “after publicly announcing
any true formula of epistemic logic, $\phi$ must be true.” Now, firstly, we
can replace ‘any true formula’ by ‘any formula’: the restriction that the
formula is true in the state of evaluation can be dropped, because if the
formula is false the announcement cannot be made, so that $[\bullet]\phi$ is
then vacuously true. Secondly, this statement implicitly quantifies over all
formulas $\psi$ of epistemic logic, which is an infinite set and,
expressively, a very powerful device. We give an example of this expressive
power below.

######  Example 2.1.

Suppose $\phi$ is the formula $\widehat{K}_{b}p\rightarrow\widehat{K}_{a}p$.
The formula $[\bullet]\phi$ is true at some world $s$ where $p$ is not true,
if and only if for every $b$-related world $u$, for every epistemic formula
$\psi$, if $u$ satisfies $p\land\psi$ then there must be some $a$-related
world, $v_{\psi}$, that also satisfies $p\land\psi$. Otherwise, announcing
$\psi$ would be sufficient to ensure $\widehat{K}_{b}p\land K_{a}\neg p$. Now,
$\psi$ is an arbitrary formula, so it can be arbitrarily complex. For each
such $\psi$, the world $v_{\psi}$ may be different, but the more complex
$\psi$ becomes, the more similar $u$ and $v_{\psi}$ must be, as they
correspond on $\psi$. Thus the formula $[\bullet]\phi$ is enough to say that
every $b$-related world that does satisfies $p$ can be “approximated
arbitrarily well” by an $a$-related world. This scenario is informally
illustrated in Figure 2 and we will make this notion of approximation more
precise in the Section 5. In [17] it was shown that such a property could be
exploited to encode a recursively enumerable tiling problem.

$.......$$a$$a$$a$$b$$u$$s$$v_{\psi_{0}}$$v_{\psi_{1}}$$v_{\psi_{2}}$

Figure 2: An informal representation of the scenario in Example 2.1. The
$\phi$-world is the root of the structure, the link from the root to the
$b$-accessible world is dotted, whereas the links to $a$-accessible worlds are
dashed. As the $\psi_{i}$ become increasingly complex, the structures attached
to $v_{\psi_{i}}$ (from left to right) become an increasingly accurate
approximation of the real structure in $u$.

The formula $[G]\phi$ expresses the property that after a group of agents
(simultaneously) announce any statements that they know to be true, $\phi$
will be true. This statement has an implicit quantifier in it as well, but
this time it is only quantifying over formulas that agents know to be true (in
base epistemic logic), rather than over all formulas that are true. The
example above does not apply, as the worlds $v$ and $u$ would now need to
agree only on formulas that some agent in $G$ knows to be true, rather than
all formulas. As such we can not claim that $u$ can be “approximated
arbitrarily well”, since the set of formulas known by some agent in $G$
creates an upper bound for this “approximation”. However, we are able to
exploit a different type of property with group announcements.

######  Example 2.2.

A group announcement made by a single agent must preserve all worlds that are
indistinguishable by that agent to the current world. Therefore, supposing
that an atom $p$ is not true at the current world, $s$, and consider formula
$[b]\widehat{K}_{a}p$ to be true there. This means that after every possible
announcement that agent $b$ knows to be true, agent $a$ still considers a
world where $p$ is true to be possible. Therefore, there is no simple
epistemic formula that $b$ knows to be true, and that is false at every
$a$-reachable world where $p$ is true. Suppose that we are able to
characterize the set of all worlds that $b$ is unable to distinguish from $s$
up to a given level of complexity, using an epistemic formula, $\psi$. It
follows that $\psi$ will be known to agent $b$, and that after the
announcement of $\psi$, agent $a$ will still consider a world where $p$ is
true to be possible. Therefore, it must be that there is an $a$-reachable
world that agrees with one of the $b$-reachable worlds up to the given level
of complexity. As the level of complexity of $\psi$ is arbitrary, again we are
able to assume that every $b$-reachable world where $p$ is true may be
“approximated arbitrarily well” by some $a$-reachable world. We will formalise
this argument in Section 5.

Finally in the case of coalition announcements there is an alternation in the
announcement made by, and known by, the coalition, and an announcement made
by, and known by, those not in the coalition. This alternation makes the
constructions we require much more difficult. However, we are able to avoid
alternations by only using “coalitions” that are the entire set of agents.
Consequently, the coalition announcement is semantically equivalent to a group
announcement where the group is the full set of agents. We have chosen to
present the proof for the undecidability of CAL separately from the proof of
undecidability of GAL, since the proof for GAL is more elegant and only relies
on single agent groups. However, the underlying mechanism is similar for both
cases.

##  3 Tilings

The undecidability of a logic may be shown by encoding an undecidable tiling
problem into the logic. The tiling problem we will use is as follows:

######  Definition 3.1.

Let $C$ be a finite set of colours and define a $C$-tile to be a four-tuple
over $C$, $\gamma=(\gamma^{u},\gamma^{r},\gamma^{d},\gamma^{\ell})$, where the
elements are referred to as, respectively, up, right, down and left. The
tiling problem is, for any given finite set of $C$-tiles, $\Gamma$, determine
if there is a function
$\lambda:\mathbb{N}\times\mathbb{N}\longrightarrow\Gamma$ such that for all
$(i,j)\in\mathbb{N}\times\mathbb{N}$:

  1. 1.

$\lambda(i,j)^{u}=\lambda(i,j+1)^{d}$

  2. 2.

$\lambda(i,j)^{r}=\lambda(i+1,j)^{\ell}$.

The tiling problem is known to be co-RE complete [9, 20]. In [17, 4] it was
shown, given a set of tiles $\Gamma$, that we could define a formula of APAL
that was satisfiable if and only if $\Gamma$ could tile
$\mathbb{N}\times\mathbb{N}$. In this paper we take a similar, but improved,
approach. The proof presented in [17] was complicated because the grid-like
structure could only be enforced up to $n$ bisimilarity (for an arbitrary
$n$). For GAL and CAL the restriction to arbitrary group announcements makes
it harder to capture the notion of $n$-bisimilarity, which via the
correspondence theory of [25] is equivalent to two worlds agreeing on the
interpretation of all formulas up to a given modal depth. As GAL and CAL do
not quantify over all formulas, but rather only over the formulas that are
known by the group of agents, this approach is more challenging.

##  4 $n$-Bisimulation

A key concept we require in this proof is $n$-bisimilarity:

######  Definition 4.1.

Fix a finite set of atoms, $\Pi$. Given a model, $M=(S,\sim,V)$, an
$n$-$\Pi$-bisimulation over $M$ is a relation $R_{n}\subseteq S\times S$
defined recursively as:

  1. 1.

$sR_{0}t$ if and only if for all $p\in\Pi$, $s\in V(p)$ if and only if $t\in
V(p)$.

  2. 2.

for all $m>0$, $sR_{m}t$ if and only if $sR_{m-1}t$ and:

    1. (a)

for all $i\in A$, for all $u$ where $s\sim_{i}u$, there is some $v$ where
$t\sim_{i}v$ and $uR_{m}v$;

    2. (b)

for all $i\in A$, for all $v$ where $t\sim_{i}v$, there is some $u$ where
$s\sim_{i}u$ and $vR_{m}u$.

Given such a model $M$, and some $s\in S$, we let $\|s\|_{n}^{\Pi}\subseteq S$
be the set of worlds $n$-$\Pi$-bisimilar to $s$. (We omit the $\Pi$ when it is
clear from context).

It is clear that $\|s\|_{n}$ is an equivalence class for all $s\in S$. Another
important property of $n$-bisimilarity is that any two worlds, $s$ and $t$,
that are not $n$-bisimilar must have a witnessing formula
$\phi\in\mathcal{L}_{el}$, such that $M_{s}\models\phi$ and
$M_{t}\not\models\phi$. Thus, if we are able to establish that two worlds in
the model cannot be distinguished by any formula, it follows that these two
worlds are $n$-bisimilar for all $n$. Through this property we are able to
constrain a model to be bisimilar to a grid-like structure, described in the
following section.

######  Lemma 4.2.

Let $\Pi$ be a finite set of propositional atoms. Suppose that $M=(S,\sim,V)$
and $s\in S$. Then for all $n$, there is some $\mathcal{L}_{el}$ formula,
$\phi$, such that for all $t\in S$, $M_{t}\models\phi$ if and only if
$t\in\|s\|_{n}^{\Pi}$.

######  Proof 4.3.

We show this by induction over $n$, where the induction hypothesis is, for any
given $n$:

> $IH(n)$: for all $t\in S$, there is some formula, $\phi^{t}_{n}$, that is
> sufficient to distinguish all states that are not $n$-$\Pi$-bisimilar to
> $t$. That is $M_{t}\models\phi^{t}_{n}$ and if $u\notin\|t\|_{n}$ then
> $M_{u}\not\models\phi^{t}_{n}$.
>
> For the base case, $IH(0)$, it is clear that if $u\notin\|t\|_{0}$, then $t$
> and $u$ must disagree on the interpretation of some atom $p\in\Pi$.
> Therefore we may set $\phi^{t}_{0}=\bigwedge\\{p\in\Pi\ |\ t\in
> V(p)\\}\land\bigwedge\\{\neg p\in\Pi\ |\ t\notin V(p)\\}$. As $\Pi$ is
> finite it is clear that this is a well-defined formula satisfying the base
> of this induction.
>
> Now suppose $IH(m)$ holds, so for all $t\in S$, there is a formula
> $\phi^{t}_{m}$ such that $M_{t}\models\phi^{t}_{m}$ and if
> $u\notin\|t\|_{m}$ then $M_{u}\not\models\phi^{t}_{m}$. Now for $u,t\in S$
> such that $u\notin\|t\|_{m+1}$, we have three possible scenarios:
>
>   1. 1.
>
> $u\notin\|t\|_{m}$, in which case there is some $\mathcal{L}_{el}$ formula
> $\phi^{t}_{m}$ where $M_{t}\models\phi^{t}_{m}$ and
> $M_{u}\not\models\phi^{t}_{m}$.
>
>   2. 2.
>
> there is some $i\in A$, and some $v$ where $t\sim_{i}v$, but for all
> $v^{\prime}$ where $u\sim_{i}v^{\prime}$, $v^{\prime}\notin\|v\|_{m}$.
> Therefore, for every such $v$ there is some formula $\phi^{v}_{m}$ where
> $M_{v}\models\phi^{v}_{m}$ and $M_{v^{\prime}}\not\models\phi^{v}_{m}$. As
> these formulas are taken from a finite set, there is a finite formula
> $\psi^{t}_{m}=\widehat{K}_{i}(\bigvee_{t\sim_{i}v}\phi^{v}_{m})$ such that
> $M_{t}\models\psi^{t}_{m}$ and $M_{u}\not\models\psi^{t}_{m}$.
>
>   3. 3.
>
> there is some $i\in A$ and some $v^{\prime}$ where $u\sim_{i}v^{\prime}$,
> but for all $v$ where $t\sim_{i}v$, $v^{\prime}\notin\|v\|_{m}$. As
> $v^{\prime}\notin\|v\|_{m}$ for all $v$ where $t\sim_{i}v$, it must be the
> case that $M_{v^{\prime}}\not\models\bigvee_{t\sim_{i}v}\phi^{v}_{m}$. We
> let $\xi^{t}_{m}=K_{i}(\bigvee_{t\sim_{i}v}\phi^{v}_{m})$, and it is clear
> that $M_{t}\models\xi^{t}_{m}$.
>
>

>
> We define the $\mathcal{L}_{el}$ formula
> $\phi^{t}_{m+1}=\phi^{t}_{m}\land\psi^{t}_{m}\land\xi^{t}_{m}$. From the
> reasoning above it is clear that $u\in\|t\|_{m+1}$ if and only if
> $M_{u}\models\phi^{t}_{m+1}$.

From the proof of Lemma 4.2 we can see that given a finite set of
propositions, $\Pi$, we only require a finite set of formulas to distinguish
all states, up to $n$-$\Pi$-bisimilarity.

######  Corollary 4.4.

Let $\Pi$ be a finite set of propositional atoms and $n\in\mathbb{N}$. Then
there is a finite set of formulas $\phi_{0},\phi_{1},\ldots,\phi_{n}$ such
that for all $M=(S,R,V)$, for all $u,v\in S$:

  1. 1.

there is some $i\leq n$ such that $M_{u}\models\phi_{i}$; and

  2. 2.

if there is some $i\leq n$ such that $M_{u}\models\phi_{i}$ and
$M_{v}\models\phi_{i}$, then $v\in\|u\|_{n}^{\Pi}$.

######  Proof 4.5.

This follows immediately from the proof of Lemma 4.2.

Finally, we present a well known folk-lemma that $n$-$\Pi$-bisimulations
preserve the interpretation of pure modal formulas over $\Pi$, with modal
depth less than or equal to $n$.

######  Lemma 4.6.

Let $M=(S,R,V)$ and suppose that $s,t\in S$ such that $t\in\|s\|_{n}^{\Pi}$.
Then for all pure modal formulas $\phi$, consisting of only atoms in $\Pi$,
that have modal depth less than or equal to $n$, we have $M_{s}\models\phi$ if
and only if $M_{t}\models\phi$.

######  Proof 4.7.

This is shown by a simple induction over $n$. If $n=0$, then $s$ and $t$ must
agree on the interpretation of all propositional atoms in $\Pi$, and so must
also agree on the interpretation of all propositional formulas. For the
induction, suppose that for all formulas $\phi$ consisting of atoms in $\Pi$,
and having modal depth less than $n$, for all $u,v\in S$ where
$u\in\|v\|_{n-1}$, we have $M_{u}\models\phi$ if and only if
$M_{v}\models\phi$. Let $s,t\in S$ be such that $t\in\|s\|_{n}$, and suppose
that $\phi$ is any formula with modal depth at most $n$. The formula $\phi$
can be broken down into a propositional combination of propositional atoms,
$p_{0},\ldots,p_{a}$ in $\Pi$ and modal formulas $\phi_{0},\ldots,\phi_{b}$.
By definition, $t\in\|s\|_{0}$ so for $x\leq a$, $M_{t}\models p_{a}$ if and
only if $M_{s}\models p_{a}$. Also, for every $x\leq b$ suppose that
$\phi_{x}=K_{i}\psi$, where the modal depth of $\psi$ is less than $n$. If
$M_{t}\models K_{i}\psi$, then for every $t^{\prime}\in tR_{i}$,
$M_{t^{\prime}}\models\psi$. Since $t\in\|s\|_{n}$, for every $s^{\prime}\in
sR_{i}$, there is some $t^{\prime}\in tR_{i}$ such that
$t^{\prime}\in\|s^{\prime}\|_{n-1}$. By the induction hypothesis,
$M_{t^{\prime}}\models\psi$ if and only if $M_{s^{\prime}}\models\psi$, so for
every $s^{\prime}\in sR_{i}$, we have $M_{s^{\prime}}\models\psi$, and
$M_{s}\models K_{i}\psi$. Conversely, if $M_{t}\not\models K_{i}\psi$, then
there is some $t^{\prime}\in tR_{i}$ where $M_{t^{\prime}}\not\models\psi$.
Since $t\in\|s\|_{n}$, for every $t^{\prime}\in tR_{i}$, there is some
$s^{\prime}\in sR_{i}$ such that $t^{\prime}\in\|s^{\prime}\|_{n-1}$. By the
induction hypothesis, and the fact that the modal depth of $\psi$ is less than
$n$, it follows that $M_{s^{\prime}}\not\models\psi$. Therefore,
$M_{s}\not\models K_{i}\psi$, and thus $M_{t}\models\phi_{x}$ if and only if
$M_{s}\models\phi_{x}$. As $s$ and $t$ agree on the interpretations of all the
parts of $\phi$, they must also agree on the interpretation of $\phi$,
completing the inductive case.

##  5 The grid-like structure

In this section we provide the main construction that allows the tiling
problem to be reduced to the satisfiability problem for formulas in APAL, GAL
and CAL. The main steps of this process are:

  1. 1.

enforcing the structure of a satisfying model to have a grid-like structure;

  2. 2.

defining a formula to represent common knowledge;

  3. 3.

using propositional atoms to represent tiles, express the formula “it is
common knowledge that adjacent tiles on the grid have matching sides.”

The model we aim to build represents an infinite grid, or a checkerboard.
Rather than the typically black and white squares of a checkerboard we use the
card suits ${\heartsuit}$, ${\clubsuit}$, ${\diamondsuit}$ and ${\spadesuit}$
to label the squares, in a regular fashion: rows either alternate between
${\spadesuit}$ and ${\diamondsuit}$ squares, or ${\heartsuit}$ and
${\clubsuit}$ squares; and columns either alternate between ${\spadesuit}$ and
${\heartsuit}$ squares, or ${\diamondsuit}$ and ${\clubsuit}$ squares. We will
provide a formula that enforces these constraints on the model, and also
requires that the squares are labelled with tiles as specified by the tiling
problem. The satisfiability of this formula is then equivalent to knowing
whether a set of tiles can tile the plane. The base structure is represented
in Figure 3.

${\heartsuit}$${\heartsuit}$${\spadesuit}$${\clubsuit}$${\heartsuit}$${\clubsuit}$${\clubsuit}$${\spadesuit}$${\heartsuit}$${\clubsuit}$${\heartsuit}$${\clubsuit}$${\diamondsuit}$${\clubsuit}$${\diamondsuit}$${\diamondsuit}$${\spadesuit}$${\heartsuit}$${\spadesuit}$${\heartsuit}$${\diamondsuit}$${\spadesuit}$${\heartsuit}$${\spadesuit}$${\heartsuit}$

Figure 3: The checkerboard configuration.

To represent this structure in an epistemic structure, $M=(S,\sim,V)$, we will
suppose that each square in the grid corresponds to five worlds in $S$,
labelled: up, down, left, right and center (corresponding respectively to the
atoms $u,\ d,\ \ell,\ r$ and the center square will be labelled by exactly one
of the propositions ${\heartsuit},\ {\clubsuit},\ {\diamondsuit}$ or
${\spadesuit}$). We also suppose that there are just two agents: the square
agent, $\mathfrak{s}$; and the edge agent, $\mathfrak{e}$. For any square,
agent $\mathfrak{s}$ cannot distinguish between any of the five worlds that
correspond to that square. For two adjacent squares (say $s$ which is to the
left of $t$) the agent $\mathfrak{e}$ is unable to distinguish between the
right world corresponding to $s$ and the left world corresponding to $t$. The
edge agent is likewise unable to distinguish between the up and down worlds
corresponding the vertically adjacent tiles. Finally we suppose that the edge
agent is unable to distinguish between any of the worlds that are labelled as
center. This representation is given in Figure 4.

$s\sim_{\mathfrak{e}}t$$s$$t$$t$$s$$u$$u$$d$$r$$u$$u$$u$$u$$u$${\heartsuit}$${\clubsuit}$${\diamondsuit}$${\spadesuit}$${\heartsuit}$${\clubsuit}$${\heartsuit}$${\clubsuit}$${\heartsuit}$$\ell$$\ell$$d$$r$$\ell$$d$$r$$d$$\ell$$u$$r$$d$$\ell$$r$$\ell$$d$$r$$\ell$$u$$d$$r$$\ell$$d$$r$$\ell$$d$$r$$s\sim_{\mathfrak{s}}t$

Figure 4: A representation of the checkerboard of Figure 3 as an epistemic
model. The agent $\mathfrak{s}$ is unable to distinguish between any worlds
inside a single square, whilst the agent $\mathfrak{e}$ is unable to
distinguish between any two worlds connected by the reflexive, transitive
closure of the arrow relation.

The model is infinite, so we may suppose that each square corresponds to a
point in $\mathbb{N}\times\mathbb{N}$. To create a tiling, we suppose that we
also have a set of propositions $C$ to label the coloured sides of tiles, and
that this set is disjoint from all the other propositions introduced so far.

Defining a formula that requires a model to have such a structure (steps 1 and
2) is dependent on the separate quantifiers of APAL, GAL and CAL. We will
first address the local properties of the grid and the tiling (step 3).
Suppose we have a model with a grid-like structure. Below we provide a formula
such that the satisfiability of that formula at the center of a square is
equivalent to the existence of a $\Gamma$ tiling of the plane. Let
$\Gamma=\\{\gamma_{1},...\gamma_{n}\\}$ be a set of tiles. We require the
following properties to be true:

  1. 1.

Every world is labelled by exactly one colour:

$oneCol=K_{\mathfrak{s}}K_{\mathfrak{e}}K_{\mathfrak{s}}\bigvee_{c\in
C}\left(c\land\bigwedge_{d\in C\backslash\\{c\\}}\neg d\right)$ (1)

Since every square contains a center world connected to every other center
world by the accessibility relation for $\mathfrak{e}$,
$K_{\mathfrak{s}}K_{\mathfrak{e}}K_{\mathfrak{s}}\phi$ implies that $\phi$
must be true in all worlds. In this case we require that every world is
labelled by exactly one colour, and this is specified via propositional
reasoning.

  2. 2.

Every square corresponds to a tile in the set $\Gamma$.

$tile_{\Gamma}=K_{\mathfrak{s}}K_{\mathfrak{e}}K_{\mathfrak{s}}\left(\bigvee_{\gamma\in\Gamma}\bigwedge\begin{array}[]{c}u\rightarrow\gamma^{u}\\\
r\rightarrow\gamma^{r}\\\ d\rightarrow\gamma^{d}\\\
\ell\rightarrow\gamma^{\ell}\end{array}\right)$ (2)

As above $K_{\mathfrak{e}}\phi$ requires $\phi$ to be true at every center
world (at least). The nested $K_{\mathfrak{s}}$ operator requires that every
square corresponds to some tile in $\Gamma$, by requiring that for some tile
$\gamma$, the $u$-world has the same colour as the top of $\gamma$, the
$r$-world has the same colour as the right side of $\gamma$, the $d$-world has
the same colour as the bottom of $\gamma$ and the $\ell$-world has the same
colour as the left side of $\gamma$.

  3. 3.

The agent $\mathfrak{e}$ always knows the colour.

$match=K_{\mathfrak{s}}K_{\mathfrak{e}}K_{\mathfrak{s}}\bigvee_{c\in
C}(K_{\mathfrak{e}}c)$ (3)

As the $\mathfrak{e}$-agent cannot distinguish the worlds corresponding to
adjoining sides of adjacent squares, requiring that agent $\mathfrak{e}$
always knows the colour means that any worlds corresponding to adjoining sides
of adjacent squares must have the same colour, as required in the tiling
problem. Note that a consequence of this formula is that the central nodes
will all be labelled by the same colour. However, as we are only concerned
with the colour labelling at the edge of the tiles, this does not effect the
encoding.

We combine these properties in the formula:

$SAT_{\Gamma}=oneCol\land tile_{\Gamma}\land match$ (4)

We note that $SAT_{\Gamma}$ does not contain any arbitrary group announcement
operators, and is in fact a formula of $\mathcal{L}_{el}$. It is also clear
that the formula $Tile_{\Gamma}$ is satisfiable by some models that do not
have the grid-like structure. Our next task is to ensure that the worlds in
each square are labelled correctly, and adjacent squares have corresponding
labels. To this end, let
$\Lambda=\\{u,d,\ell,r,{\heartsuit},{\clubsuit},{\diamondsuit},{\spadesuit}\\}$
be the set of labels. We require the following properties:

  1. 1.

Every world satisfies exactly one label $\lambda\in\Lambda$.

$oneLabel=K_{\mathfrak{s}}K_{\mathfrak{e}}K_{\mathfrak{s}}\left(\bigvee_{\lambda\in\Lambda}\left(\lambda\land\bigwedge_{\mu\in\Lambda\backslash\\{\lambda\\}}\neg\mu\right)\right)$
(5)

The reasoning here is analogous to the formula (1) above.

  2. 2.

Every equivalence class of agent $\mathfrak{s}$ contains worlds labelled by
all of $u,\ d,\ \ell$ and $r$, and exactly one of ${\heartsuit}$,
${\clubsuit}$, ${\diamondsuit}$and ${\spadesuit}$.

We define the abbreviation:

$sq(X)=K_{\mathfrak{s}}(u\lor d\lor\ell\lor r\lor
X)\land\widehat{K}_{\mathfrak{s}}u\land\widehat{K}_{\mathfrak{s}}d\land\widehat{K}_{\mathfrak{s}}\ell\land\widehat{K}_{\mathfrak{s}}r\land\widehat{K}_{\mathfrak{s}}X$
(6)

Then we require that every “square” satisfies one of this formula for a given
card suit:

$oneSuit=K_{\mathfrak{s}}K_{\mathfrak{e}}\left[sq({\heartsuit})\lor
sq({\clubsuit})\lor sq({\diamondsuit})\lor sq({\spadesuit})\right]$ (7)

Combined with the unique labelling specified by (5), this ensures the agent
$\mathfrak{s}$ always considers an up-world, a down-world, a left world, a
right world and a center world possible. Furthermore any center worlds that
the agent considers possible must be labelled by a single suit
(${\heartsuit}$, ${\clubsuit}$, ${\diamondsuit}$ or ${\spadesuit}$).

  3. 3.

Agent $\mathfrak{e}$ always knows that the world is either: $\ell$ or $r$; $u$
or $d$; or ${\heartsuit}$, ${\clubsuit}$, ${\diamondsuit}$ or ${\spadesuit}$.
However, the agent is not able to further distinguish these worlds.

This may be specified as follows:

$edge=K_{\mathfrak{s}}K_{\mathfrak{e}}K_{\mathfrak{s}}\bigvee\\!\left[\begin{array}[]{l}K_{\mathfrak{e}}(\ell\lor
r)\land\widehat{K}_{\mathfrak{e}}r\rightarrow K_{\mathfrak{e}}(\ell\rightarrow
K_{\mathfrak{s}}(u\rightarrow
K_{\mathfrak{e}}K_{\mathfrak{s}}\widehat{K}_{\mathfrak{e}}r))\\\
K_{\mathfrak{e}}(u\lor d)\land\widehat{K}_{\mathfrak{e}}u\rightarrow
K_{\mathfrak{e}}(d\rightarrow K_{\mathfrak{s}}(r\rightarrow
K_{\mathfrak{e}}K_{\mathfrak{s}}\widehat{K}_{\mathfrak{e}}u))\\\
K_{\mathfrak{e}}({\heartsuit}\lor{\clubsuit}\lor{\diamondsuit}\lor{\spadesuit})\land\widehat{K}_{\mathfrak{e}}{\heartsuit}\land\widehat{K}_{\mathfrak{e}}{\clubsuit}\land\widehat{K}_{\mathfrak{e}}{\diamondsuit}\land\widehat{K}_{\mathfrak{e}}{\spadesuit}\end{array}\right]$
(8)

For this equation, we assume that
$K_{\mathfrak{s}}K_{\mathfrak{e}}K_{\mathfrak{s}}\phi$ implies that $\phi$ is
true at all reachable states. At all such states we can see there are three
possibilities for what the agent $\mathfrak{e}$ knows: either $\ell$ or $r$ is
true, but $\mathfrak{e}$ does not know which (unless it is in the leftmost
column of the checkerboard); either $u$ or $d$ is true, but $\mathfrak{e}$
does not know which (unless it is in the bottom row of the checkerboard); or
one of ${\heartsuit}$, ${\clubsuit}$, ${\diamondsuit}$ or ${\spadesuit}$ is
true, but $\mathfrak{e}$ does not know which. If $\widehat{K}_{\mathfrak{e}}r$
is true, then we are in a square that is not in the left column of the board,
so the formula $K_{\mathfrak{e}}(\ell\rightarrow K_{\mathfrak{s}}(u\rightarrow
K_{\mathfrak{e}}K_{\mathfrak{s}}\widehat{K}_{\mathfrak{e}}r))$ ensures that
the square above also has a left neighbour. This is sufficient to restrict all
squares without a left neighbour to the left column of the board, and a
similar case can be made for the bottom row.

  4. 4.

A ${\heartsuit}$-square always has a ${\clubsuit}$-square to the right and a
${\spadesuit}$-square above; a ${\clubsuit}$-square always has a
${\heartsuit}$-square to the right and a ${\diamondsuit}$-square above; a
${\diamondsuit}$-square always has a ${\spadesuit}$-square to the right and a
${\clubsuit}$-square above; and a ${\spadesuit}$-square always has a
${\diamondsuit}$-square to the right and a ${\heartsuit}$-square above.

We can specify these constraints as:

$\displaystyle adj_{\heartsuit}$ $\displaystyle=$ $\displaystyle
K_{\mathfrak{s}}K_{\mathfrak{e}}\left({\heartsuit}\rightarrow
K_{\mathfrak{s}}\bigwedge\left[\begin{array}[]{l}r\rightarrow
K_{\mathfrak{e}}(\ell\rightarrow\widehat{K}_{\mathfrak{s}}{\clubsuit})\\\
u\rightarrow
K_{\mathfrak{e}}(d\rightarrow\widehat{K}_{\mathfrak{s}}{\spadesuit})\end{array}\right]\right)$
(11) $\displaystyle adj_{\clubsuit}$ $\displaystyle=$ $\displaystyle
K_{\mathfrak{s}}K_{\mathfrak{e}}\left({\clubsuit}\rightarrow
K_{\mathfrak{s}}\bigwedge\left[\begin{array}[]{l}r\rightarrow
K_{\mathfrak{e}}(\ell\rightarrow\widehat{K}_{\mathfrak{s}}{\heartsuit})\\\
u\rightarrow
K_{\mathfrak{e}}(d\rightarrow\widehat{K}_{\mathfrak{s}}{\diamondsuit})\end{array}\right]\right)$
(14) $\displaystyle adj_{\diamondsuit}$ $\displaystyle=$ $\displaystyle
K_{\mathfrak{s}}K_{\mathfrak{e}}\left({\diamondsuit}\rightarrow
K_{\mathfrak{s}}\bigwedge\left[\begin{array}[]{l}r\rightarrow
K_{\mathfrak{e}}(\ell\rightarrow\widehat{K}_{\mathfrak{s}}{\spadesuit})\\\
u\rightarrow
K_{\mathfrak{e}}(d\rightarrow\widehat{K}_{\mathfrak{s}}{\clubsuit})\end{array}\right]\right)$
(17) $\displaystyle adj_{\spadesuit}$ $\displaystyle=$ $\displaystyle
K_{\mathfrak{s}}K_{\mathfrak{e}}\left({\spadesuit}\rightarrow
K_{\mathfrak{s}}\bigwedge\left[\begin{array}[]{l}r\rightarrow
K_{\mathfrak{e}}(\ell\rightarrow\widehat{K}_{\mathfrak{s}}{\diamondsuit})\\\
u\rightarrow
K_{\mathfrak{e}}(d\rightarrow\widehat{K}_{\mathfrak{s}}{\heartsuit})\end{array}\right]\right)$
(20) $\displaystyle adj$ $\displaystyle=$ $\displaystyle adj_{\heartsuit}\land
adj_{\clubsuit}\land adj_{\diamondsuit}\land adj_{\spadesuit}$ (21)

Given the properties of the checkerboard model, the formula
$K_{\mathfrak{s}}K_{\mathfrak{e}}\phi$ will ensure that $\phi$ is true at
every center world. If the proposition ${\heartsuit}$ is true there, then at
every $r$-world in the square, every $\ell$-world that agent $\mathfrak{e}$
cannot distinguish from the $r$-world must belong to the square that is
immediately to the right. Therefore the center of that square must be labelled
by ${\clubsuit}$. Given the formula (7), it is sufficient for
$\widehat{K}_{\mathfrak{s}}{\clubsuit}$ to be true at the $\ell$-world.
Similar reasoning can be given for the other suits and directions.

We define the formula:

$local=oneLabel\land oneSuit\land edge\land adj$ (22)

to express the local properties. This leaves us to define the global
properties The two global properties we require are:

  * •

Given any square, the square below the square to the left of the square above
the square to its right is identical.

This is an essential feature of the grid-like construction we require, and
enforces that if we go right, up, left, and down, we end up where we began.

  * •

Every center world of every reachable square is indistinguishable to agent
$\mathfrak{e}$.

By reachable square, we mean any $\mathfrak{s}$-equivalence class that can be
reached using the union of the $\mathfrak{e}$ and $\mathfrak{s}$ accessibility
relations.

While these are the properties we would ideally like, it turns out that they
are stronger than what we are able to express. Using Lemma 4.2, the actual
properties we will show are:

  * •

For all $n$, for every center world, $w$, of any square, there is some square
below some square to the left of some square above some square to the right of
that square, whose center world is $n$-bisimilar to $w$.

Since this property holds for all $n$ we are able to make an arbitrarily good
approximation of the checkerboard configuration.

  * •

For all $n$, for every center world, $w$, of every
{$\mathfrak{e}$,$\mathfrak{s}$}-reachable square there is some
$\mathfrak{e}$-accessible world that is $n$-bisimilar to $w$.

Therefore, although we may not be able to strictly enforce the global property
we desire, we are able to make an arbitrarily good approximation of it.

The first property corresponds to the first step of our proof: enforcing a
grid like configuration. The second property encodes a common knowledge
operator required in step 2. To enforce these properties we will require the
arbitrary, group or coalition announcements, and the formulation will vary
slightly depending on the language. We will therefore address these properties
in the context of each variation in the following three subsections.

To give a generalized form of the correctness proof we use a PDL-like notation
[16] to describe composite relations:

######  Definition 5.1.

A composite program is given by the abstract syntax:

$\pi::=a\ |\ A?\ |\ \pi;\pi$

where $A$ ranges over
$\\{{\heartsuit},{\clubsuit},{\diamondsuit},{\spadesuit},u,d,\ell,r\\}$ and
$a$ ranges over $\\{\mathfrak{e},\mathfrak{s}\\}$. Each composite program
$\pi$ corresponds to a binary relation $R(\pi)$ on $S$ where:

$\begin{array}[]{rcl}R(A?)&=&\\{(s,s)\ |\ S\in V(A)\\}\\\ R(a)&=&\sim_{a}\\\
R(\pi;\pi^{\prime})&=&\\{(s,t)\ |\ \exists u\ \text{s.t.}\ (s,u)\in
R(\pi),(u,t)\in R(\pi^{\prime})\\}\end{array}$

This allows us to discuss a chain of reachable states satisfying a sequence of
propositional atoms. For example, if we have a world $t$ where $t\in V(u)$
where $t\sim_{\mathfrak{s}}u$ and $u\in V(\ell)$ and $u\sim_{\mathfrak{e}}s$
we can construct a program $\pi=\mathfrak{e};\ell?;\mathfrak{s};u?$, and write
$(s,t)\in R(\pi)$. We may also use $sR(\pi)$ to denote the set of all such
$t$. However, we refrain from writing $s\sim_{\pi}t$ to avoid confusion as
$\sim_{\pi}$ would not be an equivalence relation.

As a simplification, we will work with only a finite number of distinct
propositions in our model: the labels in $\Lambda$, and the colours in $C$. We
let $\Pi=C\cup\Lambda$ and when we refer to bisimilarity, we will mean
bisimilarity modulo the atoms in $\Pi$.

###  5.1 Arbitrary public announcements

The properties are formalized as follows:

  * •

For all $n$, for every center world, $w$, of any square, there is some square
below some square to the left of some square above some square to the right of
that square, whose center world is $n$-bisimilar to $w$.

$\displaystyle c_{apa}(X)$ $\displaystyle=$ $\displaystyle
X\rightarrow[\bullet](K_{\mathfrak{s}}(r\rightarrow(K_{\mathfrak{e}}(\ell\rightarrow
K_{\mathfrak{s}}(u\rightarrow K_{\mathfrak{e}}(d\rightarrow$
$\displaystyle\qquad K_{\mathfrak{s}}(\ell\rightarrow
K_{\mathfrak{e}}(r\rightarrow K_{\mathfrak{s}}(d\rightarrow
K_{\mathfrak{e}}(u\rightarrow\widehat{K}_{\mathfrak{s}}X))))))))))$
$\displaystyle cyc_{apa}$ $\displaystyle=$ $\displaystyle
c_{apa}({\heartsuit})\land c_{apa}({\clubsuit})\land
c_{apa}({\diamondsuit})\land c_{apa}({\spadesuit})$

  * •

For all $n$, for every center world, $w$, of every reachable square there is
some $\mathfrak{e}$-accessible world that is $n$-bisimilar to $w$.

$\begin{array}[]{l}t_{apa}(X,Y,Z)=X\rightarrow\bigwedge\left[\begin{array}[]{l}[\bullet](K_{\mathfrak{e}}\neg
Y\rightarrow K_{\mathfrak{s}}(r\rightarrow K_{\mathfrak{e}}(\ell\rightarrow
K_{\mathfrak{s}}\neg Y)))\\\ [\bullet](K_{\mathfrak{e}}\neg Z\rightarrow
K_{\mathfrak{s}}(u\rightarrow K_{\mathfrak{e}}(d\rightarrow
K_{\mathfrak{s}}\neg Z)))\\\ [\bullet](K_{\mathfrak{e}}\neg Y\rightarrow
K_{\mathfrak{s}}(\ell\rightarrow K_{\mathfrak{e}}(r\rightarrow
K_{\mathfrak{s}}\neg Y)))\\\ [\bullet](K_{\mathfrak{e}}\neg Z\rightarrow
K_{\mathfrak{s}}(d\rightarrow K_{\mathfrak{e}}(u\rightarrow
K_{\mathfrak{s}}\neg Z)))\end{array}\right]\\\
ck_{apa}=t_{apa}({\heartsuit},{\clubsuit},{\spadesuit})\land
t_{apa}({\clubsuit},{\heartsuit},{\diamondsuit})\land
t_{apa}({\diamondsuit},{\spadesuit},{\clubsuit})\land
t_{apa}({\spadesuit},{\diamondsuit},{\heartsuit})\end{array}$

The formula $cyc_{apa}$ enforces the cycle in a grid: right, up, left and
down. The formula $ck_{apa}$ captures the required approximation of common
knowledge.

We define the formula:

$CB_{apa}=K_{\mathfrak{e}}K_{\mathfrak{s}}(local\land cyc_{apa}\land
ck_{apa})$ (23)

The following lemma provides the main technical result that allows us to
define the checkerboard-like model, and hence express the tiling problem. For
brevity, let
$card={\heartsuit}\lor{\clubsuit}\lor{\diamondsuit}\lor{\spadesuit}$.

######  Lemma 5.2.

Suppose that $M=(S,\sim,V)$, $s\in S$ and $M_{s}\models CB_{apa}\land card$.
Let $U=sR(\mathfrak{s};r?;\mathfrak{e};\ell?;\mathfrak{s})\cup
sR(\mathfrak{s};u?;\mathfrak{e};d?;\mathfrak{s})\cup
sR(\mathfrak{s};\ell?;\mathfrak{e};r?;\mathfrak{s})\cup
sR(\mathfrak{s};d?;\mathfrak{e};u?;\mathfrak{s})$. Then:

  1. 1.

For all $n\in\mathbb{N}$, for all $t\in U$, if $M_{t}\models card$, then there
is some $v\sim_{\mathfrak{e}}s$ such that $v\in\|t\|_{n}$.

  2. 2.

For all $n\in\mathbb{N}$, for all $t\in
sR(\mathfrak{s};r?;\mathfrak{e};\ell?;\mathfrak{s};u?;\mathfrak{e};d?;\mathfrak{s};\ell?;\mathfrak{e};r?;\mathfrak{s};d?;\mathfrak{e};u?)$,
there is some $v\sim_{\mathfrak{s}}t$ such that $v\in\|s\|_{n}$.

######  Proof 5.3.

  1. 1.

We will address this case of $t\in
sR(\mathfrak{s};r?;\mathfrak{e};\ell?;\mathfrak{s})$, and note that the other
cases ($t\in sR(\mathfrak{s};u?;\mathfrak{e};d?;\mathfrak{s})$, $t\in
sR(\mathfrak{s};\ell?;\mathfrak{e};r?;\mathfrak{s})$ and $t\in
sR(\mathfrak{s};d?;\mathfrak{e};u?;\mathfrak{s})$) may be handled in a similar
fashion. Suppose, for contradiction, that there is some $n\in\mathbb{N}$ and
some $t\in sR(\mathfrak{s};r?\mathfrak{e};\ell?;\mathfrak{s})$ such that
$M_{t}\models card$ and for all $v\sim_{\mathfrak{e}}s$, $v\notin\|t\|_{n}$.
Then by Lemma 4.2, there is some epistemic formula $\phi_{t}^{n}$ such that
for all $w\in S$, $M_{w}\models\phi_{t}^{n}$ if and only if $w\in\|t\|_{n}$.
We recall that
$card={\heartsuit}\lor{\clubsuit}\lor{\diamondsuit}\lor{\spadesuit}$. Now
suppose, without loss of generality, $s\in V({\heartsuit})$. From the formula
$edge$ we know that all $v\sim_{\mathfrak{e}}s$ must be such that
$M_{v}\models card$, and also that for every $w\in
sR(\mathfrak{s};\mathfrak{e};\mathfrak{s})$, $M_{w}\models\ell\lor
r\rightarrow\neg card$. Therefore, there is some announcement
$\psi={\clubsuit}\rightarrow\phi_{t}^{n}$. We can observe:

    1. (a)

$M_{s}\models\psi$. Since $M_{s}\models{\heartsuit}$ and $M_{s}\models
oneLabel$, we have $M_{s}\models\neg{\clubsuit}$ so $M_{s}\models\psi$ since
the antecedent is false.

    2. (b)

For all $v\in sR(\mathfrak{e};{\clubsuit}?)$ we have $M_{v}\not\models\psi$.
As $M_{v}\models{\clubsuit}$ it must satisfy the consequent of $\psi$.
However, our assumption is that for all $v\sim_{\mathfrak{e}}s$,
$v\notin\|t\|_{n}$, so $M_{v}\not\models\phi_{t}^{n}$.

    3. (c)

For all $v\in sR(\mathfrak{s};r?)$ we have $M_{v}\models\psi$. Since $v\in
sR(\mathfrak{s};r?)$, we must have $M_{v}\models r$ and from the formula
$edge$ we know that $M_{v}\not\models card$, so $M_{v}\models\psi$ since the
antecedent of $\psi$ is false.

    4. (d)

For all $v\in sR(\mathfrak{s};r?;\mathfrak{e};\ell?)$ we have
$M_{v}\models\psi$. As above, since $M_{v}\models\ell\land edge$ we know that
$M_{v}\not\models card$, so $M_{v}\models\psi$ since the antecedent of $\psi$
is false.

    5. (e)

For some $v\in sR(\mathfrak{s};r?;\mathfrak{e};\ell?;\mathfrak{s})$ we have
$M_{v}\models\psi\land{\clubsuit}$, since $t\in
sR(\mathfrak{s};r?;\mathfrak{e};\ell?;\mathfrak{s})$, and clearly
$M_{t}\models{\clubsuit}\land\phi_{t}^{n}$.

Since $M_{s}\models ck_{apa}$ we have

$M_{s}\models{\heartsuit}\rightarrow[\bullet](K_{\mathfrak{e}}\neg{\clubsuit}\rightarrow
K_{\mathfrak{s}}(r\rightarrow K_{\mathfrak{e}}(\ell\rightarrow
K_{\mathfrak{s}}\neg{\clubsuit})))$

Substituting $\psi$ as the public announcement we have:

$M_{s}\models[\psi](K_{\mathfrak{e}}\neg{\clubsuit}\rightarrow
K_{\mathfrak{s}}(r\rightarrow K_{\mathfrak{e}}(\ell\rightarrow
K_{\mathfrak{s}}\neg{\clubsuit})))$

However, from the reasoning above, in the model
$M^{\psi}=(S^{\psi},R^{\psi},V^{\psi})$ we have

    1. (a)

$s\in S^{\psi}$, so the announcement $\psi$ is not vacuous.

    2. (b)

for all $v\in sR(\mathfrak{e};{\clubsuit}?)$, $v\notin S^{\psi}$ so
$M^{\psi}_{s}\models K_{\mathfrak{e}}\neg{\clubsuit}$.

    3. (c)

for all $v\in sR(\mathfrak{s};r?)$, $v\in S^{\psi}$.

    4. (d)

for all $v\in sR(\mathfrak{s};r?;\mathfrak{e};\ell?)$, $v\in S^{\psi}$.

    5. (e)

there is some $t\in
sR(\mathfrak{s};r?;\mathfrak{e};\ell?;\mathfrak{s};{\clubsuit}?)$ where $t\in
S^{\psi}$.

Therefore $M^{\psi}\models
K_{\mathfrak{e}}\neg{\clubsuit}\land\widehat{K}_{\mathfrak{s}}(r\land\widehat{K}_{\mathfrak{e}}(\ell\land\widehat{K}_{\mathfrak{s}}{\clubsuit}))$
giving us the required contradiction. Hence for all $n\in\mathbb{N}$, for all
$t\in sR(\mathfrak{s};r?;\mathfrak{e};\ell?;\mathfrak{s})$ where
$M_{t}\models{\clubsuit}$, there is some $v\sim_{\mathfrak{e}}s$ such that
$v\in\|t\|_{n}$. We may easily generalize the proof to the other cases where
$M_{s}\models{\clubsuit}\lor{\diamondsuit}\lor{\spadesuit}$.

The proofs for the cases: $t\in
sR(\mathfrak{s};u?;\mathfrak{e};d?;\mathfrak{s})$; $t\in
sR(\mathfrak{s};\ell?;\mathfrak{e};r?;\mathfrak{s})$; and $t\in
sR(\mathfrak{s};d?;\mathfrak{e};u?;\mathfrak{s})$) are similar to that of
$t\in sR(\mathfrak{s};r?;\mathfrak{e};\ell?;\mathfrak{s})$. The only changes
are

    1. (a)

in the second case, to replace: all references to $r$ with $u$; all references
to $\ell$ with $d$; and the reference to ${\clubsuit}$ in the definition of
$\psi$ with ${\spadesuit}$.

    2. (b)

in the third case, to replace: all references to $r$ with $\ell$; and all
references to $\ell$ with $r$.

    3. (c)

in the fourth case, to replace: all references to $r$ with $d$; all references
to $\ell$ with $u$; and the reference to ${\clubsuit}$ in the definition of
$\psi$ with ${\spadesuit}$.

  2. 2.

For the final part of this proof we are required to show that for all $n$, for
all $t\in
sR(\mathfrak{s};r?;\mathfrak{e};\ell?;\mathfrak{s};u?;\mathfrak{e};d?;\mathfrak{s};\ell?;\mathfrak{e};r?;\mathfrak{s};d?;\mathfrak{e};u?)$,
there is some $v\sim_{\mathfrak{s}}t$ such that $v\in\|n\|_{s}$. We begin by
considering any chain of worlds

$s\sim_{\mathfrak{s}}t_{1}\sim_{\mathfrak{e}}t_{2}\sim_{\mathfrak{s}}t_{3}\sim_{\mathfrak{e}}t_{4}\sim_{\mathfrak{s}}t_{5}\sim_{\mathfrak{e}}t_{6}\sim_{\mathfrak{s}}t_{7}\sim_{\mathfrak{e}}t$

where $t_{1},t_{6}\in V(r)$, $t_{2},t_{5}\in V(\ell)$, $t_{3},t\in V(u)$, and
$t_{4},t_{7}\in V(d)$.

We first show that from the first four parts of this lemma, each world in this
chain satisfies the formula $local$ (22). Because $M_{s}\models CB_{apa}$, it
follows that $M_{s}\models K_{\mathfrak{e}}K_{\mathfrak{s}}local$. Therefore
$t_{1}$ must satisfy $local$. Furthermore, from the first part of this lemma,
we know for all $n\in\mathbb{N}$, for all $t_{2}\in
sR(\mathfrak{s};r?;\mathfrak{e};\ell?)$, for all
$w_{1}\sim_{\mathfrak{s}}t_{2}$ where $M_{t}\models card$, there is some
$v_{1}\sim_{\mathfrak{e}}s$ such that $w_{1}\in\|v_{1}\|_{n}$. Since the modal
depth of $local$ is $5$, we may suppose, without loss of generality, that
$w_{1}\in\|v_{1}\|_{14}^{\Pi}$. Since $v_{1}\sim_{\mathfrak{e}}s$, we have
$M_{v_{1}}\models CB_{apa}$ and also $M_{v_{1}}\models
K_{\mathfrak{e}}K_{\mathfrak{s}}local$. By Lemma 4.6, $n$-$\Pi$-bisimilarity
preserves the interpretation of pure modal formulas with modal depth up to
$n$, we have $M_{w_{1}}\models K_{\mathfrak{s}}local$. Since
$w_{1}\sim_{\mathfrak{s}}t_{2}$ and $t_{2}\sim_{\mathfrak{s}}t_{3}$ it follows
that $M_{t_{2}}\models local$ and $M_{t_{3}}\models local$. Since
$M_{v_{1}}\models CB_{apa}\land card$, from the first part of this lemma,
given the second component of $U$, for all $n\in\mathbb{N}$, for all
$v^{\prime}\in v_{1}R(\mathfrak{s};u?;\mathfrak{e};d?)$, for all
$v^{\prime\prime}\sim_{\mathfrak{s}}v^{\prime}$ where
$M_{v^{\prime\prime}}\models card$, there is some
$v_{2}\sim_{\mathfrak{e}}v_{1}$ such that $v^{\prime\prime}\in\|v_{2}\|_{n}$.
As $w_{1}\in\|v_{1}\|_{14}^{\Pi}$, for all $w_{2}\in
w_{1}R(\mathfrak{s};u?;\mathfrak{e};d?;\mathfrak{s})$, such that
$M_{w_{2}}\models card$, there is some $v^{\prime\prime}\in
v_{1}R(\mathfrak{s};u?;\mathfrak{e};d?;\mathfrak{s})$ where
$M_{v^{\prime\prime}}\models card$ and $w_{2}\in\|v^{\prime\prime}\|_{11}$.
Putting the last two statements together, for all such $w_{2}$, there is some
$v_{2}\sim_{\mathfrak{e}}v_{1}$ such that $w_{2}\in\|v_{2}\|_{11}$. As
$v_{2}\sim_{\mathfrak{e}}v_{1}$, and $v_{1}\sim_{\mathfrak{e}}s$, we have
$v_{2}\sim_{\mathfrak{e}}s$, and hence $M_{v_{2}}\models
K_{\mathfrak{e}}K_{\mathfrak{s}}local$. As $w_{1}\sim_{\mathfrak{s}}t_{3}$,
there is some such $w_{2}$ where $t_{4}\sim_{\mathfrak{s}}w_{2}$ and
$t_{5}\sim_{\mathfrak{s}}w_{2}$. From Lemma 4.6 we have $M_{t_{4}}\models
local$ and $M_{t_{5}}\models local$.

Continuing in this way, (using the first part of the lemma, with the third
component of $U$) we are able to find some $w_{3}$ such that
$t_{6}\sim_{\mathfrak{s}}w_{3}$, $t_{7}\sim_{\mathfrak{s}}w_{3}$ and for some
$v_{3}\sim_{\mathfrak{e}}s$, $w_{3}\in\|v_{3}\|_{8}$. Finally, applying the
first part of this lemma with the fourth component of $U$, we are able to find
$w_{4}$ such that $t\sim_{\mathfrak{s}}w_{4}$, and for some
$v_{4}\sim_{\mathfrak{e}}s$, $w_{4}\in\|v_{4}\|_{5}$. Since the modal depth of
$local$ is $5$, it follows that $t_{1},\ t_{2},\ t_{3},\ t_{4},\ t_{5},\
t_{6},\ t_{7}$ and $t$ all satisfy $local$, so every world has just one label,
and every square contains a world labelled by each direction, and so on.

Again, let us suppose that $M_{s}\models{\heartsuit}$, and the proof may be
easily adjusted for the other card suits. The construction we have applied is
depicted in Figure 5.

$\sim_{n}$${\heartsuit}$$r$$t_{1}$$\ell$$t_{2}$$w_{1}$${\clubsuit}$$u$$d$${\diamondsuit}$$\ell$$r$${\spadesuit}$$d$$w_{3}$$t_{7}$$t$$u$${\heartsuit}$$v$$t_{6}$$t_{5}$$w_{2}$$t_{4}$$t_{3}$$s$

Figure 5: A representation of the final case of Lemma 5.2. The dashed boxes
represent the $\mathfrak{s}$ equivalence classes; the solid lines are the
$\mathfrak{e}$ equivalence classes; and the dashed line indicates
$n$-$\Pi$-bisimilarity.

We are required to show for every such $t$, for any given $n$, there is some
$v\sim_{\mathfrak{s}}t$ such that $v\in\|s\|_{n}$. Suppose that this was not
the case. Then for some $n\in\mathbb{N}$, for some

$t\in
sR(\mathfrak{s};r?;\mathfrak{e};\ell?;\mathfrak{s};u?;\mathfrak{e};d?;\mathfrak{s};\ell?;\mathfrak{e};r?;\mathfrak{s};d?;\mathfrak{e};u?),$

we have for all $v\sim_{\mathfrak{s}}t$, $v\notin\|s\|_{n}^{\Pi}$. From Lemma
4.2 for every $n$, there is some formula, $\phi^{n}_{s}$, such that for all
$w\in S$, $M_{w}\models\phi^{n}_{s}$ if and only if $w\in\|s\|_{n}$. Let
$\psi$ be the formula ${\heartsuit}\rightarrow\phi^{n}_{s}$. Then:

    1. (a)

$M_{s}\models\psi$. It is clear that $s$ is $n$-$\Pi$-bisimilar to itself, so
$M_{s}\models\phi^{n}_{s}$.

    2. (b)

$M_{t_{i}}\models\psi$, for $i=1,\ldots,7$. Since $M_{t_{i}}\models local$, we
have $M_{t_{i}}\models oneLabel$. We also have $M_{t_{i}}\models\ell\lor r\lor
u\lor d$, so $M_{t_{i}}\not\models{\heartsuit}$. As the antecedent is not
satisfied, we have $M_{t_{i}}\models\psi$

    3. (c)

$M_{t}\models\psi$. This follows from the reasoning used in the previous case,
since we have $M_{t}\models local$ and $M_{t}\models u$.

Therefore after announcing $\psi$, the worlds $s,t_{1},\ldots,t_{7}$, and $t$
would all remain in the model $M^{\psi}=(S^{\psi},R^{\psi},V^{\psi})$.
However, we know that there is no $v\sim_{\mathfrak{s}}t$ such that
$v\in\|s\|_{n}$, so for all $v\in tR_{\mathfrak{s}}$, we have
$M_{v}\models\neg\phi^{n}_{s}$. For all $v\in tR_{\mathfrak{s}}\cap S^{\psi}$
we must have $M_{v}\models({\heartsuit}\rightarrow\phi)\land\neg\phi^{n}_{s}$,
so it must be that $M_{v}\models\neg{\heartsuit}$. As propositions are
preserved by announcements, we have $M^{\psi}_{t}\models
K_{\mathfrak{s}}\neg{\heartsuit}$, and hence

$M^{\psi}_{s}\models\widehat{K}_{\mathfrak{s}}(r\land(\widehat{K}_{\mathfrak{e}}(\ell\land\widehat{K}_{\mathfrak{s}}(u\land\widehat{K}_{\mathfrak{e}}(d\land\widehat{K}_{\mathfrak{s}}(\ell\land\widehat{K}_{\mathfrak{e}}(r\land\widehat{K}_{\mathfrak{s}}(d\land\widehat{K}_{\mathfrak{e}}(u\land
K_{\mathfrak{s}}\neg{\heartsuit})\\!)\\!)\\!)\\!)\\!)\\!)\\!)\\!)$ (24)

It follows that $M_{s}\models\neg c_{apa}({\heartsuit})$ giving us the
required contradiction. A similar argument can be given for each of the other
card suits, completing the proof.

###  5.2 Group announcements

The approach for group announcements is similar to to the approach for
arbitrary public announcements, except we are now able to use group
announcements, which allow for a more direct proof. We note that the approach
for coalition announcements below could also be applied to group announcement
logic, since it only uses the coalition of both agents, which is equivalent to
a group announcement from both agents. However, we have chosen to present a
separate proof for group announcement logic since it only requires us to use
single agent groups, and is consequently a stronger result. The properties are
formalized as follows:

  * •

For all $n$, for every center world, $w$, of any square, there is some square
below some square to the left of some square above some square to the right of
that square, whose center world is $n$-bisimilar to $w$.

$\displaystyle c_{ga}(X)$ $\displaystyle=$ $\displaystyle
X\rightarrow[\mathfrak{s}](K_{\mathfrak{s}}(r\rightarrow(K_{\mathfrak{e}}(\ell\rightarrow
K_{\mathfrak{s}}(u\rightarrow K_{\mathfrak{e}}(d\rightarrow$
$\displaystyle\qquad K_{\mathfrak{s}}(\ell\rightarrow
K_{\mathfrak{e}}(r\rightarrow
K_{\mathfrak{s}}(d\rightarrow\widehat{K}_{\mathfrak{e}}(u\land\widehat{K}_{\mathfrak{s}}X))))))))))$
$\displaystyle cyc_{ga}$ $\displaystyle=$ $\displaystyle
c_{ga}({\heartsuit})\land c_{ga}({\clubsuit})\land c_{ga}({\diamondsuit})\land
c_{ga}({\spadesuit})$

  * •

For all $n$, for every center world, $w$, of every reachable square there is
some $\mathfrak{e}$-accessible world that is $n$-bisimilar to $w$.

$\begin{array}[]{l}t_{ga}(X,Y,Z)=X\rightarrow[\mathfrak{e}]K_{\mathfrak{s}}\bigwedge\left[\begin{array}[]{l}r\rightarrow
K_{\mathfrak{e}}(\ell\rightarrow\widehat{K}_{\mathfrak{s}}Y)\\\ u\rightarrow
K_{\mathfrak{e}}(d\rightarrow\widehat{K}_{\mathfrak{s}}Z)\\\ \ell\rightarrow
K_{\mathfrak{e}}(r\rightarrow\widehat{K}_{\mathfrak{s}}Y)\\\ d\rightarrow
K_{\mathfrak{e}}(u\rightarrow\widehat{K}_{\mathfrak{s}}Z)\end{array}\right]\\\
ck_{ga}=t_{ga}({\heartsuit},{\clubsuit},{\spadesuit})\land
t_{ga}({\clubsuit},{\heartsuit},{\diamondsuit})\land
t_{ga}({\diamondsuit},{\spadesuit},{\clubsuit})\land
t_{ga}({\spadesuit},{\diamondsuit},{\heartsuit})\end{array}$

We define the formula:

$CB_{ga}=K_{\mathfrak{s}}K_{\mathfrak{e}}K_{\mathfrak{s}}(local\land
cyc_{ga}\land ck_{ga})$ (25)

It is worth taking the time to compare the formulas $cyc_{ga}$ and $ck_{ga}$
to the corresponding formulations for arbitrary announcements: respectively
$cyc_{apa}$ and $ck_{apa}$. Consider a simple fragment of these:

$\displaystyle ck_{ga}^{*}$ $\displaystyle=$
$\displaystyle{\heartsuit}\rightarrow[\mathfrak{e}]K_{\mathfrak{s}}\left[r\rightarrow
K_{\mathfrak{e}}(\ell\rightarrow\widehat{K}_{\mathfrak{s}}{\clubsuit})\right]$
$\displaystyle ck_{apa}^{*}$ $\displaystyle=$
$\displaystyle{\heartsuit}\rightarrow[\bullet]\left[K_{\mathfrak{e}}\neg{\clubsuit}\rightarrow
K_{\mathfrak{s}}(r\rightarrow K_{\mathfrak{e}}(\ell\rightarrow
K_{\mathfrak{s}}\neg{\clubsuit}))\right]$

While each formula has a similar purpose and structure, the formulas used for
group announcements are more direct. The purpose of $ck_{ga}^{*}$ is to say
that agent $\mathfrak{e}$ cannot distinguish the center of a
${\heartsuit}$-square from the center of the ${\clubsuit}$-square to its
right. As any group announcement made by $\mathfrak{e}$ at the center of the
hearts square cannot rule out any world that agent $\mathfrak{e}$ cannot
distinguish from the center of the hearts world, the formula simply needs to
assert that after any such group announcement, if the intermittent edge worlds
remain (the $r$ and $\ell$ worlds), then the center of the ${\clubsuit}$
square must also remain. However, achieving the same using arbitrary
announcements is more complicated. After making any public announcement, if
there are no ${\clubsuit}$-worlds accessible by agent $\mathfrak{e}$ from the
center of the ${\heartsuit}$-square, then there can be no ${\clubsuit}$ at the
center of the square to the right. The correctness of this construction is
shown in Lemma 5.2.

Essentially, in GAL we are quantifying over what an agent knows to be true, so
the accessibility relation for that agent is implicit in the quantification
whereas, in APAL we quantify over all formulas, so we must make the
reachability explicit in the formula. The following lemma has a similar form
to Lemma 5.2 and provides the main technical result that allows us to define
the checkerboard like model, and hence express the tiling problem. Note that
whilst the Lemma below is very similar to the statement of Lemma 5.2, there
are some small but significant differences between the two.

######  Lemma 5.4.

Suppose that $M=(S,\sim,V)$, $s\in S$ and $M_{s}\models CB_{ga}\land card$.
Let $U=sR(\mathfrak{s};r?;\mathfrak{e};\ell?;\mathfrak{s})\cup
sR(\mathfrak{s};u?;\mathfrak{e};d?;\mathfrak{s})\cup
sR(\mathfrak{s};\ell?;\mathfrak{e};r?;\mathfrak{s})\cup
sR(\mathfrak{s};d?;\mathfrak{e};u?;\mathfrak{s})$. Then:

  1. 1.

For all $n\in\mathbb{N}$, for all $t^{\prime}\in U$, there is some
$t\sim_{\mathfrak{s}}t^{\prime}$ and some $v\sim_{\mathfrak{e}}s$ such that
$v\in\|t\|_{n}$.

  2. 2.

For all $n\in\mathbb{N}$, for all $t\in
sR(\mathfrak{s};r?;\mathfrak{e};\ell?;\mathfrak{s};u?;\mathfrak{e};d?;\mathfrak{s};\ell?;\mathfrak{e};r?;\mathfrak{s};d?)$,
there is some $v\sim_{\mathfrak{e}}t$ and some $w\sim_{\mathfrak{s}}v$ such
that $M_{v}\models u$ and $w\in\|s\|_{n}$.

######  Proof 5.5.

  1. 1.

We will assume $t^{\prime}\in
sR(\mathfrak{s};r?;\mathfrak{e};\ell?;\mathfrak{s})$ and the cases for
$t^{\prime}\in sR(\mathfrak{s};u?;\mathfrak{e};d?;\mathfrak{s})$,
$t^{\prime}\in sR(\mathfrak{s};\ell?;\mathfrak{e};r?;\mathfrak{s})$ and
$t^{\prime}\in sR(\mathfrak{s};d?;\mathfrak{e};u?;\mathfrak{s})$ are similar.
Suppose, for contradiction, that there is some $n\in\mathbb{N}$ and some
$t^{\prime}\in sR(\mathfrak{s};r?\mathfrak{e};\ell?)$ such that for all
$t\sim_{\mathfrak{s}}t^{\prime}$, for all $v\sim_{\mathfrak{e}}s$,
$v\notin\|t\|_{n}$. Then, by Lemma 4.4, there is a set of epistemic formulas
$\phi_{0},\ldots,\phi_{m}$ such that:

    1. (a)

for all $v\sim_{\mathfrak{e}}s$ there is some $a\leq m$ such that
$M_{v}\models\phi_{a}$;

    2. (b)

for all $a\leq m$, there is some $v\sim_{\mathfrak{e}}s$ such that
$M_{v}\models\phi_{a}$; and

    3. (c)

for all $a\leq m$, for all $v\sim_{\mathfrak{e}}s$ where
$M_{v}\models\phi_{a}$, for all $t\in S$, $M_{t}\models\phi_{a}$ if and only
if $t\in\|v\|_{n}$.

It follows that $M_{s}\models K_{\mathfrak{e}}\bigvee_{a\leq m}\phi_{a}$, and
by our assumption, for all $t\sim_{\mathfrak{s}}t^{\prime}$ we have
$M_{t}\models\neg K_{\mathfrak{e}}\bigvee_{a\leq m}\phi_{a}$. Let $\psi$ be
the formula $K_{\mathfrak{e}}(\ell\lor r\lor\bigvee_{a\leq m}\phi_{a})$. (Even
though, from the fact $M_{s}\models local$, we have $M_{s}\models
K_{\mathfrak{e}}(\neg\ell\land\neg r)$, we include the propositions $\ell$ and
$r$ in the disjunction for $\psi$ since they do not stop agent $\mathfrak{e}$
knowing $\psi$ is true, but they do prevent the intermittent $\ell$ and $r$
worlds from being removed by the announcement of $\psi$.)

In the model $M^{\psi}=(S^{\psi},R^{\psi},V^{\psi})$ we have

    1. (a)

$s\in S^{\psi}$, since for some $a\leq m$, $M_{s}\models\phi_{a}$, so the
announcement $\psi$ is not vacuous.

    2. (b)

for all $t^{\prime}\in sR(\mathfrak{s};r?)$, $t^{\prime}\in S^{\psi}$, since
$M_{t^{\prime}}\models K_{\mathfrak{e}}r$

    3. (c)

for all $t^{\prime}\in sR(\mathfrak{s};r?;\mathfrak{e};\ell?)$, $t^{\prime}\in
S^{\psi}$, since $M_{t^{\prime}}\models K_{\mathfrak{e}}\ell$

    4. (d)

for some $t^{\prime}\in sR(\mathfrak{s};r?;\mathfrak{e};\ell?)$ for every
$t\sim_{\mathfrak{s}}t^{\prime}$, if $t\in S^{\psi}$, then $M_{t}\models\neg
card$. By our assumption that for all $t\sim_{\mathfrak{s}}t^{\prime}$, for
all $v\sim_{\mathfrak{e}}s$, $t\notin\|v\|_{n}$, we have
$M_{t}\not\models\bigvee_{a\leq m}\phi_{a}$. Since $M_{s}\models
K_{\mathfrak{s}}K_{\mathfrak{e}}local$, it follows that $M_{t}\models
card\rightarrow K_{\mathfrak{e}}(\neg\ell\land\neg r)$, so $M_{t}\models
card\rightarrow\neg\psi$.

Therefore
$M^{\psi}_{s}\models\widehat{K}_{\mathfrak{s}}(r\land\widehat{K}_{\mathfrak{e}}(\ell\land
K_{\mathfrak{s}}\neg card))$. Hence $M_{s}\models
card\rightarrow\langle\psi\rangle\widehat{K}_{\mathfrak{s}}(r\land\widehat{K}_{\mathfrak{e}}(\ell\land
K_{\mathfrak{s}}\neg card))$ which is sufficient to contradict that
$M_{s}\models ck_{ga}$. Note that regardless of how $X$, $Y$, and $Z$ are
applied in the definition of $t_{ga}(X,Y,Z)$ this proof only requires that
$(X\lor Y\lor Z)\rightarrow card$.

As in Lemma 5.2, the cases for $t^{\prime}\in
sR(\mathfrak{s};u?;\mathfrak{e};d?;\mathfrak{s})$, $t^{\prime}\in
sR(\mathfrak{s};\ell?;\mathfrak{e};r?;\mathfrak{s})$ and $t^{\prime}\in
sR(\mathfrak{s};d?;\mathfrak{e};u?;\mathfrak{s})$ and accounted for in a
similar manner.

  2. 2.

For the final part of this proof we are required to show that for all $n$, for
all $t\in
sR(\mathfrak{s};r?;\mathfrak{e};\ell?;\mathfrak{s};u?;\mathfrak{e};d?;\mathfrak{s};\ell?;\mathfrak{e};r?;\mathfrak{s};d?)$,
there is some $v\sim_{\mathfrak{e}}t$ and $w\sim_{\mathfrak{s}}v$ such that
$M_{v}\models v$ and $w\in\|n\|_{s}$. We begin by considering any chain of
worlds

$s\sim_{\mathfrak{s}}t_{1}\sim_{\mathfrak{e}}t_{2}\sim_{\mathfrak{s}}t_{3}\sim_{\mathfrak{e}}t_{4}\sim_{\mathfrak{s}}t_{5}\sim_{\mathfrak{e}}t_{6}\sim_{\mathfrak{s}}t$

where $t_{1},t_{6}\in V(r)$, $t_{2},t_{5}\in V(\ell)$, $t_{3}\in V(u)$, and
$t_{4},t\in V(d)$.

We first show that from the first part of this lemma, each world in this chain
satisfies the formula $local$ (22). We will suppose without loss of
generality, that $M_{s}\models{\heartsuit}$. Because $M_{s}\models CB_{ga}$,
it follows that $M_{s}\models K_{\mathfrak{s}}K_{\mathfrak{e}}local$.
Therefore $t_{1}$ must satisfy $local$. Furthermore, from the first part of
this lemma with the first component from $U$, we know for all
$n\in\mathbb{N}$, for all $t_{2}\in sR(\mathfrak{s};r?;\mathfrak{e};\ell?)$,
there is some $w_{1}\sim_{\mathfrak{s}}t_{2}$ where $M_{w_{1}}\models card$,
and some $v_{1}\sim_{\mathfrak{e}}s$ such that $w_{1}\in\|v_{1}\|_{n}$. Since
the modal depth of $local$ is $5$, we may suppose, without loss of generality,
that $w_{1}\in\|v_{1}\|_{14}^{\Pi}$. Since $v_{1}\sim_{\mathfrak{e}}s$, we
have $M_{v_{1}}\models CB_{ga}$ and also $M_{v_{1}}\models
K_{\mathfrak{e}}K_{\mathfrak{s}}local$. By Lemma 4.6, $n$-$\Pi$-bisimilarity
preserves the interpretation of pure modal formulas with modal depth up to
$n$, we have $M_{w_{1}}\models K_{\mathfrak{s}}local$. Since
$w_{1}\sim_{\mathfrak{s}}t_{2}$ and $t_{2}\sim_{\mathfrak{s}}t_{3}$ it follows
that $M_{t_{2}}\models local$ and $M_{t_{3}}\models local$. Since
$M_{v_{1}}\models CB_{ga}\land card$, from the first part of this lemma with
the second component of $U$, for all $n\in\mathbb{N}$, for all $v^{\prime}\in
v_{1}R(\mathfrak{s};u?;\mathfrak{e};d?)$, for all
$v^{\prime\prime}\sim_{\mathfrak{s}}v^{\prime}$ where
$M_{v^{\prime\prime}}\models card$, there is some
$v_{2}\sim_{\mathfrak{e}}v_{1}$ such that $v^{\prime\prime}\in\|v_{2}\|_{n}$.
As $w_{1}\in\|v_{1}\|_{14}^{\Pi}$, for every $t^{\prime}\in
w_{1}R(\mathfrak{s};u?;\mathfrak{e};d?)$, there is some
$w_{2}\sim_{\mathfrak{s}}t^{\prime}$ such that $M_{w_{2}}\models card$, and
some $v^{\prime\prime}\in
v_{1}R(\mathfrak{s};u?;\mathfrak{e};d?;\mathfrak{s})$ where
$M_{v^{\prime\prime}}\models card$ and $w_{2}\in\|v^{\prime\prime}\|_{11}$.
Putting the last two statements together, for every $t^{\prime}\in
w_{1}R(\mathfrak{s};u?;\mathfrak{e};d?)$, there is some
$w_{2}\sim_{\mathfrak{s}}t^{\prime}$ and some $v_{2}\sim_{\mathfrak{e}}v_{1}$
such that $w_{2}\in\|v_{2}\|_{11}$. As $v_{2}\sim_{\mathfrak{e}}v_{1}$, and
$v_{1}\sim_{\mathfrak{e}}s$, we have $v_{2}\sim_{\mathfrak{e}}s$, and hence
$M_{v_{2}}\models K_{\mathfrak{e}}K_{\mathfrak{s}}local$. As
$w_{1}\sim_{\mathfrak{s}}t_{3}$, there is some such $w_{2}$ and $v_{2}$ such
that $t_{4}\sim_{\mathfrak{s}}w_{2}$ and $t_{5}\sim_{\mathfrak{s}}w_{2}$. From
Lemma 4.6 we have $M_{t_{4}}\models local$ and $M_{t_{5}}\models local$.

Continuing in this way, (using the third component of $U$) we are able to find
some $w_{3}$ such that $t_{6}\sim_{\mathfrak{s}}w_{3}$,
$t\sim_{\mathfrak{s}}w_{3}$ and for some $v_{3}\sim_{\mathfrak{e}}s$,
$w_{3}\in\|v_{3}\|_{8}$. Since the modal depth of $local$ is $5$, it follows
that $t_{1},\ t_{2},\ t_{3},\ t_{4},\ t_{5},\ t_{6}$ and $t$ all satisfy
$local$, so every world has just one label, and every square contains a world
labelled by each direction, and so on.

We are required to show for every such $t$, for any given $n$, there is some
$v\sim_{\mathfrak{e}}t$ and some $w\sim_{\mathfrak{s}}v$ such that
$M_{v}\models u$ and $w\in\|s\|_{n}$. Suppose that this was not the case. Then
for some $n\in\mathbb{N}$, for some $t\in
sR(\mathfrak{s};r?;\mathfrak{e};\ell?;\mathfrak{s};u?;\mathfrak{e};d?;\mathfrak{s};\ell?;\mathfrak{e};r?;\mathfrak{s};d?)$,
we have for all $v\sim_{\mathfrak{e}}t$ where $M_{v}\models u$, for all
$w\sim_{\mathfrak{s}}v$, $w\notin\|s\|_{n}$. From Lemma 4.4 for every $n$,
there is a set of formulas, $\phi_{0},\ldots,\phi_{m}$, such that

    1. (a)

for all $s^{\prime}\sim_{\mathfrak{s}}s$ there is some $a\leq m$ such that
$M_{s^{\prime}}\models\phi_{a}$, and for all $t^{\prime}\in S$,
$M_{t^{\prime}}\models\phi_{a}$ if and only if
$t^{\prime}\in\|s^{\prime}\|_{n}$.

    2. (b)

for all $a\leq m$ there is some $s^{\prime}\sim_{\mathfrak{s}}s$ such that
$M_{s^{\prime}}\models\phi_{a}$;

Let $\psi$ be the formula $K_{\mathfrak{s}}({\heartsuit}\rightarrow
K_{\mathfrak{s}}\bigvee_{a\leq m}\phi_{a})$. Then:

    1. (a)

$M_{s}\models\psi$. It is clear that for every
$s^{\prime}\sim_{\mathfrak{s}}s$, $s^{\prime}$ is $n$-$\Pi$-bisimilar to
itself, so $M_{s^{\prime}}\models\bigvee_{a\leq m}\phi_{a}$. Therefore
$M_{s}\models K_{\mathfrak{s}}\psi$.

    2. (b)

$M_{t_{i}}\models\psi$, for $i=1,\ldots,6$. Since $M_{t_{i}}\models local$, we
have $M_{t_{i}}\models oneLabel$. We also have $M_{t_{i}}\not\models
K_{\mathfrak{s}}{\heartsuit}$. As the antecedent is not satisfied, we have
$M_{t_{i}}\models\psi$

    3. (c)

$M_{t}\models\psi$. This follows from the reasoning used in the previous case,
since we have $M_{t}\models local$ and $M_{t}\models
K_{\mathfrak{s}}\neg{\heartsuit}$.

Therefore, at $s$ agent $\mathfrak{s}$ may make the announcement $\psi$, and
after announcing $\psi$, the worlds $s,t_{1},\ldots,t_{6}$, and $t$ would all
remain in the model $M^{\psi}=(S^{\psi},R^{\psi},V^{\psi})$. However, we know
that there is no $v\sim_{\mathfrak{e}}t$ where $M_{v}\models u$, such that for
some $w\sim_{\mathfrak{s}}v$, $w\in\|s\|_{n}$. So for all $v\in
tR_{\mathfrak{e}}$, we have $M_{v}\models K_{\mathfrak{s}}(u\rightarrow
K_{\mathfrak{s}}\neg\bigvee_{a\leq m}\phi_{a})$. Therefore, for all $v\in
tR_{\mathfrak{e}}\cap S^{\psi}$ where $M_{v}\models u$, for all $w\in
vR_{\mathfrak{s}}\cap S^{\psi}$, we must have $M_{w}\models
K_{\mathfrak{s}}\neg{\heartsuit}$. As propositions are preserved by
announcements, we have $M^{\psi}_{t}\models K_{\mathfrak{s}}\neg{\heartsuit}$,
and hence

$\displaystyle M^{\psi}_{s}$ $\displaystyle\models$
$\displaystyle\widehat{K}_{\mathfrak{s}}(r\land(\widehat{K}_{\mathfrak{e}}(\ell\land\widehat{K}_{\mathfrak{s}}(u\land\widehat{K}_{\mathfrak{e}}(d\land$
$\displaystyle\qquad\widehat{K}_{\mathfrak{s}}(\ell\land\widehat{K}_{\mathfrak{e}}(r\land\widehat{K}_{\mathfrak{s}}(d\land
K_{\mathfrak{e}}(u\rightarrow K_{\mathfrak{s}}\neg{\heartsuit})))))))))$

It follows that $M_{s}\models\neg cyc_{ga}$ (regardless of suit) giving us the
required contradiction.

###  5.3 Coalition announcements

The proof for coalition announcement logic is a combination of the two
previous cases. We use a coalition of both agents (which is effectively a
group announcement), and the constructions for the arbitrary public
announcement logic. We briefly compare the constructions below to the previous
cases for group announcements and arbitrary announcements. With coalition
announcements we can no longer rely on the accessibility relations being
implicit in the quantified announcement, as with group announcements, since
the quantification is now over the accessibility relations of all agents. As a
result we must use the more complicated constructions of APAL, along with the
proof methods of GAL. The properties are formalized as follows:

  * •

For all $n$, for every center world, $w$, of any square, there is some square
below some square to the left of some square above some square to the right of
that square, whose center world is $n$-bisimilar to $w$.

$\displaystyle c_{ca}(X)$ $\displaystyle=$ $\displaystyle
X\rightarrow[\\!\langle\mathfrak{s},\mathfrak{e}\rangle\\!](K_{\mathfrak{s}}(r\rightarrow(K_{\mathfrak{e}}(\ell\rightarrow
K_{\mathfrak{s}}(u\rightarrow K_{\mathfrak{e}}(d\rightarrow$
$\displaystyle\qquad K_{\mathfrak{s}}(\ell\rightarrow
K_{\mathfrak{e}}(r\rightarrow K_{\mathfrak{s}}(d\rightarrow
K_{\mathfrak{e}}(u\rightarrow\widehat{K}_{\mathfrak{s}}X))))))))))$
$\displaystyle cyc_{ca}$ $\displaystyle=$ $\displaystyle
c_{ca}({\heartsuit})\land c_{ca}({\clubsuit})\land c_{ca}({\diamondsuit})\land
c_{ca}({\spadesuit})$

  * •

For all $n$, for every center world, $w$, of every reachable square there is
some $\mathfrak{e}$-accessible world that is $n$-bisimilar to $w$.

$\begin{array}[]{l}t_{ca}(X,Y,Z)=X\rightarrow\bigwedge\left[\begin{array}[]{l}[\\!\langle\mathfrak{s},\mathfrak{e}\rangle\\!](K_{\mathfrak{e}}\neg
Y\rightarrow K_{\mathfrak{s}}(r\rightarrow K_{\mathfrak{e}}(\ell\rightarrow
K_{\mathfrak{s}}\neg Y)))\\\
[\\!\langle\mathfrak{s},\mathfrak{e}\rangle\\!](K_{\mathfrak{e}}\neg
Z\rightarrow K_{\mathfrak{s}}(u\rightarrow K_{\mathfrak{e}}(d\rightarrow
K_{\mathfrak{s}}\neg Z)))\\\
[\\!\langle\mathfrak{s},\mathfrak{e}\rangle\\!](K_{\mathfrak{e}}\neg
Y\rightarrow K_{\mathfrak{s}}(\ell\rightarrow K_{\mathfrak{e}}(r\rightarrow
K_{\mathfrak{s}}\neg Y)))\\\
[\\!\langle\mathfrak{s},\mathfrak{e}\rangle\\!](K_{\mathfrak{e}}\neg
Z\rightarrow K_{\mathfrak{s}}(d\rightarrow K_{\mathfrak{e}}(u\rightarrow
K_{\mathfrak{s}}\neg Z)))\end{array}\right]\\\
ck_{ca}=t_{ca}({\heartsuit},{\clubsuit},{\spadesuit})\land
t_{ca}({\clubsuit},{\heartsuit},{\diamondsuit})\land
t_{ca}({\diamondsuit},{\spadesuit},{\clubsuit})\land
t_{ca}({\spadesuit},{\diamondsuit},{\heartsuit})\end{array}$

We define the formula:

$CB_{ca}=K_{\mathfrak{s}}K_{\mathfrak{e}}K_{\mathfrak{s}}(local\land
cyc_{ca}\land ck_{ca})$ (26)

The following lemma provides the main technical result that allows us to
define the checkerboard like model, and hence express the tiling problem.

######  Lemma 5.6.

Suppose that $M=(S,\sim,V)$, $s\in S$ and $M_{s}\models CB_{ca}\land card$.
Let $U=sR(\mathfrak{s};r?;\mathfrak{e};\ell?;\mathfrak{s})\cup
sR(\mathfrak{s};u?;\mathfrak{e};d?;\mathfrak{s})\cup
sR(\mathfrak{s};\ell?;\mathfrak{e};r?;\mathfrak{s})\cup
sR(\mathfrak{s};d?;\mathfrak{e};u?;\mathfrak{s})$. Then:

  1. 1.

For all $n\in\mathbb{N}$, for all $t\in U$, if $M_{t}\models card$, then there
is some $v\sim_{\mathfrak{e}}s$ such that $v\in\|t\|_{n}$.

  2. 2.

For all $n\in\mathbb{N}$, for all $t\in
sR(\mathfrak{s};r?;\mathfrak{e};\ell?;\mathfrak{s};u?;\mathfrak{e};d?;\mathfrak{s};\ell?;\mathfrak{e};r?;\mathfrak{s};d?;\mathfrak{e};u?)$,
there is some $v\sim_{\mathfrak{s}}t$ such that $v\in\|s\|_{n}$.

######  Proof 5.7.

  1. 1.

As in the proof of Lemma 5.2, we address the case for $t\in
sR(\mathfrak{s};r?;\mathfrak{e};\ell?;\mathfrak{s})$ and the cases of $t\in
sR(\mathfrak{s};u?;\mathfrak{e};d?;\mathfrak{s})$, $t\in
sR(\mathfrak{s};\ell?;\mathfrak{e};r?;\mathfrak{s})$ and $t\in
sR(\mathfrak{s};d?;\mathfrak{e};u?;\mathfrak{s})$ are done in a similar
manner. Also suppose, without loss of generality, that
$M_{s}\models{\heartsuit}$. The following proof may be easily adapted to other
suits. Now suppose for contradiction that there is some $n\in\mathbb{N}$ and
some $t\in sR(\mathfrak{s};r?\mathfrak{e};\ell?;\mathfrak{s})$ where
$M_{t}\models card$, and for all $v\sim_{\mathfrak{e}}s$, $v\notin\|t\|_{n}$.
Then, by Lemma 4.2, there is some epistemic formula $\phi_{t}^{n}$ such that
for all $t^{\prime}\in S$, $M_{t^{\prime}}\models\phi_{t}^{n}$ if and only if
$t^{\prime}\in\|t\|_{n}$. As for all $v\sim_{\mathfrak{e}}s$, we have
$v\notin\|t\|_{n}$, it follows that$M_{v}\models\neg\phi_{t}^{n}$. Therefore
$M_{v}\models{\clubsuit}\rightarrow\neg\phi_{t}^{n}$ and thus $M_{s}\models
K_{\mathfrak{e}}({\clubsuit}\rightarrow\neg\phi_{t}^{n}$). (Introducing the
antecedent ${\clubsuit}$ prevents the announcement of
$K_{\mathfrak{e}}\phi_{t}^{n}$ from removing the intermittent $\ell$ and $r$
worlds that we require to construct our contradiction.) Because $M_{s}\models
local$, we have $M_{s}\models adj_{\heartsuit}$ so $M_{t}\models{\clubsuit}$.
Therefore, in the model $M^{\psi}=(S^{\psi},R^{\psi},V^{\psi})$ we have

    1. (a)

$s\in S^{\psi}$, since $M_{s}\models{\heartsuit}$ so
$M_{s}\models\neg{\clubsuit}$ and the antecedent of $\psi$ is not satisfied.

    2. (b)

for all $t^{\prime}\in sR(\mathfrak{s};r?)$, $t^{\prime}\in S^{\psi}$, since
$M_{t^{\prime}}\models r$ so $M_{t^{\prime}}\models\neg{\clubsuit}$ and the
antecedent of $\psi$ is not satisfied.

    3. (c)

for all $t^{\prime}\in sR(\mathfrak{s};r?;\mathfrak{e};\ell?)$, $t^{\prime}\in
S^{\psi}$, since $M_{t^{\prime}}\models\ell$ so the antecedent of $\psi$ is
not satisfied.

    4. (d)

for all $t^{\prime}\sim_{\mathfrak{e}}s$, where
$M_{t^{\prime}}\models{\clubsuit}$, we have $t^{\prime}\notin S^{\psi}$, since
$t^{\prime}\notin\|t\|_{n}$, so $M_{t^{\prime}}\models\neg\phi_{t}^{n}$.

    5. (e)

$t\in S^{\psi}$ since clearly $t\in\|t\|_{n}$ so $M_{t}\models\phi_{t}^{n}$.

Therefore $M^{\psi}_{s}\models
K_{\mathfrak{e}}\neg{\clubsuit}\land\widehat{K}_{\mathfrak{s}}(r\land\widehat{K}_{\mathfrak{e}}(\ell\land\widehat{K}_{\mathfrak{s}}{\clubsuit}))$.
As the coalition announcement may consist of $K_{\mathfrak{e}}\psi$ and
$K_{\mathfrak{s}}\top$ we have

$M_{s}\models{\heartsuit}\land\langle\\![\mathfrak{s},\mathfrak{e}]\\!\rangle(K_{\mathfrak{e}}\neg{\clubsuit}\land\widehat{K}_{\mathfrak{s}}(r\land\widehat{K}_{\mathfrak{e}}(\ell\land\widehat{K}_{\mathfrak{s}}{\clubsuit})))$

which is sufficient to contradict our assumption $M_{s}\models
CB_{ca}\land{\heartsuit}$.

As before, the proofs for $t\in
sR(\mathfrak{s};u?;\mathfrak{e};d?;\mathfrak{s})$, $t\in
sR(\mathfrak{s};\ell?;\mathfrak{e};r?;\mathfrak{s})$ and $t\in
sR(\mathfrak{s};d?;\mathfrak{e};u?;\mathfrak{s})$ are done similarly.

  2. 2.

For the final part of this proof we are required to show that for all $n$, for
all $t\in
sR(\mathfrak{s};r?;\mathfrak{e};\ell?;\mathfrak{s};u?;\mathfrak{e};d?;\mathfrak{s};\ell?;\mathfrak{e};r?;\mathfrak{s};d?;\mathfrak{e};u?)$,
there is some $v\sim_{\mathfrak{s}}t$ such that $v\in\|n\|_{s}$. We begin by
considering any chain of worlds

$s\sim_{\mathfrak{s}}t_{1}\sim_{\mathfrak{e}}t_{2}\sim_{\mathfrak{s}}t_{3}\sim_{\mathfrak{e}}t_{4}\sim_{\mathfrak{s}}t_{5}\sim_{\mathfrak{e}}t_{6}\sim_{\mathfrak{s}}t_{7}\sim_{\mathfrak{e}}t$

where $t_{1},t_{6}\in V(r)$, $t_{2},t_{5}\in V(\ell)$, $t_{3},t\in V(u)$, and
$t_{4},t_{7}\in V(d)$.

We may show that from the first four parts of this lemma, each world in this
chain satisfies the formula $local$ (22), using the same argument from the
proof of the fifth clause of Lemma 5.2. We will assume that
$M_{s}\models{\heartsuit}$, and cases for other suits have similar proofs. We
are required to show for every such $t\in
sR(\mathfrak{s};r?;\mathfrak{e};\ell?;\mathfrak{s};u?;\mathfrak{e};d?;\mathfrak{s};\ell?;\mathfrak{e};r?;\mathfrak{s};d?;\mathfrak{e};u?)$,
for any given $n$, there is some $v\sim_{\mathfrak{s}}t$ such that
$v\in\|s\|_{n}$. Suppose that this was not the case. Then there is some such
$t$ and some $n$ such that for all $v\sim_{\mathfrak{s}}t$,
$v\notin\|s\|_{n}$. From Lemma 4.2, there is some formula, $\phi_{s}^{n}$,
such that for all $w\in S$, $M_{w}\models\phi_{s}^{n}$ if and only if
$w\in\|s\|_{n}^{\Pi}$. Let $\psi$ be the formula
${\heartsuit}\rightarrow\widehat{K}_{\mathfrak{s}}\phi_{s}^{n}$. Then:

    1. (a)

$M_{s}\models\psi$. It is clear that $s$ is $n$-$\Pi$-bisimilar to itself, so
$M_{s}\models\phi_{s}^{n}$.

    2. (b)

$M_{t_{i}}\models\psi$, for $i=1,\ldots,7$. Since $M_{t_{i}}\models local$, we
have $M_{t_{i}}\models oneLabel$. We also have $M_{t_{i}}\models\ell\lor r\lor
u\lor d$, so $M_{t_{i}}\not\models{\heartsuit}$. As the antecedent is not
satisfied, we have $M_{t_{i}}\models\psi$

    3. (c)

$M_{t}\models\psi$. This follows from the reasoning used in the previous case,
since we have $M_{t}\models local$ and $M_{t}\models u$.

    4. (d)

for all $v\sim_{\mathfrak{s}}t$, if $M_{v}\models{\heartsuit}$, the
$M_{v}\models\neg\psi$. Since if
$M_{v}\models\widehat{K}_{\mathfrak{s}}\phi_{s}^{n}$ there would be some
$v^{\prime}\sim_{\mathfrak{s}}t$ such that $v^{\prime}\in\|s\|_{n}$
contradicting our assumption.

Therefore after announcing $\psi$, the worlds $s,t_{1},\ldots,t_{7}$, and $t$
would all remain in the model $M^{\psi}=(S^{\psi},R^{\psi},V^{\psi})$.
However, for all $v\in tR_{\mathfrak{s}}\cap S^{\psi}$ we must have
$M_{v}\models({\heartsuit}\rightarrow\phi)\land\neg\phi$, so it must be that
$M_{v}\models\neg{\heartsuit}$. As propositions are preserved by
announcements, we have $M^{\psi}_{t}\models K_{\mathfrak{s}}\neg{\heartsuit}$,
and hence

$M^{\psi}_{s}\models\widehat{K}_{\mathfrak{s}}(r\land(\widehat{K}_{\mathfrak{e}}(\ell\land\widehat{K}_{\mathfrak{s}}(u\land\widehat{K}_{\mathfrak{e}}(d\land\widehat{K}_{\mathfrak{s}}(\ell\land\widehat{K}_{\mathfrak{e}}(r\land\widehat{K}_{\mathfrak{s}}(d\land\widehat{K}_{\mathfrak{e}}(u\land
K_{\mathfrak{s}}\neg{\heartsuit})\\!)\\!)\\!)\\!)\\!)\\!)\\!)\\!)$ (27)

It follows that $M_{s}\models\neg cyc_{ga}({\heartsuit})$ giving us the
required contradiction. A similar argument can be given for each of the other
card suits, completing the proof.

##  6 Undecidability

In this section we show how the formulas $CB_{apa}$, $CB_{ga}$, and $CB_{ca}$
enforce the checkerboard structure of Figure 4 making the satisfiability of
$SAT_{\Gamma}$ (4) equivalent to the existence of a $\Gamma$-tiling of the
plane.

As the proof is complex, but uniform for the logics APAL, GAL and CAL, given
the different variations of Lemmas 5.2, 5.4 and 5.6, we can give a single
presentation of the remaining steps required. To that end, we give a unified
presentation of Lemma 5.2, Lemma 5.4 and Lemma 5.6.

######  Corollary 6.1.

Suppose that $M=(S,\sim,V)$, $s\in S$ and either
$M_{s}\models_{APAL}CB_{apa}\land card$, or $M_{s}\models_{GAL}CB_{ga}\land
card$ or $M_{s}\models_{CAL}CB_{ca}\land card$. Let
$U=sR(\mathfrak{s};r?;\mathfrak{e};\ell?;\mathfrak{s})\cup
sR(\mathfrak{s};u?;\mathfrak{e};d?;\mathfrak{s})\cup
sR(\mathfrak{s};\ell?;\mathfrak{e};r?;\mathfrak{s})\cup
sR(\mathfrak{s};d?;\mathfrak{e};u?;\mathfrak{s})$. Then, for all
$s^{\prime}\sim_{\mathfrak{e}}s$:

  1. 1.

For all $n\in\mathbb{N}$, for all $t^{\prime}\in U$, there is some
$t\sim_{\mathfrak{s}}t^{\prime}$ and some $v\sim_{\mathfrak{e}}s^{\prime}$
such that $v\in\|t\|_{n}$.

  2. 2.

For all $n\in\mathbb{N}$, for all $t\in
s^{\prime}R(\mathfrak{s};r?;\mathfrak{e};\ell?;\mathfrak{s};u?;\mathfrak{e};d?;\mathfrak{s};\ell?;\mathfrak{e};r?;\mathfrak{s};d?;\mathfrak{e};u?)$,
there is some $v\sim_{\mathfrak{s}}t$ such that $v\in\|s^{\prime}\|_{n}$.

######  Proof 6.2.

The GAL case follows from Lemma 5.4, observing that $CB_{ga}$ is known by
agent $\mathfrak{e}$. Additionally, the APAL and CAL cases follow from the
fact that $M_{s}\models adj$ (see (21)) implies that if $M_{s}\models card$
then there is always at least one $t\in sR(\mathfrak{s};r?;edge;\ell?;sq)$,
such that $M_{t}\models card$ (and similarly for the other directions).

The main construction is given in the following two lemmas.

######  Lemma 6.3.

Suppose that $M_{s}\models SAT_{\Gamma}\land{\heartsuit}$ and either
$M_{s}\models_{APAL}CB_{apa}$, or $M_{s}\models_{GAL}CB_{ga}$ or
$M_{s}\models_{CAL}CB_{ca}$. Then $\Gamma$ can tile the plane.

######  Proof 6.4.

Given the model $M=(S,R,V)$ and the state $s$, we construct a $\Gamma$-tiling
of the plane $\mathbb{N}\times\mathbb{N}$. To do this, we inductively define a
series of maps from the points in the plane $\mathbb{N}\times\mathbb{N}$ to
worlds in $S$. From this series we are able to build a complete tiling. Let
$P_{n}=\\{(i,j)\ |\ i+j\leq n\\}$. We show that there exists a map
$\tau_{n}:P_{n}\longrightarrow S$ for each $n\in\mathbb{N}$ such that:

  * •

$\tau_{n}(0,0)=s$.

  * •

For all $i,j\in\mathbb{N}$, if $i+j\leq n$, then
$\tau_{n}(i,j)\sim_{\mathfrak{e}}s$.

  * •

For all $i,j\in\mathbb{N}$, if $n>0$ then there exists
$t\in\tau_{n}(i,j)R(\mathfrak{s};\ell?;\mathfrak{e};r?;\mathfrak{s})$ such
that $\tau_{n}(i+1,j)\in\|t\|_{9(n-(i+j))}^{\Pi}$

  * •

For all $i,j\in\mathbb{N}$, if $n>0$ then there exists
$t\in\tau_{n}(i,j)R(\mathfrak{s};u?;\mathfrak{e};d?;\mathfrak{s})$ such that
$\tau_{n}(i,j+1)\in\|t\|_{9(n-(i+j))}^{\Pi}$

We show such a construction exists for each $n$ by induction. The base of the
induction is $\tau_{n}(0,0)=s$, and for the inductive step, given $(i,j)$, we
suppose that $\tau_{n}(i^{\prime},j^{\prime})$ has been defined for all
$(i^{\prime},j^{\prime})$ where $i^{\prime}+j^{\prime}<i+j$. Let $m=n-(i+j)$.
There are three inductive cases to consider:

  1. 1.

$i=0$: In this case, suppose that $\tau_{n}(0,j-1)=s^{\prime}$. Since
$s^{\prime}\sim_{\mathfrak{e}}s$ we can apply the second clause of Corollary
6.1 to find some $t\in
s^{\prime}R(\mathfrak{s};u?;\mathfrak{e};d?;\mathfrak{s})$, and some
$v\sim_{\mathfrak{e}}s^{\prime}$ such that $v\in\|t\|_{9m}$. We set
$\tau_{n}(0,j)=v$. Since $v\sim_{\mathfrak{e}}s^{\prime}\sim_{\mathfrak{e}}s$,
by transitivity we have $v\sim_{\mathfrak{e}}s$. Since there is some
$t\in\tau_{n}(0,j-1)R(\mathfrak{s};u?;\mathfrak{e};d?;\mathfrak{s})$ such that
$\tau_{n}(i,j)\in\|t\|_{9m}$, the inductive conditions are met.

  2. 2.

$j=0$: In this case, suppose that $\tau_{n}(i-1,0)=s^{\prime}$. Since
$s^{\prime}\sim_{\mathfrak{e}}s$ we can apply the third clause of Corollary
6.1 to find some $t\in
s^{\prime}R(\mathfrak{s};\ell?;\mathfrak{e};r?;\mathfrak{s})$, and some
$v\sim_{\mathfrak{e}}s^{\prime}$ such that $v\in\|t\|_{9m}$. We set
$\tau_{n}(i,0)=v$. Since $v\sim_{\mathfrak{e}}s^{\prime}\sim_{\mathfrak{e}}s$,
by transitivity we have $v\sim_{\mathfrak{e}}s$. Since there is some
$t\in\tau_{n}(0,j-1)R(\mathfrak{s};\ell?;\mathfrak{e};r?;\mathfrak{s})$ such
that $\tau_{n}(i,j)\in\|t\|_{9m}$, the inductive conditions are met.

  3. 3.

$i\neq 0$ and $j\neq 0$: In this case suppose that
$\tau_{n}(i-1,j-1)=s^{\prime}$, $\tau_{n}(i,j-1)=s_{u}$ and
$\tau_{n}(i-1,j)=s_{\ell}$. By the inductive hypothesis we have that

     * •

there is some $v^{\prime}\in
s^{\prime}R(\mathfrak{s};\ell?;\mathfrak{e};r?;\mathfrak{s})$ such that
$s_{\ell}\in\|v^{\prime}\|_{9(m+1)}$.

     * •

there is some $w^{\prime}\in
s^{\prime}R(\mathfrak{s};u?;\mathfrak{e};d?;\mathfrak{s})$ such that
$s_{u}\in\|w^{\prime}\|_{9(m+1)}$.

Since there is some $v^{\prime}\in
s^{\prime}R(\mathfrak{s};\ell?;\mathfrak{e};r?\mathfrak{s})$ such that
$s_{\ell}\in\|v^{\prime}\|_{9(m+1)}$, then there must be some $t^{\prime}\in
s_{\ell}R(\mathfrak{s};r?;\mathfrak{e};\ell?;\mathfrak{s})$ such that
$t^{\prime}\in\|s^{\prime}\|_{9m+6}$. We apply the last clause of Corollary
6.1 to $s_{\ell}$, so that for all $t\in
s_{\ell}R(\mathfrak{s};r?;\mathfrak{e};\ell?;\mathfrak{s};u?;\mathfrak{e};d?;\mathfrak{s};\ell?;\mathfrak{e};r?;\mathfrak{s};d?;\mathfrak{e};u?)$
such that there is some $v\sim_{\mathfrak{s}}t$ where $v\in\|s_{\ell}\|_{9m}$.
Therefore there must be some chain:

$s_{\ell}\sim_{\mathfrak{s}}t_{1}\sim_{\mathfrak{e}}t_{2}\sim_{\mathfrak{s}}t_{3}\sim_{\mathfrak{e}}t_{4}\sim_{\mathfrak{s}}t_{5}\sim_{\mathfrak{e}}t_{6}\sim_{\mathfrak{s}}t_{7}\sim_{\mathfrak{e}}t_{8}$

such that:

    1. (a)

$M_{t_{1}}\models r$, $M_{t_{2}}\models\ell$ and
$t^{\prime}\sim_{\mathfrak{s}}t_{2}$. Since $t^{\prime}\in
s_{\ell}R(\mathfrak{s};r?\mathfrak{e};\ell?;\mathfrak{s})$ and the conditions
of $local$ (22) are met everywhere, we can find a chain that passes through
$t^{\prime}$.

    2. (b)

$M_{t_{3}}\models u$, $M_{t_{4}}\models d$ and there is some
$t_{u}\sim_{\mathfrak{s}}t_{4}$ such that $t_{u}\in\|s_{u}\|_{9m+3}$. Since
$t^{\prime}\in\|s^{\prime}\|_{9m+6}$ and there is some $w^{\prime}\in
s^{\prime}R(\mathfrak{s};u?;\mathfrak{e};d?;\mathfrak{s})$ such that
$s_{u}\in\|w^{\prime}\|_{9(m+1)}$, there must be some $t_{u}\in
t^{\prime}R(\mathfrak{s};u?;\mathfrak{e};d?;\mathfrak{s})$ such that
$t_{u}\in\|v^{\prime}\|_{9m+3}$. Since $n$-bisimilarity is transitive, we have
$t_{u}\in\|s_{u}\|_{9m+3}$.

    3. (c)

$M_{t_{5}}\models\ell$, $M_{t_{6}}\models r$, and there is some
$t^{\prime}\sim_{\mathfrak{s}}t_{6}$ such that for some
$s^{*}\sim_{\mathfrak{e}}s$, $t^{\prime}\in\|s^{*}\|_{9m}$. By the third
clause of Corollary 6.1, for every $n$, for every $v\in
s_{u}R(\mathfrak{s};\ell?;\mathfrak{e};r?)$ there is some
$s^{*}\sim_{\mathfrak{s}}v$ such that $v^{\prime}\in\|s\|_{n}$. Therefore
there is some such $v$ where $v\in\|t_{6}\|_{9m+1}$, and thus there must be
some $t^{*}\sim_{\mathfrak{s}}t_{6}$ where $t^{*}\in\|s^{*}\|_{9m}$. We let
such a $s^{*}$ be $\tau_{n}(i,j)$.

    4. (d)

$M_{t_{7}}\models d$, $M_{t_{8}}\models u$ and there is some
$v\sim_{\mathfrak{s}}t_{8}$ such that $v\in\|s_{\ell}\|_{9m+3}$. Since
$v\sim_{\mathfrak{s}}t_{8}\sim_{\mathfrak{e}}t_{7}\sim_{\mathfrak{s}}t^{*}$,
and $t^{*}\in\|s^{*}\|_{9m}$, there must be some $w\in
s_{\ell}R(u?;\mathfrak{e};d?;\mathfrak{s})$ such that $s^{*}\in\|w\|_{9m}$, as
required for the induction.

The construction is depicted in Figure 6.

$9m+3$$s_{\ell}$$s^{\prime}$$s^{u}$$s^{*}$$t_{1}$$t_{2}$$t_{3}$$t_{4}$$t_{5}$$t_{6}$$t_{7}$$t_{8}$$t^{*}$$t^{\prime}$$t^{u}$$v$$9m+6$$9m+3$$9m$

Figure 6: The constructions for $\tau_{n}$. The curved, dashed lines indicate
$n$-$\Pi$-bisimilarity, where $n$ is indicated below the line.

Therefore, we may assume the existence of the function $\tau_{n}$ for all $n$
and given the set of mappings $\tau_{n}$, we are now able to construct a
tiling for $P^{n}$, for every $n$. For each $n\in\mathbb{N}$ we define a
function $\lambda_{n}:P^{n}\longrightarrow\Gamma$, where for each $(i,j)\in
P^{n}$, $\lambda_{n}(i,j)=\gamma$ where

$M_{\tau_{n}(i,j)}\models K_{\mathfrak{s}}(u\rightarrow\gamma^{u}\land
d\rightarrow\gamma^{d}\land\ell\rightarrow\gamma^{\ell}\land
r\rightarrow\gamma^{r}).$

By the construction of $\tau_{n}$, it follows that the conditions of the
tiling are met. For example, if $\lambda_{n}(i,j)=\gamma$, then
$M_{\tau_{n}(i,j)}\models K_{\mathfrak{s}}(u\rightarrow
K_{\mathfrak{e}}(\gamma^{u}))$. Since there is
$t\in\tau_{n}(i,j)R(\mathfrak{s};u?;\mathfrak{e};d?;\mathfrak{s})$ where
$\tau_{n}(i,j+1)\in\|t\|_{1}$, we have $M_{\tau_{n}(i,j+1)}\models
K_{\mathfrak{s}}(d\rightarrow\gamma^{u})$. This way we can show all the sides
of the tiles in the partial tilings $\lambda_{n}$ match.

We are now able to build a complete tiling
$\lambda:\mathbb{N}\times\mathbb{N}\longrightarrow\Gamma$ by enumerating
$\mathbb{N}\times\mathbb{N}$ as $a_{0},a_{1},...$ where $a_{0}=(0,0)$. We give
an inductive definition of $\lambda$, whereby we suppose that
$\lambda^{n}:\\{a_{0},\ldots,a_{n}\\}\longrightarrow\Gamma$ where
$\lambda^{0}(0,0)=\gamma$ such that

$M_{s}\models K_{\mathfrak{s}}(u\rightarrow\gamma^{u}\land
d\rightarrow\gamma^{d}\land\ell\rightarrow\gamma^{\ell}\land
r\rightarrow\gamma^{r}).$

Our induction is built on the hypothesis that for each $n$ there is an
infinite subset $X^{n}\subseteq\mathbb{N}$ such that for all $x\in X$, for all
$i\leq n$, $\lambda_{x}(a_{i})=\lambda^{n}(a_{i})$. This is clearly true for
$n=0$, where $X^{0}=\mathbb{N}$. Given the hypothesis holds for $n-1$, we set
$\lambda^{n}(a_{i})=\lambda^{n-1}(a_{i})$ for all $i<n$. Now for each $x\in
X^{n-1}$, $\lambda_{x}(a_{n})$ may be a tile of $\Gamma$, or may be undefined.
However, if $a_{n}=(i,j)$, $\lambda_{x}(a_{n})$ may only be undefined if
$x<i+j$. As there can only be a finite number of such cases, and $X^{n-1}$ is
infinite, it follows that, $\lambda_{x}(a_{n})\in\Gamma$ for infinitely many
$x$. As $\Gamma$ is a finite set, there must be some $\gamma\in\Gamma$ such
that $\lambda_{x}(a_{n})=\gamma$ for all $x\in X^{\prime}$ where $X^{\prime}$
is an infinite subset of $X^{n-1}$. We let $\lambda^{n}(a_{n})=\gamma$ and
$X^{n}=X^{\prime}$, and the induction hypothesis holds.

As $\lambda^{n}$ is a monotonically increasing function it has a well-defined
limit: $\lambda(i,j)=\gamma$ where for some $x\in\mathbb{N}$,
$\lambda^{x}(i,j)=\gamma$. As the sides of the tiles all match, this is
sufficient to show that $\Gamma$ can tile the plane.

For the converse direction we are able to give a more direct proof.

######  Lemma 6.5.

Suppose that $\Gamma$ can tile the plane. Then there is some model $M=(S,R,V)$
and some state $s\in S$ such that

  1. 1.

$M_{s}\models_{APAL}SAT_{\Gamma}\land CB_{apa}\land{\heartsuit}$

  2. 2.

$M_{s}\models_{GAL}SAT_{\Gamma}\land CB_{ga}\land{\heartsuit}$

  3. 3.

$M_{s}\models_{CAL}SAT_{\Gamma}\land CB_{ca}\land{\heartsuit}$

######  Proof 6.6.

Suppose that $\Gamma$ can tile the plane via the function
$\lambda:\mathbb{N}\times\mathbb{N}\longrightarrow\Gamma$. We build the model
$M=(S,R,V)$ where:

  * •

$S=\mathbb{N}\times\mathbb{N}\times\\{u,d,\ell,r,mid\\}$, so the state
$(i,j,k)$ represents the $k$ side of the tile at the square $(i,j)$, where
$k=mid$ represents the center of the tile.

  * •

$R_{\mathfrak{s}}=\\{((i,j,k),(i^{\prime},j^{\prime},k^{\prime}))\ |\
i=i^{\prime}\ \text{and}\ j=j^{\prime}\\}$

  * •

$(i,j,u)R_{\mathfrak{e}}=\\{(i,j,u),(i,j+1,d)\\}$

  * •

$(i,j,d)R_{\mathfrak{e}}=\\{(i,j,d),(i,j-1,u)\\}$ or $\\{(i,j,d)\\}$ if $j=0$.

  * •

$(i,j,\ell)R_{\mathfrak{e}}=\\{(i,j,\ell),(i-1,j,r)\\}$ of $\\{(i,j,\ell)\\}$
if $i=0$.

  * •

$(i,j,r)R_{\mathfrak{e}}=\\{(i,j,r),(i+1,j,\ell)\\}$

  * •

$(i,j,mid)R_{\mathfrak{e}}=\\{(i^{\prime},j^{\prime},mid)\
|(i^{\prime},j^{\prime})\in\mathbb{N}\times\mathbb{N}\\}$

  * •

for all colours $c\in C$, $V(c)=\\{(i,j,k)\ |\ \lambda(i,j)^{k}=c\\}$ (We
assume that $\lambda(i,j)^{mid}$ is always a fixed colour, say white.)

  * •

for all directions $k\in\\{u,d,\ell,r\\}$, $V(k)=\\{(i,j,k^{\prime})\ |\
k^{\prime}=k\\}$.

  * •

$V({\heartsuit})=\\{(i,j,mid)\ |\ i\textrm{ is even, and }j\textrm{ is
even}\\}$

  * •

$V({\clubsuit})=\\{(i,j,mid)\ |\ i\textrm{ is odd, and }j\textrm{ is even}\\}$

  * •

$V({\diamondsuit})=\\{(i,j,mid)\ |\ i\textrm{ is odd, and }j\textrm{ is
odd}\\}$

  * •

$V({\spadesuit})=\\{(i,j,mid)\ |\ i\textrm{ is even, and }j\textrm{ is
odd}\\}$

$\gamma_{2}^{u}$$\gamma_{7}$$\gamma_{4}$$\gamma_{1}$$\gamma_{2}$$\gamma_{3}$$\gamma_{5}$$\gamma_{6}$$\gamma_{8}$$\gamma_{9}$${\clubsuit}$${\diamondsuit}$${\spadesuit}$${\heartsuit}$${\heartsuit}$$\gamma_{1}^{d}$$\gamma_{1}^{\ell}$$\gamma_{1}^{u}$${\heartsuit}$$\gamma_{1}^{r}$$\gamma_{2}^{\ell}$$\gamma_{2}^{d}$$\gamma_{3}^{d}$$\gamma_{3}^{u}$$\gamma_{3}^{r}$$\gamma_{4}^{d}$$\gamma_{4}^{\ell}$$\gamma_{4}^{u}$$\gamma_{5}^{u}$$\gamma_{5}^{d}$$\gamma_{5}^{r}$$\gamma_{4}^{r}$$\gamma_{5}^{\ell}$$\gamma_{8}^{u}$$\gamma_{7}^{d}$$\gamma_{7}^{u}$$\gamma_{8}^{d}$$\gamma_{8}^{r}$$\gamma_{6}^{u}$$\gamma_{6}^{d}$$\gamma_{6}^{r}$$\gamma_{9}^{d}$$\gamma_{9}^{u}$$\gamma_{9}^{\ell}$$\gamma_{9}^{r}$$\gamma_{7}^{r}$${\heartsuit}$$\gamma_{7}^{\ell}$$\gamma_{2}^{r}$$\gamma_{3}^{\ell}$$\gamma_{6}^{\ell}$${\clubsuit}$${\clubsuit}$$\gamma_{8}^{\ell}$

Figure 7: A representation of the construction used for Lemma 6.5. The edge
relations between the centers of all squares have been omitted for clarity.

This construction is presented in Figure 7, and realizes the construction
presented in Figure 4. We can now confirm that the constructed model satisfies
the necessary formulas. Let $s=(0,0,m)$. Then

  1. 1.

$M_{s}\models oneCol$ (1). Since the $edge$-relation links the centers of all
squares, and every world belongs to a square, this requires every world $t\in
S$ to satisfy a unique colour atom $c\in C$. This is guaranteed by the
definition of $V(c)$.

  2. 2.

$M_{s}\models tile_{\Gamma}$ (2). Since the $\mathfrak{e}$-relation links the
centers of all squares this requires that at the center of every square, the
formula (2) requires that for every square, there is some tile $\gamma$ such
that any state labelled by the direction $k$ in that square satisfies the
colour proposition $\gamma^{k}$. As the square relations relates worlds
$(i,j,k)$ and $(i^{\prime},j^{\prime},k^{\prime})$ where $i=i^{\prime}$ and
$j=j^{\prime}$, worlds in the same square correspond to to the same tile
$\lambda(i,j)$ and are coloured accordingly.

  3. 3.

$M_{s}\models match$ (3). The $\mathfrak{e}$-relation connects the centers of
all squares, so (3) requires that at every world in every square, the edge
agent knows the colour. Let the given world be $t=(i,j,k)$. There are five
cases to consider:

    1. (a)

If the world is a center world (i.e. $k=mid$) then it must be coloured white.
As all center worlds are connected by $\mathfrak{e}$ only to center worlds, at
a center world, the edge agent knows the colour is white.

    2. (b)

If the world is a right world ($k=r$), then its colour is $\lambda(i,j)^{r}$.
As $tR_{\mathfrak{e}}=\\{(i,j,r),(i+1,j,\ell)\\}$ we have for all
$t^{\prime}\in tR_{\mathfrak{e}}$, the colour of $t^{\prime}$ is either
$\lambda(i,j)^{r}$ or $\lambda(i+1,j,\ell)$. From Definition 3.1 it follows
that $\lambda(i,j)^{r}=\lambda(i+1,j)^{\ell}$, so the colour is known to agent
$\mathfrak{e}$.

    3. (c)

Similar arguments can be given where $k=\ell,\ u,$ or $d$. In the case
$k=\ell$ and $i=0$, or $k=d$ and $j=0$, we note that $tR_{\mathfrak{e}}$ is a
singleton so the result follows trivially.

  4. 4.

$M_{s}\models SAT_{\Gamma}$ (4). This follows from the previous three cases.

  5. 5.

$M_{s}\models K_{\mathfrak{e}}K_{\mathfrak{s}}local$ (22). As $local$ is a
purely epistemic formula, it is straightforward to check that all the required
properties are satisfied by $M_{s}$.

  6. 6.

$M_{s}\models K_{\mathfrak{e}}K_{\mathfrak{s}}cyc_{apa}$ (23). Suppose
$t=(i,j,mid)\in S$ and $M_{t}\models{\heartsuit}$. After every possible
announcement, $\psi$, that can be made there are two possibilities. If
$t_{0}=t$, $t_{1}=(i,j,r)$, $t_{2}=(i+1,j,\ell)$, $t_{3}=(i+1,j,u)$,
$t_{4}=(i+1,j+1,d)$, $t_{5}=(i+1,j+1,\ell)$, $t_{6}=(i,j+1,r)$,
$t_{7}=(i,j+1,d)$, and $t_{8}=(i,j,u)$ all remain in $S^{\psi}$, in which case
$\\{t_{1}\\}=V(r)\cap t_{0}R_{\mathfrak{s}}$, $\\{t_{2}\\}=V(\ell)\cap
t_{1}R_{\mathfrak{e}}$, $\\{t_{3}\\}=V(u)\cap t_{2}R_{\mathfrak{s}}$,
$\\{t_{4}\\}=V(d)\cap t_{3}R_{\mathfrak{e}}$, $\\{t_{5}\\}=V(\ell)\cap
t_{4}R_{\mathfrak{s}}$, $\\{t_{6}\\}=V(r)\cap t_{5}R_{\mathfrak{e}}$,
$\\{t_{7}\\}=V(d)\cap t_{6}R_{\mathfrak{s}}$, $\\{t_{8}\\}=V(u)\cap
t_{7}R_{\mathfrak{e}}$ and $t\in t_{8}R_{\mathfrak{s}}$. Alternatively one of
the worlds $t_{0},\ldots,t_{8}$ does not remain in $S^{\psi}$, so one of
$V(r)\cap t_{0}R^{\psi}_{\mathfrak{s}}$, $V(\ell)\cap
t_{1}R^{\psi}_{\mathfrak{e}}$, $V(u)\cap t_{2}R^{\psi}_{\mathfrak{s}}$,
$V(d)\cap t_{3}R^{\psi}_{\mathfrak{e}}$, $V(\ell)\cap
t_{4}R^{\psi}_{\mathfrak{s}}$, $V(r)\cap t_{5}R^{\psi}_{\mathfrak{e}}$,
$V(d)\cap t_{6}R^{\psi}_{\mathfrak{s}}$, $V(u)\cap
t_{7}R^{\psi}_{\mathfrak{e}}$ or $t_{8}R^{\psi}_{\mathfrak{s}}$ is empty. In
either case we have

$\begin{array}[]{l}M^{\psi}_{t}\models K_{\mathfrak{s}}(r\rightarrow
K_{\mathfrak{e}}(\ell\rightarrow K_{\mathfrak{s}}(u\rightarrow
K_{\mathfrak{e}}(d\rightarrow K_{\mathfrak{s}}(\ell\rightarrow\\\ \hfill
K_{\mathfrak{e}}(r\rightarrow K_{\mathfrak{s}}(d\rightarrow
K_{\mathfrak{e}}(u\rightarrow\widehat{K}_{\mathfrak{s}}{\heartsuit})))))))).\end{array}$

Similar arguments can be given for the other suits, so it follows that for all
$t\in S$, $M_{t}\models cyc_{apa}$.

  7. 7.

$M_{t}\models ck_{apa}$ (23). Suppose $t=(i,j,mid)\in S$ and
$M_{t}\models{\heartsuit}$. Suppose that there is some announcement $\psi$
such that for $t^{\prime}\in V({\clubsuit})$, $t^{\prime}\notin
tR^{\psi}_{\mathfrak{e}}$. As $v=(i+1,j,mid)\sim_{\mathfrak{e}}t$, and $v\in
V({\clubsuit})$, we must have $v\notin S^{\psi}$. Therefore if $t_{0}=t$,
$t_{1}=(i,j,r)$, and $t_{2}=(i+1,j,\ell)$ remain in $S^{\psi}$ then, by the
same reasoning as in the previous case, we will have $M^{\psi}_{t}\models
K_{\mathfrak{s}}(r\rightarrow K_{\mathfrak{e}}(\ell\rightarrow
K_{\mathfrak{s}}\neg{\clubsuit}))$. If any of the worlds $t_{0},\ t_{1}$, or
$t_{2}$ do not remain in $S^{\psi}$ then the formula is vacuously true.
Similar arguments can be given for the other suits, so for all $t\in S$,
$M_{t}\models ck_{apa}$.

  8. 8.

$M_{s}\models K_{\mathfrak{e}}K_{\mathfrak{s}}cyc_{ga}$ (25). Suppose that
$M_{t}\models{\heartsuit}$. Suppose that $\psi$ is some announcement that is
known to agent $\Box$ at $t$. Let $t_{0}=t$, $t_{1}=(i,j,r)$,
$t_{2}=(i+1,j,\ell)$, $t_{3}=(i+1,j,u)$, $t_{4}=(i+1,j+1,d)$,
$t_{5}=(i+1,j+1,\ell)$, $t_{6}=(i,j+1,r)$, $t_{7}=(i,j+1,d)$, and
$t_{8}=(i,j,u)$. As agent-$\mathfrak{s}$ knows $\psi$, but cannot distinguish
$t$ from $t_{1}$ and $t_{8}$, it follows that $t_{0},\ t_{1}$ and $t_{8}$
remain in $S^{\psi}$. Regardless of whether the other states also remain in
$S^{\psi}$, we have $M_{t}\models cyc_{ga}$ in much that same way that
$M_{t}\models cyc_{apa}$.

  9. 9.

$M_{s}\models K_{\mathfrak{e}}K_{\mathfrak{s}}ck_{ga}$ (25). Suppose that
$t=(i,j,mid)$ and $M_{t}\models{\heartsuit}$. As agent $\mathfrak{e}$ cannot
distinguish any of the worlds $(i^{\prime},j^{\prime},mid)$ from $t$, any
announcement $\psi$ that is known to agent $\mathfrak{e}$ must preserve all of
those worlds. Therefore after making such an announcement, regardless of
whether $(i,j,r)$ and $(i+1,j,\ell)$ remain, we have $M^{\psi}_{t}\models
K_{\mathfrak{s}}(\ell\rightarrow
K_{\mathfrak{e}}(r\rightarrow\widehat{K}_{\mathfrak{s}}{\clubsuit}$. Similar
arguments can be given for other directions and suits so we have $M_{t}\models
ck_{ga}$.

  10. 10.

$M_{s}\models K_{\mathfrak{e}}K_{\mathfrak{s}}cyc_{ca}$ (26). Suppose that
$M_{t}\models{\heartsuit}$. Suppose that $\psi$ is a conjunction of
announcements that are known to agents $\Box$ or $\mathfrak{e}$ at $t$. Let
$t_{0}=t$, $t_{1}=(i,j,r)$, $t_{2}=(i+1,j,\ell)$, $t_{3}=(i+1,j,u)$,
$t_{4}=(i+1,j+1,d)$, $t_{5}=(i+1,j+1,\ell)$, $t_{6}=(i,j+1,r)$,
$t_{7}=(i,j+1,d)$, and $t_{8}=(i,j,u)$. As the announcement of $\psi$ can only
possibly remove these worlds, it follows that $M_{t}\models cyc_{ca}$, in the
same way that $M_{t}\models cyc_{apa}$.

  11. 11.

$M_{s}\models K_{\mathfrak{e}}K_{\mathfrak{s}}ck_{ca}$ (26). Suppose that
$t=(i,j,mid)$ and $M_{t}\models{\heartsuit}$. Let $\psi$ be an conjunction of
announcements that are known to either agent $\mathfrak{s}$ or agent
$\mathfrak{e}$. If $S^{\psi}\cap V({\clubsuit})$ is empty, then
$t^{\prime}=(i+1,j,mid)\notin S^{\psi}$. Therefore,
$tR^{\psi}(\mathfrak{s};r?;\mathfrak{e};\ell;\mathfrak{s};{\clubsuit}?)$ is
empty, so $M^{\psi}_{t}\models K_{\mathfrak{s}}(r\rightarrow
K_{\mathfrak{e}}(\ell\rightarrow K_{\mathfrak{s}}\neg{\clubsuit}))$. Similar
arguments can be given for other directions and suits so the result follows.

As we have show that $M_{s}$ satisfies all the necessary sub-formulas, the
result follows.

######  Theorem 6.7.

The satisfiability problem for APAL, GAL and CAL is undecidable, provided that
there is more than one agent in the system. In the case of a single agent, all
logics are decidable.

######  Proof 6.8.

Lemmas 6.3 and 6.5 show that the satisfiability problems for APAL, GAL, and
CAL are equivalent to an undecidable tiling problem and therefore are not
recursively enumerable. The single agent case is given as Proposition 18 of
[6] (the arbitrary announcement operator is then definable, so that the logic
is equally expressive as the base epistemic logic), and the single agent
fragments of GAL and CAL can be shown similarly.

##  7 Future work

The previous sections give an essentially negative result: we are unable to
determine the satisfiability of formulas in APAL, GAL, and CAL. However, the
core purposes of these logics are to determine what agents can achieve by
sharing knowledge, and this is still a question of great interest. The
undecidability proof given here does not use an intrinsic property of
knowledge sharing, but rather exploits the power of quantifying over language.
With this in mind, we consider the question of what other logics could
successfully reason about knowledge sharing agents. We list some of the
possible answers below:

  * •

In the logics presented in this paper we assumed that accessibility relations
are equivalence relations, and correspondingly we quantify over knowledge
formulas, not over beliefs. Related to this, the quantifications are over
truthful announcements, and not over announcements that are merely believed to
be true, but that may be mistaken or even intentionally false (as in lies).
The logics presented in this paper can be straightforwardly generalized to
such scenarios, by the dual strategy of $(i)$ considering arbitrary
accessibility relations (or, for example KD45 accessibility relations, for
modelling consistent beliefs), and $(ii)$ not using the standard model
restriction semantics of public announcements, but the ‘arrow restriction’
(accessibility relation restricting) semantics for public announcements of
[18].

  * •

One approach could be to consider generalizations of announcements as the
medium of informative updates. By replacing the public announcements in
arbitrary public announcement logic with refinements [31, 12] it is possible
to define a decidable logic that may be used to reason about the
quantification of all informative updates (and not merely public updates:
announcements). This logic is called refinement modal logic (RML). The
essential difference between APAL and RML is, that while APAL has an operator
that quantifies over all public announcements, RML has an operator that
quantifies over all refinements. Recent work [19] presents a logic that
quantifies over event models [7], and it is shown there that this so-called
arbitrary action model logic is equally expressive as refinement modal logic.
One can in fact synthesize an action model from the formula supposedly true
after a refinement. Hales’ approach can clearly be adapted to quantify over
group event models, and this would be a valuable generalization of group
announcement logic. Like RML, such a logic would then be decidable.

  * •

A way towards a decidable arbitrary public announcement logic may be to only
allow quantification over positive formulas. In a positive formula all $K_{a}$
operators are in the scope of an even number of negations. The positive
formulas are also known as the universal fragment. This means agents may
announce what they know, and what they know other agents know, and so on.
However, they may not announce what they don’t know, or what they know other
agents don’t know. The appealing thing about these announcements is that once
they are made, they will always remain true, so they have a monotonic nature.
This suggests that a logic of arbitrary (or group) positive announcements may
be more computationally amenable than GAL. However, there may well be various
other roads leading to a decidable arbitrary public announcement logic. For
example, only to quantify over formulas that have a restricted epistemic
(modal) depth, or variations of first-order epistemic logics with explicit
quantifiers as in [8]. Yet another way to decidability is to consider
arbitrary announcements on specific domains, as in the recent [13].

## References

  * [1] T. Ågotnes.  Action and knowledge in alternating-time temporal logic.  Synthese (Special Section on Knowledge, Rationality and Action), 149(2):377–409, 2006.
  * [2] T. Ågotnes, P. Balbiani, H. van Ditmarsch, and P. Seban.  Group announcement logic.  Journal of Applied Logic, 8:62–81, 2010.
  * [3] T. Ågotnes and H. van Ditmarsch.  Coalitions and announcements.  In Proc. of 7th AAMAS, pages 673–680. IFAAMAS, 2008.
  * [4] T. Ågotnes, H. van Ditmarsch, and T. French.  The undecidability of group announcements.  In Proc. of the 13th AAMAS, pages 893–900, 2014.
  * [5] R. Alur, T. A. Henzinger, and O. Kupferman.  Alternating-time temporal logic.  Journal of the ACM, 49:672–713, 2002.
  * [6] P. Balbiani, A. Baltag, H. van Ditmarsch, A. Herzig, T. Hoshi, and T. D. Lima.  ‘Knowable’ as ‘known after an announcement’.  Review of Symbolic Logic, 1(3):305–334, 2008.
  * [7] A. Baltag, L. 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.
  * [8] F. Belardinelli and W. van der Hoek.  Epistemic quantified boolean logic: Expressiveness and completeness results.  In Q. Yang and M. Wooldridge, editors, Proceedings of 24th IJCAI, pages 2748–2754. AAAI Press, 2015.
  * [9] R. Berger.  The undecidability of the domino problem.  Number 66 in Memoirs of the American Mathematical Society. American Mathematical Soc., 1966.
  * [10] T. Bolander and M. Andersen.  Epistemic planning for single and multi-agent systems.  Journal of Applied Non-classical Logics, 21(1):9–34, 2011.
  * [11] T. Bolander, M. Jensen, and F. Schwarzentruber.  Complexity results in epistemic planning.  In Q. Yang and M. Wooldridge, editors, Proceedings of 24th IJCAI, pages 2791–2797. AAAI Press, 2015.
  * [12] L. Bozzelli, H. van Ditmarsch, T. French, J. Hales, and S. Pinchinat.  Refinement modal logic.  Information and Computation, 239:303–339, 2014.
  * [13] T. Charrier and F. Schwarzentruber.  Arbitrary public announcement logic with mental programs.  In G. Weiss, P. Yolum, R. Bordini, and E. Elkind, editors, Proceedings of AAMAS, pages 1471–1479. ACM, 2015.
  * [14] A. Cordón-Franco, H. van Ditmarsch, D. Fernández-Duque, and F. Soler-Toscano.  A colouring protocol for the generalized russian cards problem.  Theor. Comput. Sci., 495:81–95, 2013.
  * [15] R. Fagin, J. Halpern, Y. Moses, and M. Vardi.  Reasoning about Knowledge.  MIT Press, Cambridge MA, 1995.
  * [16] M. Fischer and R. Ladner.  Propositional dynamic logic of regular programs.  Journal of Computer and System Sciences, 18(2):194–211, 1979.
  * [17] T. French and H. van Ditmarsch.  Undecidability for arbitrary public announcement logic.  In C. Areces and R. Goldblatt, editors, Advances in Modal Logic 7, pages 23–42, London, 2008. College Publications.
  * [18] J. Gerbrandy.  Bisimulations on Planet Kripke.  PhD thesis, University of Amsterdam, 1999.  ILLC Dissertation Series DS-1999-01.
  * [19] J. Hales.  Arbitrary action model logic and action model synthesis.  In Proc. of 28th LICS, pages 253–262. IEEE, 2013.
  * [20] D. Harel.  Effective transformations on infinite trees, with applications to high undecidability, dominoes, and fairness.  J. ACM, 33(1):224–248, 1986.
  * [21] C. Lutz.  Complexity and succinctness of public announcement logic.  In Proc. of the 5th AAMAS, pages 137–144, 2006.
  * [22] J. Miller and L. Moss.  The undecidability of iterated modal relativization.  Studia Logica, 79(3):373–407, 2005.
  * [23] M. Pauly.  A modal logic for coalitional power in games.  Journal of Logic and Computation, 12(1):149–166, 2002.
  * [24] J. Plaza.  Logics of public communications.  In Proc. of the 4th ISMIS, pages 201–216. Oak Ridge National Laboratory, 1989.
  * [25] J. van Benthem.  Correspondence theory.  Springer, 1984.
  * [26] J. van Benthem.  Logics for information update.  In J. van Benthem, editor, Proc. of TARK VIII, pages 51–88, Los Altos, 2001. Morgan Kaufmann.
  * [27] J. van Benthem.  One is a lonely number: on the logic of communication.  In Logic colloquium 2002. Lecture Notes in Logic, Vol. 27, pages 96–129. A.K. Peters, 2006.
  * [28] J. van Benthem.  Logic in Games.  MIT Press, 2014.
  * [29] W. van der Hoek and M. Wooldridge.  Tractable multiagent planning for epistemic goals.  In Proc. of the First International Joint Conference on Autonomous Agents & Multiagent Systems (AAMAS 2002), pages 1167–1174. ACM, 2002.
  * [30] H. van Ditmarsch.  Quantifying notes.  In Proc. of 19th WoLLIC, LNCS 7456, pages 89–109. Springer, 2012\.