some fixed number $\ell\geq 0$ of iterations of the loop and corresponds to a
path $n\to[n,\ell,j]\to j$ in $M^{\prime\prime}$ which has the same
probability, reward and duration. Note in particular that the probability of a
path $n\to\cdots\to n\to j$ that iterates the loop exactly $\ell$ times and
then goes to $j$ is
$\mathop{p}\nolimits(n,n)^{\ell}(1-\mathop{p}\nolimits(n,n))\cdot\frac{\mathop{p}\nolimits(n,j)}{1-\mathop{p}\nolimits(n,n)}=\mathop{p}\nolimits^{\prime\prime}(n,[n,\ell,j])$.
One thus readily verifies that $M^{\prime\prime}$ is a summary of $M$ in the
sense of Definition A.3.

It remains to observe that $M^{\prime}$ is a summary of $M^{\prime\prime}$.
This is because it is the result of removing intermediate states via Lemma
A.5. We conclude that $M^{\prime}$ is a summary of $M$. The claim of the lemma
now follows from Lemma A.4. ∎

##  Appendix B Proofs for Section 6

See 6.2 In this section, we show how to find the outcome of an induced Markov
chain for a specific player in state 1 in the first order theory over the
reals. The problem, in particular, is that depending on which strategy profile
we picked, the induced Markov chain could have different (end) strongly
connected components and we need the formula to be the same no matter which
strategy profile we picked. Still, our solution is to implement loop and state
elimination, see Section 5, while taking care that some of these steps might
not be possible to do (for example, you cannot do state elimination of a state
that is absorbing with incoming edges or if it has already been eliminated,
and you cannot do loop elimination on a state if there is no other successor
of the state or if it has been eliminated).

For each pair of (1) memory vectors ${\bf m}$ and ${\bf m^{\prime}}$, (2) game
states $v$ and $v^{\prime}$ and (3) signal vectors ${\bf s}$ and ${\bf
s^{\prime}}$ and for each iteration $i$ (an iteration consists of either one
loop or one state elimination step), we have variables corresponding to the
(possible) state $(v,m,s)$ and edge
$((v,m,s),(v^{\prime},m^{\prime},s^{\prime}))$ of the induced Markov chain,
describing the Markov chain at the beginning of iteration $i$. For simplicity,
we will talk about $(v,m,s)$ as being a state of the Markov chain. Therefore,
there are at most $N$ states and we only need to assign value to the states of
the Markov chain initially.

To be explicit about it, we first run a loop and then state elimination on
state $x$ for each $x\in\\{N,N-1,\dots,1\\}$, except we do not do state
elimination on state $1$. In other words, for each $1\leq j<2N$, in iteration
$j$ for odd $j$, we do loop elimination on state $N+1-(j+1)/2$ and in
iteration $j$ for even $j$, we do state elimination on state $N+1-j/2$.

Specifically, we have variables, each describing the Markov chain at the start
of iteration $j$. Let $S=(v,{\bf m},{\bf s})$ and $T=(v^{\prime},{\bf
m^{\prime}},{\bf s^{\prime}})$. The intention of them is as follows:

  1. (1)

$x_{S,j}$ should be 1 if state $s$ exists and otherwise 0.

  2. (2)

$x_{S,T,j}$ should be 1 if action $(S,T)$ exists and otherwise 0.

  3. (3)

$q_{S,T,j}$ should be the probability to use action $(S,T)$ when in $S$.

  4. (4)

$n_{S,T,j}$ should be the duration of action $(S,T)$.

  5. (5)

$r_{S,T,j}$ should be the reward of action $(S,T)$ for the specific player.

We have some expressions (i.e. some boolean combinations of polynomials)
giving the value of each of these variables at the start of iteration 1 and
depending on the value of the variables at the start of a loop or state
elimination iteration, we have expressions giving the value of each of these
variables after that iteration. The conjunction of all of these expressions
give the full formula describing the outcome of the game for the specific
player.

##### Setting the initial values of the variables

Note that expressions such as

$\sum_{{\bf a}=(a_{1},\dots,a_{k})\mid\Delta(v,{\bf
a})(*,s^{\prime},v^{\prime})>0}\prod_{i=1}^{k}q_{a_{i}}^{s_{i},m_{i},i}b_{m^{\prime}_{i}}^{s_{i}^{\prime},m_{i},i}$

are explicit polynomials given the game and states $(v,m,s)$ and
$(v^{\prime},m^{\prime},s^{\prime})$ explicitly because the set of such $a$’s
comes directly from the input game ($\Delta(v,a)(*,s^{\prime},v^{\prime})$ is
the probability to go from $v$ to $v^{\prime}$ when the players plays $a$,
emitting signals $s^{\prime}$, ignoring the reward) and for a given $a$ the
product is explicit. The expressions at the beginning, i.e. for iteration 1,
are as follows:

  1. (1)

The expression for $x_{(v,{\bf m},{\bf s}),1}$ is

$x_{(v,{\bf m},{\bf s}),1}=1$

(one could omit these variables, but including them makes it easier to
follow). That is, initially, all states exists.

  2. (2)

The expression for $x_{(v,{\bf m},{\bf s}),(v^{\prime},{\bf m^{\prime}},{\bf
s^{\prime}}),1}$, for ${\bf m}=(m_{1},m_{2},\dots,m_{k})$, ${\bf
s}=(s_{1},s_{2},\dots,s_{k})$, ${\bf
m^{\prime}}=(m_{1}^{\prime},m_{2}^{\prime},\dots,m_{k}^{\prime})$ and ${\bf
s^{\prime}}=(s_{1}^{\prime},s_{2}^{\prime},\dots,s_{k}^{\prime})$ is

$\displaystyle(x_{(v,{\bf m},{\bf s}),(v^{\prime},{\bf m^{\prime}},{\bf
s^{\prime}}),1}=1$
$\displaystyle\wedge\sum_{a=(a_{1},\dots,a_{k})\mid\Delta(v,a)(*,s^{\prime},v^{\prime})>0}\prod_{i=1}^{k}q_{a_{i}}^{s_{i},m_{i}}\cdot
b_{m^{\prime}_{i}}^{s_{i}^{\prime},m_{i},i}>0)$ $\displaystyle\vee(x_{(v,{\bf
m},{\bf m}),(v^{\prime},{\bf m^{\prime}},{\bf s^{\prime}}),1}=0$
$\displaystyle\wedge\sum_{a=(a_{1},\dots,a_{k})\mid\Delta(v,a)(*,s^{\prime},v^{\prime})>0}\prod_{i=1}^{k}q_{a_{i}}^{s_{i},m_{i},i}\cdot
b_{m^{\prime}_{i}}^{s_{i}^{\prime},m_{i},i}=0)$

In words, the expression sets
$x_{(v,m,s),(v^{\prime},m^{\prime},s^{\prime}),1}$ to 1 iff there is an action
$a$ that happens with positive probability which has $v^{\prime}$ while
emitting ${\bf s^{\prime}}$ as an outcome, and the probability to update from
${\bf m}$ to ${\bf m^{\prime}}$ on signal ${\bf s}$ (i.e. for each player, the
probability to update from $m_{i}$ to $m_{i}^{\prime}$ on signal $s_{i}$) is
also positive.

  3. (3)

The expression for $q_{(v,{\bf m},{\bf s}),(v^{\prime},{\bf m^{\prime}},{\bf
s^{\prime}}),1}$ is

$q_{(v,{\bf m},{\bf s}),(v^{\prime},{\bf m^{\prime}},{\bf
s^{\prime}}),1}=\sum_{a=(a_{1},\dots,a_{k})\mid\Delta(v,a)(*,{\bf
s^{\prime}},v^{\prime})>0}\prod_{i=1}^{k}q_{a_{i}}^{s_{i},m_{i},i}\cdot
b_{m^{\prime}_{i}}^{s_{i}^{\prime},m_{i},i}\cdot\Delta(v,a)(*,s^{\prime},v^{\prime})\enspace.$

In words, the expression $\prod_{i=1}^{k}q_{a_{i}}^{s_{i},m_{i},i}$ is the
probability of using action profile $a$ when the signals and memory were ${\bf
s}$ and ${\bf m}$ respectively. That multiplied by
$\prod_{i=1}^{k}b_{m^{\prime}_{i}}^{s_{i},m_{i},a,i}$ is then the probability
to update ${\bf m}$ to ${\bf m^{\prime}}$ as well, on signal ${\bf s}$.
Finally, that times $\Delta(v,a)(*,s^{\prime},v^{\prime})$ is then the
probability to go to $v^{\prime}$, and emitting signal ${\bf s^{\prime}}$ to
the players, when in $v$ with the signal being $s$, and the players used
action $a$. The full expression is then summing over all possible action
profiles $a$.

  4. (4)

The expression for $n_{(v,{\bf m},{\bf s}),(v^{\prime},{\bf m^{\prime}},{\bf
s^{\prime}}),1}$ is

$n_{(v,{\bf m},{\bf s}),(v^{\prime},{\bf m^{\prime}},{\bf
s^{\prime}}),1}=1\enspace.$

I.e. the length of the edge initially is 1.

  5. (5)

The expression for $r_{(v,{\bf m},{\bf s}),(v^{\prime},{\bf m^{\prime}},{\bf
s}),1}$ is

$r_{(v,{\bf m},{\bf s}),(v^{\prime},{\bf m^{\prime}},{\bf
s^{\prime}}),1}q_{(v,{\bf m},{\bf s}),(v^{\prime},{\bf m^{\prime}},{\bf
s^{\prime}}),1}=\sum_{r\mid r\text{ is a reward for the selected
player}}\sum_{a=(a_{1},\dots,a_{n})\mid\Delta(v,a)(r,{\bf
s^{\prime}},v^{\prime})>0}\prod_{i=1}^{k}q_{a_{i}}^{s_{i},m_{i},i}b_{m_{i}^{\prime}}^{s_{i}^{\prime},m_{i},i}\Delta(v,a)(r,{\bf
m^{\prime}},{\bf s^{\prime}})r\enspace.$

In words,
$\prod_{i=1}^{k}q_{a_{i}}^{s_{i},m_{i},i}b_{m_{i}^{\prime}}^{s_{i}^{\prime},m_{i},i}\Delta(v,a)(r,{\bf
m^{\prime}},s^{\prime})$ expresses the probability that, when in state $v$ and
emitting signal ${\bf s}$ and the players have memory ${\bf m}$, we go to
$v^{\prime}$ emitting $s^{\prime}$ and the players update memory to ${\bf
m^{\prime}}$, while the players used joint action $a$ and the specific player
we focus on gets reward $r$. We then sum over all possible $r$’s and $a$’s to
get the expected reward. The reason we have $r_{(v,{\bf m},{\bf
s}),(v^{\prime},{\bf m^{\prime}},{\bf s^{\prime}}),1}q_{(v,{\bf m},{\bf
s}),(v^{\prime},{\bf m^{\prime}},{\bf s^{\prime}}),1}$ on the left-hand side
is that rewards in a Markov chain for an edge are conditional on following
that edge (it is perhaps easiest to understand using an example: If the game
has only a single action $a$, memory $m$ and signal $s$ for each player in
every state and we have that $\Delta(v,a)$, for some state $v$, is the uniform
distribution over $(1,s,t)$ and $(1,s,u)$ for some states $t,u$, then the
right hand side of the expression for going from $v$ to $t$ is $1/2$ because
$\Delta(v,a)(1,s,t)=1/2$ and each other variable in it is 1 (or 0). But
clearly, the reward for going from $v$ to $t$ should be 1, because that is the
reward for each action in the game!).

For simplicity, in the remainder, we write $S$ for $(v,{\bf m},{\bf s})$ and
$T$ for $(v^{\prime},{\bf m^{\prime}},{\bf s^{\prime}})$, because these are
the states of the Markov chain.

We will next give the expressions for each variable and each $1<j<2N$,
depending on whether $j$ is odd or even (i.e. depending on whether we are
doing loop or state elimination).

##### Loop elimination

For even $j$ (i.e. we are doing loop elimination from $j-1$ to $j$ on some
state $v=N+1-j/2$), we use the following expressions:

  1. (1)

The expression for $x_{S,j}$ is

$x_{S,j}=x_{S,j-1}\enspace.$

In words, each state exists if it did before.

  2. (2)

The expression for $x_{v,v,j}$ is

$(x_{v,v,j}=0\wedge\sum_{S\mid S\neq
v}x_{v,s,j-1}>0)\vee(x_{v,v,j}=1\wedge\sum_{S\mid S\neq
v}x_{v,s,j-1}=0)\enspace.$

In words, the loop $(v,v)$ should not exist after this iteration if $v$ has
another successor (the sum $\sum_{S\mid S\neq v}x_{v,S,j-1}$ is 0 precisely if
for all $S\neq v$, $(v,S)$ does not exist). We can not eliminate a loop if the
state does not have another successor though.

For each $S,T$, except $S=T=v$, the expression for $x_{S,T,j}$ is

$x_{S,T,j}=x_{S,T,j-1}\enspace.$

In words, the edge is still there if it was before.

  3. (3)

The expression for $q_{v,S,j}$, for each $S\neq v$ is

$\displaystyle(x_{v,v,j-1}$ $\displaystyle=1\wedge x_{v,v,j}=0\wedge
q_{v,S,j}(1-q_{v,v,j-1})=q_{v,S,j-1})\vee$ $\displaystyle(x_{v,v,j-1}$
$\displaystyle=0\wedge x_{v,v,j}=0\wedge q_{v,S,j}=q_{v,S,j-1})$

In words, if we are doing loop elimination (i.e. the self-loop existed before
but not after $x_{v,v,j-1}=1\wedge x_{v,v,j}=0$), then,
$q_{v,S,j}=q_{v,S,j-1}/(1-q_{v,v,j-1})\Rightarrow
q_{v,S,j}(1-q_{v,v,j-1})=q_{v,S,j-1})$, because $q_{v,v,j-1}\neq 1$ \- if the
probability of using the self-loop had been 1, we had no other successors of
$v$ than $v$ and thus we could not do loop elimination. The other part is
saying that if there were no self-loop before and after, then the value of
$q_{v,S,j}$ is as before. This is fine to do even if the edge $(v,S)$ does not
exist, but one could also test that similarly. Note that we do not consider
the case where there is a self-loop both before and after even if it can
occur: It only occurs in case there are no $S\neq v$ such that $(v,S)$ exists
and in that case, we do not need to set $q_{v,S,j}$ to anything in particular.

The expression for $q_{S,T,j}$ for each $S,T$ such that $S\neq v$ is

$q_{S,T,j}=q_{S,T,j-1}\enspace.$

In words, the value of the edge probability is as before. Again, this is fine
to do even if the edge $(v,S)$ does not exist, but one could also test that
similarly.

Note that we are not setting $q_{v,v,j}$ at all, since its value does not
matter as long as the edge does not exist.

  4. (4)

The expression for $n_{v,S,j}$, for each $S\neq v$ is

$\displaystyle(x_{v,v,j-1}$ $\displaystyle=1\wedge x_{v,v,j}=0\wedge
n_{v,S,j}(1-q_{v,v,j-1})=q_{v,v,j-1}n_{v,v,j-1}+n_{v,S,j-1}(1-q_{v,v,j-1}))\vee$
$\displaystyle(x_{v,v,j-1}$ $\displaystyle=0\wedge x_{v,v,j}=0\wedge
n_{v,S,j}=n_{v,S,j-1})\enspace.$

In words, if we are doing loop elimination (i.e. the self-loop existed before
but not after $x_{v,v,j-1}=1\wedge x_{v,v,j}=0$), then, since we took the loop
$q_{v,v,j-1}/(1-q_{v,v,j-1})$ many times in expectation, each taking
$n_{v,v,j-1}$ many steps, we need to add that in, giving us
$n_{v,S,j}=q_{v,v,j-1}n_{v,v,j-1}/(1-q_{v,v,j-1})+n_{v,S,j}\Rightarrow
n_{v,S,j}(1-q_{v,v,j-1})=q_{v,v,j-1}n_{v,v,j-1}+n_{v,S,j}(1-q_{v,v,j-1})$. On
the other hand, if we did not have a loop to eliminate, the number of steps
for this edge is as before. Finally, like in the previous case, if we did not
do loop elimination or if this edge does not exist, we can set the value of
$n_{v,S,j}$ arbitrarily.

The expression for $n_{S,T,j}$, for each $S\neq v$ is

$n_{S,T,j}=n_{S,T,j-1}\enspace.$

In words, we do not change the edge at all if it is not going out of $v$.

  5. (5)

The expression for $r_{v,S,j}$, for each $S\neq v$ is

$\displaystyle(x_{v,v,j-1}$ $\displaystyle=1\wedge x_{v,v,j}=0\wedge
r_{v,S,j}(1-q_{v,v,j-1})=q_{v,v,j-1}r_{v,v,j-1}+r_{v,S,j-1}(1-q_{v,v,j-1}))\vee$
$\displaystyle(x_{v,v,j-1}$ $\displaystyle=0\wedge x_{v,v,j}=0\wedge
r_{v,S,j}=r_{v,S,j-1})\enspace.$

In words, this is analogous to how we updated $n_{v,S,j}$

The expression for $r_{S,T,j}$, for each $S\neq v$ is

$r_{S,T,j}=r_{S,T,j-1}\enspace.$

In words, we do not change the edge at all if it is not going out of $v$.

##### State elimination

For odd $j>3$ (i.e. we are doing state elimination from $j-1$ to $j$ on some
state $v=N+1-(j-1)/2$), we use the following expressions:

  1. (1)

The expression for $x_{v,j}$ is

$\displaystyle(x_{v,j}$ $\displaystyle=0\wedge x_{v,j-1}=0)\vee$
$\displaystyle(x_{v,j}$ $\displaystyle=1\wedge x_{v,j-1}=1\wedge\sum_{S\neq
v}x_{S,v,j-1}>0\wedge\sum_{S\neq v}x_{v,S,j-1}=0)\vee$ $\displaystyle(x_{v,j}$
$\displaystyle=0\wedge x_{v,j-1}=1\wedge(\sum_{S\neq
v}x_{S,v,j-1}=0\vee\sum_{S\neq v}x_{v,S,j-1}>0))$

In words, we can not eliminate $v$ if it has already been eliminated, or if it
is absorbing and have incoming edges. Note that $\sum_{S\neq v}x_{S,v,j-1}$ is
the number of incoming edges to $v$ and $\sum_{S\neq v}x_{v,S,j-1}$ is the
number of outgoing from $v$, in both cases ignoring loops.

For each other state $S\neq v$ the expression for $x_{S,j}$ is

$x_{S,j}=x_{S,j-1}$

In words, it exists if it did before.

  2. (2)

The expression for $x_{v,S,j}$, for each $S\neq v$ is as follows:

$(x_{v,j}=1\wedge x_{v,S,j}=x_{v,S,j-1})\vee(x_{v,j}=0\wedge x_{v,S,j}=0)$

In words, if we did not do state elimination, we do nothing to the edge,
otherwise, we remove it.

Similarly, the expression for $x_{S,v,j}$, for each $S\neq v$ is as follows:

$(x_{v,j}=1\wedge x_{S,v,j}=x_{S,v,j-1})\vee(x_{v,j}=0\wedge x_{S,v,j}=0)$

Also, the expression for $x_{v,v,j}$ is as follows:

$(x_{v,j}=1\wedge x_{v,v,j}=x_{v,v,j-1})\vee(x_{v,j}=0\wedge x_{v,v,j}=0)$

Finally, the expression for each other edge $x_{S,T}$ for $S\neq v\neq T$, is
as follows:

$\displaystyle(x_{v,j}$ $\displaystyle=1\wedge x_{S,T,j}=x_{S,T,j-1})\vee$
$\displaystyle(x_{v,j}$ $\displaystyle=0\wedge
x_{S,T,j}=1\wedge(x_{S,T,j-1}=1\vee x_{S,v,j-1}+x_{v,T,j-1}=2))\vee$
$\displaystyle(x_{v,j}$ $\displaystyle=0\wedge x_{S,T,j}=0\wedge
x_{S,T,j-1}=0\wedge x_{S,v,j-1}+x_{v,T,j-1}<2)$

In words, if we did not do state elimination we did nothing, otherwise, there
is an edge $(S,T)$ if there were one before or if there were an edge from $S$
to $v$ and one from $v$ to $T$ and otherwise not.

  3. (3)

The expression for $q_{S,T,j}$, for each $S\neq v\neq T$ is

$\displaystyle(x_{v,v,j}$ $\displaystyle=0\wedge
x_{S,v,j-1}+x_{v,T,j-1}=2\wedge x_{S,T,j-1}=1\wedge
q_{S,T,j}=q_{S,T,j-1}+q_{S,v,j-1}*q_{v,T,j-1})\vee$ $\displaystyle(x_{v,v,j}$
$\displaystyle=0\wedge x_{S,v,j-1}+x_{v,T,j-1}<2\wedge
q_{S,T,j}=q_{S,T,j-1})\vee$ $\displaystyle(x_{v,v,j}$ $\displaystyle=0\wedge
x_{S,v,j-1}+x_{v,T,j-1}=2\wedge x_{S,T,j-1}=0\wedge
q_{S,T,j}=q_{S,v,j-1}*q_{v,T,j-1})\vee$ $\displaystyle(x_{v,v,j}$
$\displaystyle=1\wedge q_{S,T,j}=q_{S,T,j-1})$

In words, the first clause is saying that if we do state elimination, we had
edges $(S,v),(v,T)$ and $(S,T)$, then the probability to go through $(S,T)$
after the elimination is the probability of going from $S$ to $v$ to $T$ plus
the probability to go $(S,T)$ from before we did state elimination. The second
clause is saying that if we do state elimination and had $(S,T)$ but not both
$(S,v)$ and $(v,T)$ then the probability for $(S,T)$ is as before. The third
is saying that if we do state elimination and had both $(S,v)$ and $(v,T)$,
but not $(S,T)$ then the probability for $(S,T)$ after is the probability of
going $S$ to $v$ to $T$ before. The last is saying that if we did not do state
elimination, then the probability remains unchanged.

The expression for $q_{v,S,j}$, for each $S$ is

$(x_{v,v,j}=1\wedge q_{v,S,j}=q_{v,S,j-1})\vee x_{v,v,j}=0$

In words, if we did not do state elimination, then the probability remains the
same. If we did state elimination we do not care about $q_{v,S,j}$. We could
as such equally have used the expression $q_{v,S,j}=q_{v,S,j-1}$, since we do
not care about the value of $q_{v,S,j}$ if we did do state elimination, but
this makes the construction easier to follow.

The expression for $q_{S,v,j}$, for each $S\neq v$ is

$(x_{v,v,j}=1\wedge q_{S,v,j}=q_{S,v,j-1})\vee x_{v,v,j}=0$

In words, if we did not do state elimination, then the probability remains the
same. If we did state elimination we do not care about $q_{S,v,j}$. Like
above, we could do $q_{S,v,j}=q_{S,v,j-1}$ instead.

  4. (4)

The expression for $n_{S,T,j}$, for each $S\neq v\neq T$ is

$\displaystyle(x_{v,v,j}$ $\displaystyle=0\wedge
x_{S,v,j-1}+x_{v,T,j-1}=2\wedge x_{S,T,j-1}=1\wedge$ $\displaystyle n_{S,T,i}$
$\displaystyle(q_{S,T,j-1}+q_{S,v,j-1}q_{v,T,j-1})=n_{S,T,j-1}q_{S,T,j-1}+q_{S,v,j-1}q_{v,T,j-1}(n_{S,v,j-1}+n_{v,T,j-1}))\vee$
$\displaystyle(x_{v,v,j}$ $\displaystyle=0\wedge
x_{S,v,j-1}+x_{v,T,j-1}<2\wedge n_{S,T,j}=n_{S,T,j-1})\vee$
$\displaystyle(x_{v,v,j}$ $\displaystyle=0\wedge
x_{S,v,j-1}+x_{v,T,j-1}=2\wedge x_{S,T,j-1}=0\wedge
n_{S,T,j}=n_{S,v,j-1}+n_{v,S,j-1})\vee$ $\displaystyle(x_{v,v,j}$
$\displaystyle=1\wedge n_{S,T,j}=n_{S,T,j-1})$

In words, the first clause (which is over the first two lines) is saying that
if we do state elimination, we had edges $(S,v),(v,T)$ and $(S,T)$, then the
expected length to go through $(S,T)$ after the elimination is

$\frac{n_{S,T,j-1}q_{S,T,j-1}}{q_{S,T,j-1}+q_{S,v,j-1}q_{v,T,j-1}}+\frac{q_{S,v,j-1}q_{v,T,j-1}(n_{S,v,j-1}+n_{v,T,j-1})}{q_{S,T,j-1}+q_{S,v,j-1}q_{v,S,j-1}}\enspace,$

i.e. if we went through $(S,T)$ after, it corresponded to going from $S$ to
$T$ directly before or from $S$ to $v$ to $T$ and those options are not
necessarily equally likely, so we need to multiply with the conditional
probability of going through those edges. The second clause is saying that if
we do state elimination and had $(S,T)$ but not both $(S,v)$ and $(v,T)$ then
the length of $(S,T)$ is as before. The third is saying that if we do state
elimination and had both $(S,v)$ and $(v,T)$, but not $(S,T)$ then the length
of $(S,T)$ after is the length of the path from $S$ to $v$ to $T$. The last is
saying that if we did not do state elimination, then the length remains
unchanged.

The expression for $n_{v,S,j}$, for each $S$ is

$(x_{v,v,j}=1\wedge n_{v,S,j}=n_{v,S,j-1})\vee x_{v,v,j}=0$

In words, if we did not do state elimination, then the length remains the
same. If we did state elimination we do not care about $n_{v,S,j}$. We could
as such equally have used the expression $n_{v,S,j}=n_{v,S,j-1}$, since we do
not care about the value of $n_{v,S,j}$ if we did do state elimination, but
like for the probability it seemed harder to follow.

The expression for $n_{S,v,j}$, for each $S\neq v$ is

$(x_{v,v,j}=1\wedge n_{S,v,j}=n_{S,v,j-1})\vee x_{v,v,j}=0$

In words, if we did not do state elimination, then the length remains the
same. If we did state elimination we do not care about $n_{S,v,j}$. Like
above, we could do $n_{S,v,j}=n_{S,v,j-1}$ instead.

  5. (5)

The expression for $r_{S,T,j}$ is much the same as for $n_{S,T,j}$ but is
included for completeness.

The expression for $r_{S,T,j}$, for each $S\neq v\neq T$ is

$\displaystyle(x_{v,v,j}$ $\displaystyle=0\wedge
x_{S,v,j-1}+x_{v,T,j-1}=2\wedge x_{S,T,j-1}=1\wedge$ $\displaystyle r_{S,T,j}$
$\displaystyle(q_{S,T,j-1}+q_{S,v,j-1}q_{v,S,j-1})=r_{S,T,j-1}q_{S,T,j-1}+q_{S,v,j-1}q_{v,T,j-1}(r_{S,v,j-1}+r_{v,T,j-1}))\vee$
$\displaystyle(x_{v,v,j}$ $\displaystyle=0\wedge
x_{S,v,j-1}+x_{v,T,j-1}<2\wedge r_{S,T,j}=r_{S,T,j-1})\vee$
$\displaystyle(x_{v,v,j}$ $\displaystyle=0\wedge
x_{S,v,j-1}+x_{v,T,j-1}=2\wedge x_{S,T,j-1}=0\wedge
r_{S,T,j}=r_{S,v,j-1}+r_{v,T,j-1})\vee$ $\displaystyle(x_{v,v,j}$
$\displaystyle=1\wedge r_{S,T,j}=r_{S,T,j-1})$

In words, the first clause (which covers the first two lines) is saying that
if we do state elimination, we had edges $(S,v),(v,T)$ and $(S,T)$, then the
expected reward to go through $(S,T)$ after the elimination is
$r_{S,T,j-1}q_{S,T,j-1}/(q_{S,T,j-1}+q_{S,v,j-1}q_{v,T,j-1})+q_{S,v,j-1}q_{v,T,j-1}(r_{S,v,j-1}+r_{v,T,j-1})/(q_{S,T,j-1}+q_{S,v,j-1}q_{v,T,j-1})$,
i.e. if we went through $(S,T)$ after, it corresponded to going from $S$ to
$T$ directly before or from $S$ to $v$ to $T$ and those options are not
necessarily equally likely, so we need to multiply with the conditional
probability of going through those edges. The second clause is saying that if
we do state elimination and had $(S,T)$ but not both $(S,v)$ and $(v,T)$ then
the reward of $(S,T)$ is as before. The third is saying that if we do state
elimination and had both $(S,v)$ and $(v,T)$, but not $(S,T)$ then the reward
of $(S,T)$ after is the reward of the path from $S$ to $v$ to $T$. The last is
saying that if we did not do state elimination, then the reward remains
unchanged.

The expression for $r_{v,S,j}$, for each $S$ is

$(x_{v,v,j}=1\wedge r_{v,S,j}=r_{v,S,j-1})\vee x_{v,v,j}=0$

In words, if we did not do state elimination, then the length remains the
same. If we did state elimination we do not care about $r_{v,S,j}$. We could
as such equally have used the expression $r_{v,S,j}=r_{v,S,j-1}$, since we do
not care about the value of $r_{v,S,j}$ if we did do state elimination, but
like for the probability it seemed harder to follow.

The expression for $r_{S,v,j}$, for each $S\neq v$ is

$(x_{v,v,j}=1\wedge r_{S,v,j}=r_{S,v,j-1})\vee x_{v,v,j}=0$

In words, if we did not do state elimination, then the reward remains the
same. If we did state elimination we do not care about $r_{S,v,j}$. Like
above, we could do $r_{S,v,j}=r_{S,v,j-1}$ instead.

##### Finding the value

Once we did all the above iterations, we are left with a Markov chain where
either state 1 is absorbing or it has no self-loop and has edges to absorbing
states. All remaining states are absorbing. We want a variable $v_{s}$ that,
for each state, $s$ is the value of the state (if it exists). For each state,
$s\neq 1$, we have a variable $v_{s}$ with expression

$(x_{s,2N}=1\wedge v_{s}n_{s,s,2N-1}=r_{s,s,2N})\vee x_{s,2N}=0$

In words, if the state exists, the mean-payoff value is
$v_{s}=r_{s,s,2N}/n_{s,s,2N}$. Otherwise, if the state does not exist, we do
not care.

For state $1$, we have the variable $v_{1}$ with expression

$(x_{1,1,2N}=1\wedge v_{1}n_{1,1,2n}=r_{1,1,2N})\vee(x_{1,1,2N}=0\wedge
v_{1}=\sum_{s\neq 1}x_{1,s,2N}q_{1,s,2N}v_{s})$

In words, the value of $1$, if it is absorbing, is like the above. If it is
not absorbing, it is for each other state $s$ state 1 has an edge to, the
probability of going to $s$ from 1 times the value of $s$. Note that
$x_{1,s,2N}$ is an indicator variable for whether the edge $(1,s)$ exists.

##### Proof of lemma

The correctness of the lemma follows from that each variable, both initially
and based on the previous variables, is set correctly. There are $2N-1$
iterations. In each iteration, we use $5$ variables, 4 for edges and 1 for
states. There can be at most $N^{2}$ edges and $N$ states. Because we have
variables for before and after each iteration (the before matches the ones for
after the previous), we get a total of $8N^{3}+2N$ variables for this.
Additionally, we use $N$ variables for the values, getting us up to
$8N^{3}+3N$. Each variable requires between $1$ and $13$ polynomials for below
$100N^{3}+40N$ polynomials in total ($8\cdot 13=104$, but many of the
expressions are much smaller than the worst case). The maximum degree is
$|A|\cdot b$ for each of these polynomials (for setting the initial
variables). The worst case for the numbers in the coefficients comes from the
input game of $\tau$.

##  Appendix C Proofs for Section 7

###  C.1. A proof of Claim 7.4

See 7.4

###### Proof.

We first prove that the rewards differ additively. Without loss of generality,
we assume that for every pair of game states $v,v^{\prime}\in V$, actions
vector ${\bf a}\in A^{k}$, and signal vector $s$, there exists a unique reward
vector ${\bf r}$ such that $\Delta(v,{\bf a})({\bf r},s,v^{\prime})>0$. If the
same action profile produces different rewards on the same action, then we can
replace all such transitions in the game by a single transition which produces
the expected reward from all such possible transitions. Let

$X\stackrel{{\scriptstyle\text{{\tiny{def}}}}}{{=}}\sum_{a\in
A^{k}\mid\Delta(v,a)({\bf r},{\bf s^{\prime}},v^{\prime})>0}\Delta(v,a)({\bf
r},{\bf s^{\prime}},v^{\prime}){\bf r}[i]\cdot\left(p(\sigma,v,{\bf m},s,{\bf
m^{\prime}},{\bf a})-p(\sigma^{\prime},v,{\bf m},s,{\bf m^{\prime}},{\bf
a})\right)$

be the difference in rewards in $M$ and $M^{\prime}$ for player $i$. For
convenience, we write $p(a)$ instead of $p(\sigma,{\bf m},s,{\bf
m^{\prime}},{\bf a})$ and $p^{\prime}(a)$ for $p(\sigma^{\prime},{\bf
m},s,{\bf m^{\prime}},{\bf a})$.

We have that ${\bf r}[i]\in[-C,C]$ and we will next bound
$p(a)-p^{\prime}(a)$. We have that for all action profiles $a$,
$p(a)-p^{\prime}(a)=p(a)(1-p^{\prime}(a)/p(a))$. There are two cases, either
$p^{\prime}(a)>p(a)$ or $p(a)>p^{\prime}(a)$. If $p^{\prime}(a)>p(a)$, then
$1-p^{\prime}(a)/p(a)=-\delta(p(a),p^{\prime}(a))$. Otherwise, if
$p(a)>p^{\prime}(a)$ then $\delta(p(a),p^{\prime}(a))=p(a)/p^{\prime}(a)-1$,
implying that $p^{\prime}(a)/p(a)=1/(\delta(p(a),p^{\prime}(a))+1)$ and thus
that
$1-p^{\prime}(a)/p(a)=\delta(p(a),p^{\prime}(a))/(\delta(p(a),p^{\prime}(a))+1)$.
We have that $p(a)/p^{\prime}(a)+1)\leq\delta(p(a),p^{\prime}(a))$ because
$\delta(p(a),p^{\prime}(a))$ is non-negative and we, therefore, divide with
something bigger than 1. Hence,
$p(a)-p^{\prime}(a)\in[-p(a)\delta(p(a),p^{\prime}(a)),p(a)\delta(p(a),p^{\prime}(a))]$.
Clearly, $\delta(p(a),p^{\prime}(a))\leq\delta(\sigma,\sigma^{\prime})$,
because it is a maximum over a set containing $\delta(p(a),p^{\prime}(a))$.
Thus, ${\left|X\right|}\leq\sum_{a=(a_{1},\dots,a_{k})}C\cdot\Delta(v,a)({\bf
r},s,v^{\prime})\cdot
p(a)\delta(\sigma,\sigma^{\prime})=C\cdot\delta(\sigma,\sigma^{\prime})\sum_{a=(a_{1},\dots,a_{k})}\Delta(v,a)({\bf
r},s,v^{\prime})p(a)$, which is $\leq C\cdot\delta(\sigma,\sigma^{\prime})$ as
the sum of probabilities is $\leq 1$.

We now prove that the transition probabilities differ multiplicatively. We
have that $P=\sum_{a=(a_{1},\dots,a_{k})}p(\sigma,{\bf m},s,{\bf
m^{\prime}},{\bf a})\cdot\Delta(v,{\bf a})(r,{\bf s^{\prime}},v^{\prime})$ and
similarly $P^{\prime}=\sum_{a=(a_{1},\dots,a_{k})}p(\sigma^{\prime},{\bf
m},s,{\bf m^{\prime}},{\bf a})\cdot\Delta(v,{\bf a})(r,{\bf
s^{\prime}},v^{\prime})$. We will look at the sums term by term. We have three
cases, either $P=P^{\prime}$, $P>P^{\prime}$ or $P<P^{\prime}$. In the first
case, we have that $\delta(P,P^{\prime})=0\leq\delta(\sigma,\sigma^{\prime})$.
The two remaining cases we show just one as the other is analogous. Consider
that $P>P^{\prime}$ and thus $\delta(P,P^{\prime})=P/P^{\prime}-1$. We have
that

$p(a)/p^{\prime}(a)-1\leq\delta(\sigma,\sigma^{\prime})\Rightarrow
p(a)\leq(\delta(\sigma,\sigma^{\prime})+1)p^{\prime}(a)$

and therefore that

$\displaystyle\delta(P,P^{\prime})+1=P/P^{\prime}$
$\displaystyle=\frac{\sum_{a=(a_{1},\dots,a_{k})}p(a)\cdot\Delta(v,a)({\bf
r},s,v^{\prime})}{\sum_{a=(a_{1},\dots,a_{k})}p^{\prime}(a)\cdot\Delta(v,a)({\bf
r},s,v^{\prime})}$
$\displaystyle\leq\frac{\sum_{a=(a_{1},\dots,a_{k})}p^{\prime}(a)(\delta(\sigma,\sigma^{\prime})+1)\cdot\Delta(v,a)({\bf
r},s,v^{\prime})}{\sum_{a=(a_{1},\dots,a_{k})}p^{\prime}(a)\cdot\Delta(v,a)({\bf
r},s,v^{\prime})}$ $\displaystyle=\delta(\sigma,\sigma^{\prime})+1\qed$

###  C.2. Approximating Markov Chains

We first recall some properties of $u$-bit floating point numbers
$\mathbb{Q}(u)$ and the finite-precision variants of the addition,
multiplication and division operations $\oplus^{u},\oslash^{u},\otimes^{u}$.

###### Proposition C.1.

  1. (1)

For every $x\in\mathbb{R}_{>0}$ and $u\in\mathbb{N}$ there exists
$x^{\prime}\in\mathbb{Q}(u)$ that is $(u,1)$-close to $x$.

  2. (2)

If $x$ is $(u,i)$-close to $y$ and $y$ is $(u,j)$-close to $z$, then $x$ is
$(u,i+j)$-close to $z$.

  3. (3)

Let $x$, $\tilde{x}$, $y$, $\tilde{y}$ be non-negative numbers such that $x$
is $(u,i)$-close to $\tilde{x}$ and $y$ is $(u,j)$-close to $\tilde{y}$. Then,
$x+y$ is $(u,\text{max}(i,j)+1)$-close to $\tilde{x}+\tilde{y}$, $xy$ is
$(u,i+j)$-close to $\tilde{x}\tilde{y}$, and $x/y$ is $(u,i+j)$-close to
$\tilde{x}/\tilde{y}$.

  4. (4)

If $x^{\prime}\in\mathbb{Q}(u)$ is $(u,j)$-close to $x$ and
$y^{\prime}\in\mathbb{Q}(u)$ is $(u,j)$-close to $y$, then
$x^{\prime}\oplus^{u}y^{\prime}$ is $(u,\max(i,j)+1)$-close to $x+y$;
$x^{\prime}\oslash^{u}y^{\prime}$ is $(u,ij+1)$-close to $x/y$; and
$x^{\prime}\otimes^{u}y^{\prime}$ is $(u,i+j+1)$-close to $xy$;

We also recall some properties of probability distributions represented by
approximately normalised representation.

###### Lemma C.2.

  1. (1)

For any probability distribution $q=(q_{1},q_{2},\ldots,q_{m})$ there exist
$(p_{1},p_{2},\ldots,p_{m})\in\mathbb{P}(u)$ so that for all $i$, $q_{i}$ and
$p_{i}$ are $(u,2m+2)$-close.

  2. (2)

Suppose that $a_{1},a_{2},\ldots,a_{m}\in\mathbb{D}(u)$ and for all $i=1\ldots
m$ let $p^{\prime}_{i}=a_{i}\oslash^{u}\bigoplus^{u}_{j=1\ldots m}a_{j}$ and
$p_{i}=p^{\prime}_{i}/\sum_{j=1\ldots m}p^{\prime}_{j}$. Then
$(p^{\prime}_{1},p^{\prime}_{2},\ldots,p^{\prime}_{m})$ is an approximately
normalised representation of $(p_{1},p_{2},\ldots,p_{m})\in\mathbb{P}(u)$.

We recall the following Lemma of Solan (Solan, 2003). This is very similar to
our Lemma 7.3 in that it quantifies the change in value as a result of
perturbations. Instead of perturbing strategies in MDPs, as we do in Lemma
7.3, this considers perturbations of transition probabilities _and reward
functions_ in Markov chains.

###### Lemma C.3 ((Solan, 2003), Theorem 4).

Given a Markov chain $M$ and $M^{\prime}$ with the same states, let
$\mathop{dist}(\mathop{p}\nolimits_{ij},\mathop{p}\nolimits_{ij})\leq\varepsilon$,
$\mathop{dist}(\mathop{r}\nolimits_{ij},\mathop{r}\nolimits^{\prime}_{ij})\leq
C$, and
$\mathop{dist}(\mathop{d}\nolimits_{ij},\mathop{d}\nolimits^{\prime}_{ij})\leq
C$. Then the mean payoff value of $M$ and $M^{\prime}$ differ by at most
$4\varepsilon NC$.

We can now bound the error introduced by the imprecise loop elimination and
state eliminations procedures.

See 7.9

###### Proof.

Let $\hat{M}$ be the Markov chain obtain by the precise loop elimination
algorithm. By Lemma 5.4, $M$ has the same mean-payoff value as $\hat{M}$.
Therefore, we bound the difference in mean-payoff value of $M^{\prime}$ and
$\hat{M}$. Let $N$ be the number of states in the Markov chain.

Since the probabilities in $M$ and $M^{\prime}$ are given in approximately
normalised representation, we write $\mathop{p}\nolimits(i,j)$ and
$\mathop{p}\nolimits^{\prime}(i,j)$ for the numbers giving the approximately
normalised representation of the distributions
$\tilde{\mathop{p}\nolimits}(i,j)$ and
$\tilde{\mathop{p}\nolimits}^{\prime}(i,j)$ respectively. We write
$\hat{\mathop{p}\nolimits}(i,j)$ to represent the probabilities in $\hat{M}$.

  1. (1)

Each $\mathop{p}\nolimits(i,j)$ is $(u,N)$-close to the actual probability
distribution of $M$, which is $\tilde{\mathop{p}\nolimits}(i,j)$ by Lemma C.2.

  2. (2)

Each $\oplus_{k\neq i}\mathop{p}\nolimits(n,k)$ is $(u,2N-1)$-close to
$\sum_{k\neq i}\tilde{\mathop{p}\nolimits}(n,k)$ by $N-1$ applications of Item
4 of Proposition C.1 and item (1) above.

  3. (3)

Each $\mathop{p}\nolimits^{\prime}(n,j)$ is $(u,(2N-1)N)$-close to
$\hat{\mathop{p}\nolimits}(n,j)$ by Item 4 of Proposition C.1 and items (1)
and (2) above.

  4. (4)

Each $\tilde{\mathop{p}\nolimits}^{\prime}(n,j)$ is $(u,N)$-close to
$\mathop{p}\nolimits^{\prime}(n,j)$ by definition of approximately normalised
representation and Lemma C.2.

  5. (5)

Each $\tilde{\mathop{p}\nolimits}^{\prime}(n,j)$ is $(u,2(N-1)N+N)$-close to
$\hat{probm}(n,j)$ by Item 2 of Proposition C.1 and items (3) and (4), and
therefore at least $(u,2N^{2})$-close.

  6. (6)

Each
$(\mathop{r}\nolimits(n,j)\otimes\mathop{p}\nolimits(n,j)\oplus(\mathop{r}\nolimits(n,n))\otimes\mathop{p}\nolimits(n,n))$
is $(u,N+1)$-close to
$\mathop{r}\nolimits(n,j)\tilde{\mathop{p}\nolimits(n,j)}+\mathop{r}\nolimits(n,n)\tilde{\mathop{p}\nolimits}(n,n)$
by item (1) above and Item 4 of Proposition C.1.

  7. (7)

Each $\mathop{r}\nolimits^{\prime}(i,j)$ is $(u,2(N-1)(N+1))$-close to
$\hat{\mathop{r}\nolimits}(i,j)=(\mathop{r}\nolimits(n,j)\tilde{\mathop{p}\nolimits(n,j)}+\mathop{r}\nolimits(n,n)\tilde{\mathop{p}\nolimits}(n,n))/\sum_{k\neq
i}\tilde{\mathop{p}\nolimits}(n,k)$ by Item 4 of Proposition C.1 applied to
items (6) and (2), so at most $(u,2N^{2}+N)$-close.

  8. (8)

Each $\mathop{d}\nolimits^{\prime}(i,j)$ is $(u,2N^{2}+N)$-close to
$\hat{\mathop{d}\nolimits}(i,j)$ by the same argument as item (7).

By Lemma C.3, we get that the mean-payoff value of $M^{\prime}$ differ from
the value in $\hat{M}$ by at most $4\varepsilon NC$, where the $\varepsilon$
is the maximum difference in the probabilities of $\hat{M}$ and $M^{\prime}$,
and $C$ is the maximum difference of rewards in $\hat{M}$ and $M^{\prime}$. In
our case, we have
$\varepsilon=\big{(}\frac{1}{1-2^{-u-1}}\big{)}^{2(N)^{2}}-1$. Since, $u\geq
1000N^{2}$, we have $\big{(}\frac{1}{1-2^{-u-1}}\big{)}^{2(N)^{2}}\leq
5(N^{2})2^{-u}$, which gives $\varepsilon\leq 5(N^{2})2^{-u}$. Similarly, we
get $C\leq 5(N^{2}+N)2^{-u}$, which together gives $4N\varepsilon C\leq
100(N^{4}+N^{3})2^{-u}$. Choosing $\delta_{2}=100(N^{4}+N^{3})$ completes the
proof of item (2).

The exponent for the probabilities are always negative as the values are $\leq
1$. It is easy to see that in our updates
$2\tilde{\mathop{p}\nolimits}_{ij}\geq\tilde{\mathop{p}\nolimits^{\prime}}_{ij}\geq\tilde{\mathop{p}\nolimits}_{ij}$.
This implies that the negative exponents in the probabilities decreases by at
most $1$.

The rewards and durations can be assumed to be $\geq 1$ and therefore the
exponent can be assumed to be positive. Note that the rewards can be made $>1$
by adding the smallest reward to each step and then subtracting it from the
obtained value in the end. In a single step the rewards are less than twice
the maximum reward in the input Markov chain. Therefore, the maximum exponent
is at most $1$ more than that in the input. A similar argument works for
duration as well assuming that the durations in the input are all $\geq 1$. ∎

See 7.8

###### Proof.

Let $\hat{M}$ be the Markov chain obtain by the precise state elimination
algorithm. By Lemma 5.2, $M$ has the same mean-payoff value as $\hat{M}$.
Therefore, we bound the difference in mean-payoff value of $M^{\prime}$ and
$\hat{M}$. We again estimate the relative distance between the precise and
imprecise variables using the same notations as above. Let $N$ be the number
of states of the Markov chain.

  1. (1)

Each $\mathop{p}\nolimits(i,j)$ is $(u,N)$-close to the actual probability
distribution of $M$, which is $\tilde{\mathop{p}\nolimits}(i,j)$ by Lemma C.2.

  2. (2)

Each $\mathop{p}\nolimits^{\prime}(i,j)$ is $(u,2N+2)$-close to
$\hat{\mathop{p}\nolimits}(i,j)$ by item (1) above and applying Item 4 of
Proposition C.1.

  3. (3)

Each $\mathop{r}\nolimits^{\prime}(i,j)$ is $(u,2N+3)$-close to
$\hat{\mathop{r}\nolimits}(i,j)$ by applying Item 4 of Proposition C.1 to item
(1). The dominating factor is the distance between
$\mathop{p}\nolimits(i,n)\otimes\mathop{p}\nolimits(n,j)\otimes(\mathop{r}\nolimits(i,n)\oplus\mathop{r}\nolimits(n,j))$
and
$\tilde{\mathop{p}\nolimits(i,n)}\tilde{\mathop{p}\nolimits(n,j)}(\mathop{r}\nolimits(i,n)\oplus\mathop{r}\nolimits(n,j))$,
which gives the $2N+3$ term.

  4. (4)

Similar to item (3), we have $\mathop{d}\nolimits^{\prime}(i,j)$ is
$(u,2N+3)$-close to $\hat{\mathop{d}\nolimits}(i,j)$.

Instead of using the bound $2N+3$ obtained above, we instead use $3N$ for the
sake of brevity, as $(u,2N+3)$-closeness implies $(u,3N)$-close assuming
$N\geq 3$. By Lemma C.3, we get that the mean-payoff value of $M^{\prime}$
differ from the value in $\hat{M}$ by at most $4N\varepsilon C$, where the
$\varepsilon$, $\varepsilon=\big{(}\frac{1}{1-2^{-u-1}}\big{)}^{3N}-1$. Since
$u\geq 1000N^{2}$, we have $\big{(}\frac{1}{1-2^{-u-1}}\big{)}^{3N}\leq
1+7N2^{-u}$ which gives $\varepsilon\leq 1+7N2^{-u}$. We get the same bound on
$C$ and therefore, $4N\varepsilon C\leq 200N2^{-u}$. Choosing
$\delta_{1}=200N$ completes the proof of item (2).

The increase in positive and decrease in negative exponents can be shown to be
at most $1$ by the same argument as the loop-elimination case. ∎


# Satisfiability of Arbitrary Public Announcement Logic with Common Knowledge
is $\Sigma^{1}_{1}$-hard

Rustam Galimullin University of Bergen
Bergen, Norway<EMAIL_ADDRESS>University of Liverpool
Liverpool, UK Louwe B. Kuijer University of Liverpool
Liverpool, UK<EMAIL_ADDRESS>
###### Abstract

Arbitrary Public Announcement Logic with Common Knowledge (APALC) is an
extension of Public Announcement Logic with common knowledge modality and
quantifiers over announcements. We show that the satisfiability problem of
APALC on $S5$-models, as well as that of two other related logics with
quantification and common knowledge, is $\Sigma^{1}_{1}$-hard. This implies
that neither the validities nor the satisfiable formulas of APALC are
recursively enumerable. Which, in turn, implies that APALC is not finitely
axiomatisable.

##  1 Introduction

Quantified Public Announcement Logics. Epistemic logic (EL) [22] is one of the
better-known formalisms for reasoning about knowledge of agents in multi-agent
systems. It extends the language of propositional logic with constructs
$\square_{a}\varphi$ meaning that ‘agent $a$ knows $\varphi$’. Formulas of EL
are interpreted on epistemic models (or, equivalently, $S5$-models) that
comprise a set of states, equivalence relations for each agent between states,
and a valuation function that specifies in which states propositional
variables are true. However, EL provides only a static description of
distribution of knowledge in a system. Extensions of the logic that allow one
to reason about how information of individual agents and groups thereof
changes as a result of some epistemic event are generally collectively known
as dynamic epistemic logics (DELs) [11].

The prime example of a DEL and arguably the most well-studied logic in the
family is public announcement logic (PAL) [26]. A public announcement is an
event of all agents publicly and simultaneously receiving the same piece of
information. The language of PAL extends that of EL with formulas
$[\psi]\varphi$ that are read as ‘after public announcement of $\psi$,
$\varphi$ is true’.

Quantification over various epistemic actions, and in particular over public
announcements, has been explored in the last 15 or so years [10]. Adding
quantification over public announcements allows one to shift the emphasis from
the effects of a particular announcement to the question of (non-)existence of
an announcement leading to a desired epistemic goal. In this paper, we focus
on the three, perhaps most well-known, quantified PALs (QPALs). The first of
the three is arbitrary PAL (APAL) [7] that extends the language of PAL with
constructs $[!]\varphi$ meaning ‘after any public announcement, $\varphi$ is
true’. A formula with the dual existential quantifier $\langle!\rangle\varphi$
is read as ‘there is a public announcement, after which $\varphi$ is true’.

Observe that quantifiers of APAL do not specify whether an announcement can be
made by any of the agents, or groups thereof, modelled in a system. Hence, a
more ‘agent-centric’ quantified PAL was proposed. Group announcement logic
(GAL) [2] extends the language of PAL with formulas $[G]\varphi$ meaning
‘after any announcement by agents from group $G$, $\varphi$ is true’. A
formula with the dual of the universal GAL quantifier is $\langle
G\rangle\varphi$ that is read ‘there is an announcement by agents from group
$G$ that makes $\varphi$ true’.

Once we start reasoning about what groups of agents can achieve by making
public announcements, it is only too natural to consider their abilities in a
game-theoretic setting. In particular, we may let agents outside of the group
make their own announcements in an attempt to preclude the group from reaching
their epistemic goals. A QPAL with such a competitive flavour to it is called
coalition announcement logic (CAL) [3, 16]. The logic extends PAL with
modalities $[\\!\langle G\rangle\\!]\varphi$ that are read as ‘whatever agents
from coalition $G$ announce, there is a counter-announcement by the anti-
coalition that makes $\varphi$ true’. The diamond version
$\langle\\![G]\\!\rangle\varphi$ is then means that ‘there is an announcement
by coalition $G$, such that whatever the anti-coalition announces at the same
time, they cannot avoid $\varphi$’. Observe, that compared to APAL and GAL,
modalities of CAL contain double quantification: $\forall\exists$ and
$\exists\forall$ correspondingly. As the name of the logic suggests,
modalities of CAL were inspired by coalition logic [25], and they capture
game-theoretic notions of $\alpha$\- and $\beta$-effectivity [6].

Some Logical Properties of QPALs. One of the most pressing open problems in
the area is the existence of finitary axiomatisations of QPALs. Both finitary
and infinitary axiom systems for APAL were proposed in [7], but later the
finitary version was shown to be unsound [20]. The infinitary axiomatisation
is, however, sound and complete [8]. As the axiomatisation of GAL [2] is quite
similar to that of APAL, its finitary version is also not sound [14, Footnote
4], and its infinitary version can be shown to be sound and complete by a
modification of the proof from [8]. To the best of our knowledge, there are no
known sound and complete proof systems, finitary or infinitary, for CAL111A
complete infinitary axiomatisation with CAL modalities and additional
operators was given in [17].

The satisfiability problem for QPALs is known to be undecidable [4]. The
result is achieved by a reduction from the classic tiling problem that
consists in answering the question whether a given finite set of tiles can
tile the $\mathbb{N}\times\mathbb{N}$ plane. Since this problem is co-RE-
complete [9, 18], or, equivalently, $\Pi^{0}_{1}$-complete, the reduction
amounts to the fact that the satisfiability problem for QPALs is co-RE-hard
(or $\Pi^{0}_{1}$-hard). Note that this result does not rule out the existence
of finitary axiomatisations of QPALs. A prime example of a logic with a co-RE-
complete satisfiability problem and a finitary axiomatisation is first-order
logic.

Overview of the paper and our result. In this paper we consider extensions of
QPALs with common knowledge [13], which is a classic variant of group
knowledge in multi-agent systems. Its intuitive meaning is that ‘$\varphi$ is
common knowledge among agents in group $G$ if everyone in $G$ knows $\varphi$,
everyone in $G$ knows that everyone in $G$ knows $\varphi$ and so on ad
infinitum’. Semantically, common knowledge among agents from $G$ corresponds
to the reflexive transitive closure of equivalence relations of all agents
from group $G$. We call extensions of APAL, GAL, and CAL with common knowledge
APALC [5], GALC, and CALC, correspondingly, or QPALCs if we refer to all of
them at the same time.

The result we prove in this paper is that the satisfiability problems for
QPALCs are $\Sigma_{1}^{1}$-hard. We do this by showing that the _recurring
tiling problem_ , which is known to be $\Sigma_{1}^{1}$-complete [19], can be
reduced to satisfiability of QPALC formulas. Because the satisfiability
problems are $\Sigma_{1}^{1}$-hard, it follows that, in particular, the set of
valid QPALC formulas is not recursively enumerable. That, in turn, implies
that QPALCs have no finitary axiomatisations. The non-existence of a finitary
axiomatisation of a somewhat related arbitrary arrow update logic [12] with
common knowledge was shown in [21] by the reduction from the non-halting
problem. Moreover, the recurring tiling problem was used in [23] to
demonstrate that the satisfiability problem of PAL with iterated announcements
and common knowledge is $\Sigma^{1}_{1}$-complete.

The use of common knowledge is instrumental in our paper, since it allows us
to have a ‘tighter’ grid than the ones from [4] and [15]. We deem our result
important in at least two ways. First, the non-existence of finitary
axiomatisations of QPALCs is interesting in its own right as it demonstrates
that presence of common knowledge in QPALCs is a sufficient condition for
$\Sigma^{1}_{1}$-hardness. Second, having both our construction (with common
knowledge) and the constructions from [4] and [15] side by side, allows one to
flesh out crucial differences between $\Sigma^{1}_{1}$-hardness and
$\Sigma_{1}^{0}$-hardness arguments, and, hopefully, move closer to tackling
the open problem of (non-)existence of finitary axiomatisations of QPALs.

Outline of the paper. The rest of the paper is organised as follows. In
Section 2 we cover the background on QPALCs. After that, in Section 3, we
prove the main claim of this paper, and, finally, we conclude in Section 4.

##  2 Quantified Public Announcement Logics with Common Knowledge

Let $A$ be a finite set of agents, and $P$ be a countable set of propositional
variables.

######  Definition 2.1.

The _languages of arbitrary public announcement logic with common knowledge_
$\mathsf{APALC}$, _group announcement logic with common knowledge_
$\mathsf{GALC}$, and _coalition announcement logic with common knowledge_
$\mathsf{CALC}$ are inductively defined as

$\displaystyle\mathsf{APALC}$ $\displaystyle\thinspace\ni$
$\displaystyle\enspace\varphi::=p\mid\neg\varphi\mid(\varphi\land\varphi)\mid\square_{a}\varphi\mid[\varphi]\varphi\mid\blacksquare_{G}\varphi\mid[!]\varphi$
$\displaystyle\mathsf{GALC}$ $\displaystyle\thinspace\ni$
$\displaystyle\enspace\varphi::=p\mid\neg\varphi\mid(\varphi\land\varphi)\mid\square_{a}\varphi\mid[\varphi]\varphi\mid\blacksquare_{G}\varphi\mid[G]\varphi$
$\displaystyle\mathsf{CALC}$ $\displaystyle\thinspace\ni$
$\displaystyle\enspace\varphi::=p\mid\neg\varphi\mid(\varphi\land\varphi)\mid\square_{a}\varphi\mid[\varphi]\varphi\mid\blacksquare_{G}\varphi\mid[\\!\langle
G\rangle\\!]\varphi$

where $p\in P$, $a\in A$, and $G\subseteq A$. Duals are defined as
$\Diamond_{a}\varphi:=\lnot\square_{a}\lnot\varphi$,
$\langle\psi\rangle\varphi:=\lnot[\psi]\lnot\varphi$,
$\blacklozenge_{G}\varphi:=\lnot\blacksquare_{G}\lnot\varphi$,
$\langle!\rangle\varphi:=\lnot[!]\lnot\varphi$, $\langle
G\rangle\varphi:=\lnot[G]\lnot\varphi$ and
$\langle\\![G]\\!\rangle\varphi:=\lnot[\\!\langle G\rangle\\!]\lnot\varphi$.

The fragment of $\mathsf{APALC}$ without $[!]\varphi$ is called _public
announcement logic with common knowledge_ $\mathsf{PALC}$; the latter without
$[\varphi]\varphi$ is _epistemic logic with common knowledge_ $\mathsf{ELC}$;
$\mathsf{PALC}$ and $\mathsf{ELC}$ minus $\blacksquare_{G}\varphi$ are,
correspondingly, _public announcement logic_ $\mathsf{PAL}$ and _epistemic
logic_ $\mathsf{EL}$. Finally, fragments of $\mathsf{APALC}$, $\mathsf{GALC}$
and $\mathsf{CALC}$ without $\blacksquare_{G}\varphi$ are called _arbitrary
public announcement logic_ $\mathsf{APAL}$, _group announcement logic_
$\mathsf{GAL}$ and _coalition announcement logic_ $\mathsf{CAL}$ respectively.

######  Definition 2.2.

A _model_ $M$ is a tuple $(S,\sim,V)$, where $S$ is a non-empty set of states,
$\sim:A\rightarrow 2^{S\times S}$ gives an equivalence relation for each
agent, and $V:P\rightarrow 2^{S}$ is the valuation function. By $\sim_{G}$ we
mean reflexive transitive closure of $\bigcup_{a\in G}\sim_{a}$. We will
denote model $M$ with a distinguished state $s$ as $M_{s}$.

We would like to stress that agent relations in our models are equivalence
relations (and hence our models are $S5$ models). The results of this paper do
not generalise to arbitrary agent relations in any obvious way.

It is assumed that for group announcements, agents know the formulas they
announce. In the following, we write $\mathsf{PALC}^{G}=\\{\bigwedge_{i\in
G}\square_{i}\psi_{i}\mid\textrm{for all }i\in G,\psi_{i}\in\mathsf{PALC}\\}$
to denote the set of all possible announcements by agents from group $G$. We
will use $\psi_{G}$ to denote arbitrary elements of $\mathsf{PALC}^{G}$.

######  Definition 2.3.

Let $M_{s}=(S,R,V)$ be a model, $p\in P$, $G\subseteq A$, and
$\varphi,\psi\in\mathsf{APALC}\cup\mathsf{GALC}\cup\mathsf{CALC}$.

$\displaystyle M_{s}\models p$ iff $\displaystyle\quad s\in V(p)$
$\displaystyle M_{s}\models\lnot\varphi$ iff $\displaystyle\quad
M_{s}\not\models\varphi$ $\displaystyle M_{s}\models\varphi\land\psi$ iff
$\displaystyle\quad M_{s}\models\varphi\text{ and }M_{s}\models\psi$
$\displaystyle M_{s}\models\square_{a}\varphi$ iff $\displaystyle\quad\forall
t\in S:s\sim_{a}t\text{ implies }M_{t}\models\varphi$ $\displaystyle
M_{s}\models\blacksquare_{G}\varphi$ iff $\displaystyle\quad\forall t\in
S:s\sim_{G}t\text{ implies }M_{t}\models\varphi$ $\displaystyle
M_{s}\models[\psi]\varphi$ iff $\displaystyle\quad M_{s}\models\psi\text{
implies }M_{s}^{\psi}\models\varphi$ $\displaystyle M_{s}\models[!]\varphi$
iff $\displaystyle\quad\forall\psi\in\mathsf{PALC}:M_{s}\models[\psi]\varphi$
$\displaystyle M_{s}\models[G]\varphi$ iff
$\displaystyle\quad\forall\psi_{G}\in\mathsf{PALC}^{G}:M_{s}\models[\psi_{G}]\varphi$
$\displaystyle M_{s}\models[\\!\langle G\rangle\\!]\varphi$ iff
$\displaystyle\quad\forall\psi_{G}\in\mathsf{PALC}^{G},\exists\chi_{A\setminus
G}\in\mathsf{PALC}^{A\setminus G}:M_{s}\models\psi_{G}\text{ implies
}M_{s}\models\langle\psi_{G}\land\chi_{A\setminus G}\rangle\varphi$

where $M_{s}^{\psi}=(S^{\psi},R^{\psi},V^{\psi})$ with $S^{\psi}=\\{s\in S\mid
M_{s}\models\psi\\}$, $R^{\psi}(a)$ is the restriction of $R(a)$ to $S^{\psi}$
for all $a\in A$, and $V^{\psi}(p)=V(p)\cap S^{\psi}$ for all $p\in P$.

Observe, that it follows from the definition of the semantics that in the case
of the grand coalition $A$, $M_{s}\models[A]\varphi$ if and only if
$M_{s}\models[\\!\langle A\rangle\\!]\varphi$. For the case of the empty group
$\varnothing$, we assume that the conjunction of an empty set of formulas is a
tautology.

######  Remark 1.

For APAL, GAL, and CAL, we assume that quantification ranges over a
quantifier-free fragment of the language, i.e. over PAL, which is equally
expressive as EL [26]. This is, however, not as straightforward once we
consider ELC and PALC. The latter is strictly more expressive than ELC [11,
Theorem 8.48], and ELC, in its turn, is strictly more expressive than EL, and
thus it matters, expressivity-wise, which quantifer-free fragment of a QPALC
the quantification ranges over. These matters are explored in [5], where also
infinitary axiomatisations of APALC and GALC are given. For our current
purposes, though, the difference in the range of quantification does not play
a role.

##  3 The Satisfiability Problem of QPALCs is $\Sigma^{1}_{1}$-hard

We prove the $\Sigma^{1}_{1}$-hardness of the satisfiability problem of QPALCs
via a reduction from the recurring tiling problem [18].

######  Definition 3.1.

Let $C$ be a finite set of _colours_. A _tile_ is a function
$\tau:\\{\mathsf{north},\mathsf{south},\mathsf{east},\mathsf{west}\\}\to C$. A
finite set of tiles $\mathrm{T}$ is called an _instance_ of the tiling
problem. A _solution_ to an instance of the tiling problem is a
function222Throughout the paper we assume that $0\in\mathbb{N}$.
$f:\mathbb{N}\times\mathbb{N}\to\mathrm{T}$ such that for all
$(i,j)\in\mathbb{N}\times\mathbb{N}$,

$\displaystyle f(i,j)(\mathsf{north})=f(i,j+1)(\mathsf{south})\text{ and
}f(i,j)(\mathsf{east})=f(i+1,j)(\mathsf{west}).$

######  Definition 3.2.

Let $\mathrm{T}$ be a finite set of tiles with a designated tile
$\tau^{\ast}\in\mathrm{T}$. The _recurring tiling problem_ is the problem to
determine whether there is a solution to instance $\mathrm{T}$ of the tiling
problem such that $\tau^{\ast}$ appears infinitely often in the first column.

We assume without loss of generality that the designated tile $\tau^{\ast}$
occurs only in the first column.

###  3.1 Encoding a Tiling

For our construction we will require five propositional variables — north,
south, east, west and centre — to designate the corresponding sides of tiles.
Additionally, we will have designated propositional variables for each colour
in $C$, and for each tile $\tau_{i}\in\mathrm{T}$ there is a propositional
variable $p_{i}$ that represents this tile. Finally, we will use $p^{\ast}$
for the special $\tau^{\ast}$.

In our construction, we will represent each tile with (at least) five states:
one for each of the four sides of a tile, and one for the centre. As for
agents, we require only three of them for our construction. Agent $s$, for
square, cannot distinguish states within the same tile. Agent $v$, for
vertical, cannot distinguish between the northern part of one tile and the
southern part of the tile above. Similarly, the horizontal agent $h$ cannot
distinguish between the eastern and western parts of adjacent tiles. See
Figure 1 for the depiction of an intended grid-like model.

{$\mathsf{west},c_{2}\\}${$\mathsf{centre}\\}${$\mathsf{north},c_{1}\\}${$\mathsf{east},c_{4}\\}${$\mathsf{south},c_{3}\\}${$\mathsf{south},c_{1}\\}$$v${$\mathsf{north},c_{3}\\}$$v${$\mathsf{east},c_{2}\\}$$h${$\mathsf{west},c_{4}\\}$$h$$\tau_{i}$

$\tau_{i}$$\tau_{j}$$\tau_{k}$$v$$v$$v$$\tau_{k}$$\tau_{j}$$h$$h$$h$$\tau_{i}$$\tau_{k}$$h$$h$$h$$v$$v$$\tau_{j}$$\tau_{i}$$h$$h$$h$$v$$v$$v$$v$

Figure 1: Left: a representation of a single tile $\tau_{i}$, where agent $s$
has the universal relation within the dashed square, relations $h$ and $v$ are
equivalences, and reflexive arrows are omitted. Each state is labelled by a
set of propositional variables that are true there. Right: an example of a
grid-like model that we construct in our proof. Each tile $\tau$ has a similar
structure as presented on the left of the figure.

Let an instance $\mathrm{T}$ of the recurring tiling problem be given. We
start by construction of formula $\Psi_{\mathrm{T}}$ that will be satisfied in
a given model if and only if the model is grid-like. We will build up
$\Psi_{\mathrm{T}}$ step-by-step, defining useful subformulas along the way.
Let $\mathsf{Position}$ be the following set
$\mathsf{Position}:=\\{\mathsf{north},$ $\mathsf{south},$ $\mathsf{east},$
$\mathsf{west},\mathsf{centre}\\}$.

The first constraint, expressed by formula $\mathit{one\\_colour}$, is that
each state is coloured by exactly one colour. To ensure that all five parts —
north, south, east, west, and centre — are present in a current square, we
state in $\mathit{all\\_parts}$ that in all squares the square agent $s$ has
access to all five relevant states.

$\displaystyle\mathit{one\\_colour}:=$ $\displaystyle\bigvee_{c\in
C}\left(c\land\bigwedge_{d\in C\setminus\\{c\\}}\lnot d\right)$
$\displaystyle\mathit{all\\_parts}:=$
$\displaystyle\square_{s}\bigvee_{{q\in\mathsf{Position}}}q\land\bigwedge_{q\in\mathsf{Position}}\Diamond_{s}q$

The formulas $\mathit{hor}$ and $\mathit{vert}$ state that the relation $h$
only allows us to move between $\mathsf{east}$ and $\mathsf{west}$ states,
while $v$ only allows movement between $\mathsf{north}$ and $\mathsf{south}$
states.

$\displaystyle\mathit{hor}:=$
$\displaystyle{}\bigwedge_{q\in\\{\mathsf{north},\mathsf{south},\mathsf{centre}\\}}(q\rightarrow\square_{h}q)$
$\displaystyle\mathit{vert}:=$
$\displaystyle{}\bigwedge_{q\in\\{\mathsf{east},\mathsf{west},\mathsf{centre}\\}}(q\rightarrow\square_{v}q)$

With $\mathit{one\\_pos}$ we force each state to satisfy exactly one
propositional variable from $\mathsf{Position}$, and with
$\mathit{one\\_tile}$ we ensure that all states within the same tile are
labelled by the tile proposition.

$\displaystyle\mathit{one\\_pos}:=$
$\displaystyle\bigvee_{q\in\mathsf{Position}}\left(q\land\bigwedge_{q^{\prime}\in\mathsf{Position}\setminus\\{q\\}}\lnot
q^{\prime}\right)$ $\displaystyle\mathit{one\\_tile}:=$
$\displaystyle\bigvee_{\tau_{i}\in\mathrm{T}}\left(p_{i}\land\square_{s}p_{i}\land\bigwedge_{\tau_{j}\in\mathrm{T}\setminus\\{\tau_{i}\\}}\lnot
p_{j}\right)$

Next, we force each state in a tile to satisfy exactly one atom corresponding
to their designated colour:

$\mathit{state\\_col}:=\bigvee_{\tau_{i}\in\mathrm{T}}\left(p_{i}\to\bigwedge_{q\in\mathsf{Position}\setminus\\{\mathsf{centre}\\}}(q\to\tau_{i}(q))\right),$

where $\tau_{i}(q)$ is the colour of the tile $\tau_{i}$ on the side $q$ (e.g.
$\tau_{i}(\mathsf{south})$ is the bottom colour of tile $\tau_{i}$).

All the formulas considered so far deal with the representation of a single
tile. We will use the following abbreviation:

$\psi_{\mathit{tile}}:=\mathit{one\\_colour}\land\mathit{all\\_parts}\land\mathit{hor}\land\mathit{vert}\land\mathit{one\\_pos}\land\mathit{one\\_tile}\land\mathit{state\\_col}$

Adjoining tiles are required to have the same colour on the sides facing each
other, we simulate this by requiring that agents $h$ and $v$ consider a
current colour in the top and right directions. In such a way we also ensure
that the grid is infinite in the positive quadrant.

$\mathit{adj\\_tiles}:=\bigwedge_{c\in C}\left((\mathsf{north}\land
c\to\Diamond_{v}\mathsf{south}\land\square_{v}c)\land(\mathsf{east}\land
c\to\Diamond_{h}\mathsf{west}\land\square_{h}c)\right)$

We are concerned with the reduction from the $\mathbb{N}\times\mathbb{N}$
recurring tiling problem, i.e. our grid will have left and bottom edges. We
force the existence of a tile at position $(0,0)$ with the following formula:

$\displaystyle\mathit{init}:=$
$\displaystyle{}\blacklozenge_{\\{h,v,s\\}}(\blacksquare_{\\{v,s\\}}(\mathsf{west}\rightarrow\square_{h}\mathsf{west})\land\blacksquare_{\\{h,s\\}}(\mathsf{south}\rightarrow\square_{v}\mathsf{south}))$

For the remaining formulas, it is useful to define two abbreviations. We use
$\square_{\mathit{up}}\varphi$ to denote
$\square_{s}(\mathsf{north}\rightarrow\square_{v}(\mathsf{south}\rightarrow\varphi))$,
i.e., we first move, by agent $s$, to the state representing the northern
quadrant of the tile, then we move, by agent $v$, to southern quadrant of the
tile above, where we evaluate $\varphi$. Similarly, we use
$\square_{\mathit{right}}\varphi$ to denote
$\square_{s}(\mathsf{east}\rightarrow\square_{h}(\mathsf{west}\rightarrow\varphi))$.
The duals $\lozenge_{\mathit{up}}$ and $\lozenge_{\mathit{right}}$ are defined
as usual.

The next two formulas are used to guarantee that for every tile there are
unique tiles, up to PALC-indistinguishability, above it and to its right.

$\displaystyle\mathit{up}:=$
$\displaystyle[!](\lozenge_{\mathit{up}}\lozenge_{s}\mathsf{centre}\rightarrow\square_{\mathit{up}}\lozenge_{s}\mathsf{centre})$
$\displaystyle\mathit{right}:=$
$\displaystyle[!](\lozenge_{\mathit{right}}\lozenge_{s}\mathsf{centre}\rightarrow\square_{\mathit{right}}\lozenge_{s}\mathsf{centre})$

Additionally, we use the following two formulas to establish a commutative
property: going up and then right results in a state that is PALC-
indistinguishable from going right and then up.

$\displaystyle\mathit{right\&up}:=[!](\lozenge_{\mathit{right}}\lozenge_{\mathit{up}}\lozenge_{s}\mathsf{centre}\rightarrow\square_{\mathit{up}}\square_{\mathit{right}}\lozenge_{s}\mathsf{centre})$
$\displaystyle\mathit{up\&right}:=[!](\lozenge_{\mathit{up}}\lozenge_{\mathit{right}}\lozenge_{s}\mathsf{centre}\rightarrow\square_{\mathit{right}}\square_{\mathit{up}}\lozenge_{s}\mathsf{centre})$

Finally, we make sure that any two states that are $h$ or $v$ related and that
are in the same position are parts of indistinguishable tiles.

$\displaystyle\mathit{no\\_change}:=$
$\displaystyle{}\bigwedge_{q,q^{\prime}\in\mathsf{Position}}[!]((q\wedge\lozenge_{s}q^{\prime})\rightarrow(\square_{h}(q\rightarrow\lozenge_{s}q^{\prime})\wedge\square_{v}(q\rightarrow\lozenge_{s}q^{\prime})))$

The formula $\mathit{hor}$ states that unless we are in a $\mathsf{east}$ or
$\mathsf{west}$ position, we cannot go to a different position using $h$.
Similarly, $\mathit{vert}$ states that unless we are in a $\mathsf{north}$ or
$\mathsf{south}$ position we can’t use $v$ to change position. The formula
$\mathit{no\\_change}$ then states that any move by relation $h$ or $v$ that
does not change the position must lead to an indistinguishable tile.

We abbreviate formulas with quantifiers as

$\psi_{x\&y}:=\mathit{up}\land\mathit{right}\land\mathit{right\&up}\land\mathit{up\&right}\land\mathit{no\\_change}$

In our reduction, we are interested in grids where a special tile appears
infinitely often in the first column of the grid. The following formula
requires that the special tile appears only in the leftmost column:

$\mathit{tile\\_left}:=p^{\ast}\to\square_{s}(\mathsf{west}\to\square_{h}\mathsf{west})$

All of this completes the necessary requirements for the grid. Now, by adding
a common knowledge modality for all agents, we force all of the aforementioned
formulas to hold everywhere in the grid.

$\Psi_{\mathrm{T}}:=\blacksquare_{\\{h,v,s\\}}\left(\psi_{\mathit{tile}}\land\mathit{adj\\_tiles}\land\mathit{init}\land\psi_{\mathit{x\&y}}\land\mathit{tile\\_left}\right)$

Observe that $\Psi_{\mathrm{T}}$ does not say anything about the special tile
$\tau^{\ast}$ appearing infinitely often in the first column. The formula
merely requires that if there is a special tile, then it should appear in the
first column. We first show that $\Psi_{\mathrm{T}}$ forces a grid-like model,
and only after that will we consider the (in)finite number of occurrences of
the special tile.

######  Lemma 1.

Let $\mathrm{T}$ be an instance of the recurring tiling problem. If
$\mathrm{T}$ can tile $\mathbb{N}\times\mathbb{N}$, then $\Psi_{\mathrm{T}}$
is satisfiable.

###### Proof.

Assume that there is a tiling of the $\mathbb{N}\times\mathbb{N}$ plane with a
finite set of tiles $\mathrm{T}$. We construct model $M=(S,\sim,V)$ satisfying
$\Psi_{\mathrm{T}}$ directly from the given tiling. In particular,

  * •

$S=\mathbb{N}\times\mathbb{N}\times\\{\mathfrak{n},\mathfrak{s},\mathfrak{e},\mathfrak{w},\mathfrak{c}\\}$,

  * •

$\sim_{s}=\\{(i,j,\mathfrak{l}),(i^{\prime},j^{\prime},\mathfrak{l}^{\prime})\mid
i=i^{\prime}\text{ and }j=j^{\prime}\\}$

  * •

$\sim_{v}$ is the reflexive closure of
$\\{(i,j,\mathfrak{n}),(i,j+1,\mathfrak{s})\\}$

  * •

$\sim_{h}$ is the reflexive closure of
$\\{(i,j,\mathfrak{e}),(i+1,j,\mathfrak{w})\\}$

  * •

for all $\tau_{k}\in\mathrm{T}$,
$V(p_{k})=\\{(i,j,\mathfrak{l})\mid\tau_{k}\text{ is at }(i,j)\\}$

  * •

for all $c\in C$, $V(c)=\\{(i,j,\mathfrak{l})\mid\tau(\mathfrak{l})=c\\}$

  * •

for all $l\in\mathsf{Position}$, $V(l)=\\{(i,j,\mathfrak{l})\mid l\text{
corresponds to }\mathfrak{l}\\}$

To argue that $M_{(0,0,\mathfrak{e})}\models\Psi_{\mathrm{T}}$ we first notice
that due to the fact that $\mathrm{T}$ tiles the $\mathbb{N}\times\mathbb{N}$
plane and by the construction of $M$, subformulas of $\Psi_{\mathrm{T}}$ that
do not involve arbitrary announcements are straightforwardly satisfied.

Now, consider the formula $\mathit{up}$. For every $(i,j,\mathfrak{l})$, there
is at most one $(i^{\prime},j^{\prime},\mathfrak{l}^{\prime})$ that is
reachable by taking an $s$-step to a $\mathsf{north}$ state followed by a
$v$-step to a $\mathsf{south}$ state, namely
$(i^{\prime},j^{\prime},\mathfrak{l}^{\prime})=(i,j+1,\mathfrak{s})$.
Furthermore, this property is retained in any submodel of $M$. As a
consequence, in any state of any submodel of $M$, $\lozenge_{\mathit{up}}\chi$
implies $\square_{\mathit{up}}\chi$, for every $\chi$. In particular, it
follows that
$M_{(i,j,\mathfrak{l})}\models[!](\lozenge_{\mathit{up}}\lozenge_{s}\mathsf{centre}\rightarrow\square_{\mathit{up}}\lozenge_{s}\mathsf{centre})$,
i.e., $M_{(i,j,\mathfrak{l})}\models\mathit{up}$.

Similar reasoning shows that $(i,j,\mathfrak{l})$ satisfies the other
conjuncts of $\psi_{x\&y}$. Hence
$M_{(i,j,\mathfrak{l})}\models\psi_{\mathit{tile}}\land\mathit{adj\\_tiles}\land\mathit{init}\land\psi_{\mathit{x\&y}}\land\mathit{tile\\_left}$,
for all $(i,j,\mathfrak{l})$, and thus
$M_{(0,0,\mathfrak{e})}\models\Psi_{\mathrm{T}}$. ∎

The more complex part of the reduction is to show that if $\Psi_{\mathrm{T}}$
is satisfiable, then a tiling exists.

######  Lemma 2.

Let $\mathrm{T}$ be an instance of the recurring tiling problem. If
$\Psi_{\mathrm{T}}$ is satisfiable, then $\mathrm{T}$ can tile
$\mathbb{N}\times\mathbb{N}$.

###### Proof.

Let $M$ be such that $M_{s}\models\Psi_{\mathrm{T}}$. The model $M$ is
partitioned by $\sim_{s}$, we refer to these partitions as grid points, and
label these points as follows.

  * •

The grid point containing $s$ is labelled $(0,0)$.

  * •

If $A$ and $B$ are grid points, $A$ is labelled $(i,j)$ and there is a
$\mathsf{north}$-state in $A$ that is $v$-indistinguishable to a
$\mathsf{south}$-state in $B$, then $B$ is labelled $(i,j+1)$.

  * •

If $A$ and $B$ are grid points, $A$ is labelled $(i,j)$ and there is a
$\mathsf{east}$-state in $A$ that is $h$-indistinguishable to a
$\mathsf{west}$-state in $B$, then $B$ is labelled $(i+1,j)$.

Note that a single grid point might have multiple labels. We say that $(i,j)$
is tiled with $\tau_{i}$ if there is some grid point labelled with $(i,j)$
that contains a state where $p_{i}$ holds. We start by noting that because the
main connective of $\Psi_{\mathrm{T}}$ is $\blacksquare_{\\{h,v,s\\}}$, the
formula holds in every labelled grid point. For every labelled grid point $X$
and every $x\in X$, we therefore have $M_{x}\models\psi_{\mathit{tile}}$. So
$X$ contains states for every direction, each labelled with exactly one colour
that corresponds to the tile that holds on $X$. We continue by proving the
following claim.

Claim 1: Let $X$, $A$ and $B$ be grid points where $X$ is labeled $(i,j)$
while $A$ and $B$ are both labeled $(i,j+k)$ by virtue of being $k$-steps to
the north of $X$. Then $A$ and $B$ are PALC-indistinguishable, in the sense
that for every $\chi\in\mathsf{PALC}$, if there is an $a\in A$ such that
$M_{a}\models\chi$ then there is a $b\in B$ such $M_{b}\models\chi$ (and vice
versa).

Proof of Claim 1: By induction on $k$. As base case, let $k=1$ and suppose
towards a contradiction that, for some $\chi\in\mathsf{PALC}$ and $a\in A$,
$M_{a}\models\chi$ while for every $b\in B$, $M_{b}\not\models\chi$. Consider
then the formula $\mathsf{centre}\rightarrow\lozenge_{s}\chi$. Every
$\mathsf{centre}$ state in $A$ satisfies this formula, while none of the
$\mathsf{centre}$ states in $B$ do. Hence, for every state $x\in X$,
$M_{x}\models[\mathsf{centre}\rightarrow\lozenge_{s}\chi](\lozenge_{\mathit{up}}\lozenge_{s}\mathsf{centre}\land\neg\square_{\mathit{up}}\lozenge_{s}\mathsf{centre})$.
But that contradicts $M_{x}\models\mathit{up}$. From this contradiction, we
prove the base case $k=1$.

Now, suppose as induction hypothesis that $k>1$ and that the claim holds for
all $k^{\prime}<k$. Again, suppose towards a contradiction that
$M_{a}\models\chi$ while $M_{b}\not\models\chi$ for all $b\in B$. Let
$A^{\prime}$ and $B^{\prime}$ be grid points that lie $k-1$ steps to the north
of $X$ and one step to the south of $A$ and $B$, respectively. Then for every
$a^{\prime}\in A^{\prime}$ and $b^{\prime}\in B^{\prime}$,
$M_{a^{\prime}}\models\lozenge_{\mathit{up}}\lozenge_{s}\chi$ and
$M_{b^{\prime}}\models\lozenge_{\mathit{up}}\neg\lozenge_{s}\chi$. By the
induction hypothesis, $A^{\prime}$ and $B^{\prime}$ are indistinguishable, so
$M_{a^{\prime}}\models\lozenge_{\mathit{up}}\lozenge_{s}\chi\wedge\lozenge_{\mathit{up}}\neg\lozenge_{s}\chi$.
But then there are distinguishable grid points one step to the north of
$A^{\prime}$, contradicting the induction hypothesis. From this contradiction,
we prove the induction step and thereby the claim.

Similar reasoning shows that any two grid points $A,B$ that are labeled
$(i+k,j)$ by virtue of being $k$ steps to the right of the same grid point $X$
are indistinguishable. Now, we can prove the next claim.

Claim 2: Let $X$, $A$ and $B$ be grid points, where $X$ is labelled $(i,j)$,
$A$ is labelled $(i+1,j+1)$ by virtue of being above $A^{\prime}$ which is to
the right of $X$, and $B$ is labelled $(i+1,j+1)$ by virtue of being to the
right of $B^{\prime}$ which is above $B$. Then $A$ and $B$ are PALC-
indistinguishable.

Proof of claim 2: Suppose towards a contradiction that for some
$\chi\in\mathsf{PALC}$ and $a\in A$ we have $M_{a}\models\chi$, while
$M_{b}\not\models\chi$ for all $b\in B$. Then for $x\in X$ we have
$M_{x}\models[\mathsf{centre}\rightarrow\lozenge_{s}\chi](\lozenge_{\mathit{right}}\lozenge_{\mathit{up}}\lozenge_{s}\mathsf{centre}\wedge\lozenge_{\mathit{up}}\lozenge_{\mathit{right}}\neg\lozenge_{s}\mathsf{centre})$,
contradicting $M_{x}\models\mathit{right\&up}$.

From Claim 1 it follows that any $A$ and $B$ that are labelled $(i,j)$ by
virtue of being $i$ steps to the right and then $j$ steps up from $(0,0)$ are
PALC-indistinguishable. Claim 2 then lets us commute the “up” and “right”
moves. Any path to $(i,j)$ can be obtained from the path that first goes right
$i$ steps then up $j$ steps by a finite sequence of such commutations. Hence
any grid points $A$ and $B$ that are labelled $(i,j)$ are PALC-
indistinguishable.

The tile formulas $p_{i}$, for every $\tau_{i}\in\mathrm{T}$, are PALC-
formulas, so there is exactly one tile $\tau_{i}$ that is assigned to the grid
point $(i,j)$. Furthermore, $\mathit{state\\_col}$ then guarantees that each
side of a grid point has the colour corresponding to the tile, and
$\mathit{adj\\_tiles}$ guaranteees that the tile colours match. This shows
that if $\Psi_{\mathrm{T}}$ is satisfiable, then $\mathrm{T}$ can tile
$\mathbb{N}\times\mathbb{N}$. ∎

###  3.2 Encoding the Recurring Tile

The final formula that is satisfied in a grid model if and only if a given
tiling has a tile that occurs infinitely often in the first column would be

$\Psi_{\mathrm{T}}\land\blacksquare_{\\{v,s\\}}[\blacksquare_{\\{h,s\\}}\lnot
p^{\ast}]\lnot\Psi_{\mathrm{T}}.$

In other words, the recurring tiling problem can be reduced to the APALC-
satisfiability problem, where the reduction maps the instance
$(\mathrm{T},\tau^{\ast})$ of the recurring tiling problem to the
satisfiability of
$\Psi_{\mathrm{T}}\land\blacksquare_{\\{v,s\\}}[\blacksquare_{\\{h,s\\}}\lnot
p^{\ast}]\lnot\Psi_{\mathrm{T}}$.

Intuitively, the formula states that if we remove all rows with the special
tile, then our model is no longer a grid. See Figure 2, where on the left we
have a grid with the special grey tile $\tau^{\ast}$ appearing infinitely
often in the first column (every other tile in the first column is grey).
Formula $\blacksquare_{\\{h,s\\}}\lnot p^{\ast}$ holds only in those squares
of the grid that lie on rows without the special tile. Thus, announcing
$\blacksquare_{\\{h,s\\}}\lnot p^{\ast}$ removes all rows that has the grey
tile (see the right part of Figure 2). Since the grey tile appears infinitely
often in the original grid, we have to remove an infinite number of rows after
the announcement of $\blacksquare_{\\{h,s\\}}\lnot p^{\ast}$, thus ensuring
that what is left of the original model is not a grid.

Figure 2: Left: An original grid with a special grey tile $\tau^{\ast}$
appearing infinitely often in the first column. Right: The grid after the
public announcement of $\blacksquare_{\\{h,s\\}}\lnot p^{\ast}$. Crossed-out
rows are not preserved after the announcement.

######  Theorem 1.

Let $\mathrm{T}$ be an instance of the tiling problem with a special tile
$\tau^{\ast}\in\mathrm{T}$. Set $\mathrm{T}$ can tile
$\mathbb{N}\times\mathbb{N}$ with $\tau^{\ast}$ appearing infinitely often in
the first column if and only if
$\Psi_{\mathrm{T}}\land\blacksquare_{\\{v,s\\}}[\blacksquare_{\\{h,s\\}}\lnot
p^{\ast}]\lnot\Psi_{\mathrm{T}}$ is satisfiable.

###### Proof.

First, let us can extend the labelling from the proof of Lemma 2 as follows:

  * •

For every $q\in\mathsf{Position}$, if $A$ and $B$ are grid points, $A$ is
labeled $(i,j)$ and there is a $q$ state in $A$ that is $v$ or
$h$-indistinguishable from a $q$ state in $B$, then $B$ is labeled $(i,j)$.

It follows from $\mathit{no\\_change}$ that this extended labelling retains
the property that any two grid points with the same label are PALC-
indistinguishable. Furthermore, from $\mathit{hor}$ and $\mathit{vert}$ it
follows that every grid point that is reachable by $h$, $v$ and $s$ is now
labelled with some coordinates $(i,j)$. Hence we can identify the
$\\{h,v,s\\}$-reachable grid points in any model of $\Psi_{\mathrm{T}}$ with
$\mathbb{N}\times\mathbb{N}$.

Now, assume that set $\mathrm{T}$ cannot tile the $\mathbb{N}\times\mathbb{N}$
plane with a special tile $\tau^{\prime}\in\mathrm{T}$ appearing infinitely
often in the first column. We argue that in this case,
$\Psi_{\mathrm{T}}\land\blacksquare_{\\{v,s\\}}([\blacksquare_{\\{h,s\\}}\lnot
p^{\ast}]\lnot\Psi_{\mathrm{T}})$ is not satisfiable. The first conjunct is
straightforward. If $\mathrm{T}$ cannot tile the $\mathbb{N}\times\mathbb{N}$
plane, then, by Lemma 2, $\Psi_{\mathrm{T}}$ is not satisfiable.

So suppose that $\mathrm{T}$ can tile the plane, but only in such a way that
$\tau^{\ast}$ occurs finitely often. For every model $M_{(0,0,\mathfrak{l})}$
of $\Psi_{\mathrm{T}}$, there is then some $k\in\mathbb{N}$ that is the last
row in which $p^{\ast}$ is true. The formula $\blacksquare_{\\{h,s\\}}\neg
p^{\ast}$ holds exactly on those rows where $p^{\ast}$ does not hold in the
first column. As a result, the update $[\blacksquare_{\\{h,s\\}}\neg
p^{\ast}]$ does not remove any rows past row $k$. The grid points
$\mathbb{N}\times\mathbb{N}_{>k}$ then still form a grid that is isomorphic to
$\mathbb{N}\times\mathbb{N}$, and that is tiled. See Figure 3 for a depiction
of the situation.

It follows that
$M_{(0,k,\mathfrak{l})}\not\models[\blacksquare_{\\{h,s\\}}\neg
p^{\ast}]\neg\Psi_{\mathrm{T}}$, and therefore
$M_{(0,0,\mathfrak{l})}\not\models\blacksquare_{\\{v,s\\}}[\blacksquare_{\\{h,s\\}}\neg
p^{\ast}]\neg\Psi_{\mathrm{T}}$. This is true for every model of
$\Psi_{\mathrm{T}}$, so
$\Psi_{\mathrm{T}}\land\blacksquare_{\\{v,s\\}}[\blacksquare_{\\{h,s\\}}\neg
p^{\ast}]\neg\Psi_{\mathrm{T}}$ is not satisfiable.

If, on the other hand, $\mathrm{T}$ can tile the plane in such a way that
$\tau^{\ast}$ occurs infinitely often in the first column, then there is a
model of $\Psi_{\mathrm{T}}$ where the modality $[\blacksquare_{\\{h,s\\}}\neg
p^{\ast}]$ removes infinitely many rows, and therefore does not leave any
infinite grid. So
$\Psi_{\mathrm{T}}\wedge\blacksquare_{\\{v,s\\}}[\blacksquare_{\\{h,s\\}}\neg
p^{\ast}]\neg\Psi_{\mathrm{T}}$ is satisfiable. ∎

Figure 3: Left: An original grid with a special grey tile $\tau^{\ast}$
appearing finitely often in the first column. Right: The grid after the public
announcement of $\blacksquare_{\\{h,s\\}}\lnot p^{\ast}$. Crossed-out rows are
not preserved after the announcement. A full $\mathbb{N}\times\mathbb{N}$ grid
that is still available after the announcement is depicted with thick lines.

In the construction of $\Psi_{\mathrm{T}}$ and proofs of Lemmas 1 and 2, we
used APALC quantifiers $[!]$. We can prove the similar results for GALC and
CALC quantifers by substituting $[!]$ with $[\\{h,v,s\\}]$ and
$[\\!\langle\\{h,v,s\\}\rangle\\!]$ correspondingly, and substituting
$\mathsf{PALC}$ with $\mathsf{PALC}^{\\{h,v,s\\}}$. We get the hardness result
from the $\Sigma^{1}_{1}$-completeness of the recurring tiling problem [19].

######  Theorem 2.

The satisfiability problem of QPALCs is $\Sigma^{1}_{1}$-hard.

The $\Sigma^{1}_{1}$-hardness of the satisfiability problems of QPALCs
together with the fact that the class of $\Sigma^{1}_{1}$ problems is strictly
greater than the class of co-RE problems [24, Chapter 4] imply that the sets
of validites of the logics are not RE, which, in turn, implies that QPALCs are
not finitely axiomatisable.

######  Corollary 1.

The set of valid formulas of QPALCs is neither RE nor co-RE.

######  Corollary 2.

QPALCs do not have finitary axiomatisations.

##  4 Discussion

The existence of finitary axiomatisations of any of APAL, GAL, and CAL is a
long-standing open problem. In this paper, we have showed that the
satisfiability problem of the logics extended with common knowledge modality
is $\Sigma^{1}_{1}$-hard, and thus they do not admit of finitary
axiomatisations. Table 1 contains the overview of the known results, including
those shown in this paper, and open questions.

| APAL | GAL | CAL | APALC | GALC | CALC
---|---|---|---|---|---|---
Finitary axiomatisation | ? | ? | ? | ✗ (Cor. 2) | ✗ (Cor. 2) | ✗ (Cor. 2)
Infinitary axiomatisation | ✔[7] | ✔[2] | ? | ✔[5] | ✔[5] | ?
Table 1: Overview of the known results and open problems.

It is important to point out that the use of common knowledge is instrumental
in our construction. Arguments from [15, 4] did not rely on common knowledge
to enforce local grid properties globally, and instead the authors used an
agent with the universal relation over the set of states. This approach is
good enough if one wants to demonstrate the existence of a grid-like model.
However, if we also require that the grid satisfies some property, like a
special tile occurring infinitely often in the first column, then the presence
of the global agent makes it harder to ensure this. The problem is that such
an unrestrained relation may access other grids within the same model, and
thus we may end up in the situation when the property is satisfied by a set of
grids taken together and not by any single grid.

Our construction is ‘tighter’ than those in [15, 4]. In particular, our
vertical and horizontal agents can ‘see’ only one step ahead. This guarantees
that we stay within the same grid. In order to force grid properties globally,
we use common knowledge operators that allow us to traverse a given grid-like
model in all directions. It is not yet clear how to have a ‘tight’ grid and
still be able to traverse the model without common knowledge. With this work,
apart from showing that QPALCs are $\Sigma^{1}_{1}$-hard, we also hope to have
elucidated the exact obstacle one has to overcome in order to claim the same
about QPALs.

### Acknowledgements

We would like to thank the three anonymous reviewers for their encouraging
comments and constructive suggestions, which helped us to improve the
presentation of our result.

## References

  * [1]
  * [2] Thomas Ågotnes, Philippe Balbiani, Hans van Ditmarsch & Pablo Seban (2010): _Group announcement logic_.  Journal of Applied Logic 8(1), pp. 62–81, 10.1016/j.jal.2008.12.002.
  * [3] Thomas Ågotnes & Hans van Ditmarsch (2008): _Coalitions and announcements_.  In Lin Padgham, David C. Parkes, Jörg P. Müller & Simon Parsons, editors: Proceedings of the 7th AAMAS, IFAAMAS, pp. 673–680.
  * [4] Thomas Ågotnes, Hans van Ditmarsch & Tim French (2016): _The undecidability of quantified announcements_.  Studia Logica 104(4), pp. 597–640, 10.1007/s11225-016-9657-0.
  * [5] Thomas Ågotnes & Rustam Galimullin (2023): _Quantifying over information change with common knowledge_.  Autonomous Agents and Multi-Agent Systems 37(19), p. 40, 10.1007/s10458-023-09600-1.
  * [6] Robert J. Aumann (1961): _The core of a cooperative game without side payments_.  Transactions of the American Mathematical Society 98(3), pp. 539–552, 10.2307/1993348.
  * [7] Philippe Balbiani, Alexandru Baltag, Hans van Ditmarsch, Andreas Herzig, Tomohiro Hoshi & Tiago de Lima (2008): _‘Knowable’ as ‘known after an announcement’_.  Review of Symbolic Logic 1(3), pp. 305–334, 10.1017/S1755020308080210.
  * [8] Philippe Balbiani & Hans van Ditmarsch (2015): _A simple proof of the completeness of APAL_.  Studies in Logic 8(2), pp. 65–78.
  * [9] Robert L. Berger (1966): _The undecidability of the domino problem_.  Memoirs of the American Mathematical Society, pp. 1–38.
  * [10] Hans van Ditmarsch (2023): _To be announced_.  Information and Computation 292, pp. 1–42, 10.1016/j.ic.2023.105026.
  * [11] Hans van Ditmarsch, Wiebe van der Hoek & Barteld Kooi (2008): _Dynamic epistemic logic_.  Synthese Library 337, Springer, 10.1007/978-1-4020-5839-4.
  * [12] Hans van Ditmarsch, Wiebe van der Hoek, Barteld Kooi & Louwe B. Kuijer (2017): _Arbitrary arrow update logic_.  Artificial Intelligence 242, pp. 80–106, 10.1016/j.artint.2016.10.003.
  * [13] Ronald Fagin, Joseph Y. Halpern, Yoram Moses & Moshe Vardi (1995): _Reasoning about knowledge_.  The MIT Press.
  * [14] Jie Fan (2016): _Removing your ignorance by announcing group ignorance: a group announcement logic for ignorance_.  Studies in Logic 9(4), pp. 4–33.
  * [15] Tim French & Hans van Ditmarsch (2008): _Undecidability for arbitrary public announcement logic_.  In Carlos Areces & Robert Goldblatt, editors: Proceedings of the 7th AiML, College Publications, pp. 23–42.
  * [16] Rustam Galimullin (2019): _Coalition announcements_.  Ph.D. thesis, University of Nottingham, UK.
  * [17] Rustam Galimullin (2021): _Coalition and relativised group announcement logic_.  Journal of Logic, Language and Information 30(3), pp. 451–489, 10.1007/s10849-020-09327-2.
  * [18] David Harel (1985): _Recurring dominoes: making the highly undecidable highly understandable_.  In Marek Karpinski & Jan van Leeuwen, editors: Topics in the Theory of Computation, North-Holland Mathematics Studies 102, North-Holland, pp. 51–71, 10.1016/S0304-0208(08)73075-5.
  * [19] David Harel (1986): _Effective transformations on infinite trees, with applications to high undecidability, dominoes, and fairness_.  Journal of the ACM 33(1), pp. 224–248, 10.1145/4904.4993.
  * [20] Louwe B. Kuijer (2015): _Unsoundness of $R$($\square$)_.  Manuscript.  Available at https://personal.us.es/hvd/APAL_counterexample.pdf.
  * [21] Louwe B. Kuijer (2017): _Arbitrary arrow update logic with common knowledge is neither RE nor co-RE_.  In Jérôme Lang, editor: Proceedings of the 16th TARK, EPTCS 251, pp. 373–381, 10.4204/EPTCS.251.27.
  * [22] John-Jules Ch. Meyer & Wiebe van der Hoek (1995): _Epistemic logic for AI and computer science_.  Cambridge Tracts in Theoretical Computer Science 41, CUP, 10.1017/CBO9780511569852.
  * [23] Joseph S. Miller & Lawrence S. Moss (2005): _The undecidability of iterated modal relativization_.  Studia Logica 79(3), pp. 373–407, 10.1007/s11225-005-3612-9.
  * [24] Piergiorgio Odifreddi (1989): _Classical recursion theory_.  Studies in Logic and the Foundations of Mathematics 142, Elsevier.
  * [25] Marc Pauly (2002): _A modal logic for coalitional power in games_.  Journal of Logic and Computation 12(1), pp. 149–166, 10.1093/logcom/12.1.149.
  * [26] Jan Plaza (1989): _Logics of public communications_.  In: Proceedings of the 4th ISMIS, Oak Ridge National Laboratory, pp. 201–216.