Small Undecidable Problems in Epistemic Planning

1 Introduction

Developing autonomous agents is central in artificial intelligence. Agents should be able to plan their actions for achieving a goal, and to reason about their knowledge and other agents' knowledge. Epistemic planning [Baral et al., 2017] focuses on generating plans in a multi-agent context. Goals can be epistemic (for instance, the goal could be that "agent a knows that agent b does not know p"). Some actions can change the physical world as well as the knowledge of agents. Typical actions are public actions where both knowledge and physical changes are commonlyknown by the agents [Kominis and Geffner, 2015]. Traditionally, goals are expressed in epistemic logic (the goal above is expressed by formula Ka¬Kbp). On top of the classical planning setting with pre/post-conditions for actions, the Dynamic Epistemic Logic [van Ditmarsch et al., 2007; Bolander, 2017] framework offers a representation of knowledge change: actions are graphs [Baltag et al., 1998] whose nodes are events (with pre/post-conditions) while edges denote epistemic relations.

In this setting, the epistemic planning problem consists in finding a sequence of actions leading to an epistemic state satisfying the goal. The problem is undecidable in general; there are several proofs in the literature, by reducing either the halting problem of Turing machines [Bolander and Andersen, 2011], or of two-counter machines [Aucher and Bolander, 2013; Charrier et al., 2016]. Unfortunately, none of these proofs exhibit bounds to parameters (number of actions, number of propositions, etc.) involved in the problem.

In order to bound the parameters, we suggest to focus on one-dimensional three-neighbor cellular automata [von Neumann, 1951]. First, small universal cellular automata [Smith, 1968; Wolfram, 2002] have been exhibited. Second, DEL and cellular automata share theoretical features. On the one hand, all cells in a cellular automaton update their own state (called symbol later) synchronously according to a local rule. On the other hand, knowledge update in DEL consists in synchronously applying pre/post-conditions (that are local properties in epistemic logic) in several possible worlds.

Our first contribution is to take advantage of small universal cellular automata with a blank background (almost all cells' symbols except finitely many are ) to provide a small class of instances for the epistemic planning problem that is already undecidable (see Corollary 1). Interestingly, the repertoire of actions (made up of one action) and the goal are both fixed, only the initial knowledge state is part of the input.

Whereas public actions lead to decidability in epistemic planning [Kominis and Geffner, 2015; Belardinelli et al., 2017], the second contribution is that public actions are enough for undecidability when the initial knowledge state is automatic [Blumensath and Grädel, 2000] (the gap between finite and automatic for structures is analogous to the gap between finite and regular for languages). This result is quite surprising since leaping from finite to automatic structures usually maintains decidability, for instance for firstorder model checking. More surprisingly, undecidability is obtained for a very small class of instances (see Corollary 2) by taking advantage of Wolfram's Rule 110.

In a last contribution, we show how to remove the common knowledge operator from goal formulas (Corollaries 3 and 4).

The paper is organized as follows. We first recall the DEL setting and the epistemic planning problem in Section 2. Sections 3 and 4 are dedicated to the proofs of our two undecidability results and contain the material on cellular automata. Finally, Section 5 outlines the proof that common knowledge can be avoided in the goal formulas.

2 Background on Epistemic Planning

Knowledge states A knowledge state is a pointed Kripke model that describes an epistemic situation. In few words, it is a graph whose vertices are possible worlds with a distinguished world w0. In the literature, such models are often denoted byM,w0, but here, we write them S for "states"; for ease of notation, we will improperly write the ordered pair (S, w) to denote state S whose actual world w0 has been replaced with w. Let Ag be a finite set of agents and AP be a countable set of propositions.

Definition 1 A state S = (W, (Ra)a∈Ag, V, w0) is defined by a non-empty set W of epistemic worlds, equivalence relations Ra ⊆ W×W called epistemic relations, a valuation function V : W → 2AP , and a world w0 ∈ W called the actual world.

In Definition 1, the valuation function V is a labeling for the worlds. The intuitive meaning of the epistemic relations is: wRaw′ holds 1 if agent a considers world w′ as possible in world w. The assumption of epistemic relations being equivalence relations is referred to as S5 [Chellas, 1980].

Consider the state S = (W, (Ra)a∈Ag, V, w0) where W = {w0, w}, Ra = Rb = W×W, V (w0) = {p}, and V (w) = ∅. This state has 2 agents and 1 proposition, and is depicted in Figure 1a, with the convention that the pointed world is in a double circle and equivalent worlds are linked with plain lines (in order to lighten the pictures, loops are omitted). In the epistemic situation described by S, agents a and b do not distinguish w0 from w, and therefore do not know that p holds.

Epistemic language The language LEL extends the propositional language with epistemic modal operators and is defined by: ϕ ::= ⊤ | p | ¬ϕ | (ϕ ∨ ϕ) | Kaϕ | CGϕ, with p ∈ AP, a ∈ Ag, G ⊆ Ag. Formula Kaϕ is read "agent a knows that ϕ holds" and formula CGϕ is read "ϕ is commonly known among agents in G". We define the usual abbreviations (ϕ1 ∧ ϕ2) for ¬(¬ϕ1 ∨ ¬ϕ2), ˆKaϕ for ¬Ka¬ϕ

1 This is a standard notation for (w, w′ ) ∈ Ra.

and ˆ CGϕ for ¬CG¬ϕ. The semantics of LEL is defined by induction over the formula (Boolean cases are omitted).

• (W, (Ra)a∈Ag, V, w) |= p if p ∈ V (w);
• (W, (Ra)a∈Ag, V,w) |=Kaϕ if for all w′ s.t. wRaw′ , (W, (Ra)a∈Ag, V, w′ ) |= ϕ;
• (W, (Ra)a∈Ag, V,w) |= CGϕ if for all w′ s.t. w (⋃a∈G Ra )∗ w′ , (W, (Ra)a∈Ag, V,w′ ) |= ϕ

where (⋃a∈G Ra )∗ is the reflexive and transitive closure of the union of the Ra for a ∈ G.

Actions Actions are modeled by so-called pointed event models 2 [van Ditmarsch et al., 2007]. They are graphs whose nodes are events with a distinguished event e0 that represents the real event taking place (in the current world) when action A is executed. In more formal words:

Definition 2 An action A = (E, (Ra)a∈Ag, pre, post, e0) is given by a non-empty finite set of events E, equivalence relations (Ra)a∈Ag ⊆ E×E, a precondition function pre : E → LEL, a postcondition function post : E ×AP → LEL and an event e0 ∈ E called the current event.

The precondition function defines under which condition an event can take place. The postcondition decribes the effect of an event on the world: after an event e has taken place, the truth of p is assigned to the value post(e, p). Actions made up of a single event (card(E) = 1) are public actions. Figure 1b shows the action A where E = {e0, e}, Ra = E × E, Rb = {(e0, e0), (e, e)}, pre(e0) = p, pre(e) = ⊤, post(e0, q) = ⊤ and post(e, r) = ⊤. In figures and formal definitions, when a postcondition post(e, p) is omitted, we mean that post(e, p) = p.

Product The update of a state S by an action A is a new state written S ⊗A and defined as a product.The product is defined only if the current event in A can take place, namely its precondition holds in the current world of S.

Definition 3 Let S = (W, (Ra)a∈Ag, V,w0) be a state and A = (E, (Ra)a∈Ag, pre, post, e0) be an action. If S |= pre(e0), we define the product of S and A as the state S ⊗ A = (W ′ , (Ra)′ , V ′ , (w, e0)) where:

• W ′ = {(w, e) ∈ W ×E | (S, w) |= pre(e)};
• (w, e)R′a (w′ , e′ ) iff wRaw′ and eRae′ ;
• V ′ ((w, e)) = {p ∈ AP | (S, w) |= post(e, p)}.

Figure 1c shows the product S ⊗ A of state S of Figure 1a and action A of Figure 1b. For instance, formula Kb(p ∧ q ∧Ka(¬q → r)) holds in state S ⊗A. In the following, the expression S⊗A1, . . . ,Am is a concise notation for (. . . ((S ⊗A1) ⊗A2) · · · ⊗Am).

The epistemic planning problem introduced by [Bolander and Andersen, 2011] can now be defined.

2 In the literature, pointed event models are often denoted by E, e. We also decided to simplify the notations and to call them actions.

Definition 4 (Epistemic planning problem)

• input: a state S, a finite set of actions A and a formula ϕ ∈ LEL;
• output: yes if there exists a sequence of actions (a plan) A1, . . . ,Am ∈ A such that S ⊗A1, . . . ,Am |= ϕ; no otherwise.

3 Small Epistemic Planning Problems

In this section, we show the undecidability of two restrictions of the epistemic planning problem, where A is fixed and no longer part of the input. Undecidability is proven by reduction from undecidable reachability problems on cellular automata. From now on throughout the paper, Ag = {a, b}; recall that all models (i.e. states and actions) are S5 (epistemic relations are equivalence relations).

3.1 Universal 1DCellular Automata

In this article, we only consider one-dimensional threeneighbor cellular automata. An infinite sequence of cells are settled on a line; each cell is in a state represented by a symbol 3 of a finite alphabet Σ. Given a cell, a transition function f maps a three-neighbor (left-cell symbol, current symbol, right-cell symbol) to the new symbol of the cell.

Definition 5 A cellular automaton is a pair A = (Σ, f) where Σ is a finite alphabet and f : Σ3 → Σ is a transition function.

Example 1 (Rule 110 [Wolfram, 2002]) The Rule 110 cellular automaton is the two-symbol cellular automaton AR110 = ({0, 1}, f110) where f110 is defined by the Boolean formula f110(x, y, z) := (x ∧ y ∧ ¬z) ∨ (x ∧ ¬y ∧ z) ∨ (¬x ∧ y ∧ z) ∨ (¬x ∧ y ∧ ¬z) ∨ (¬x ∧ ¬y ∧ z).

A configuration, that is the symbols of cells on an infinite line, is modeled by an infinite word c ∈ ΣZ , that is, a map that assigns a symbol c[i] to any integer i ∈ Z. A computation step is performed by the following rule.

Definition 6 Given a cellular automaton A, given an infinite word c ∈ ΣZ , we define the successor of c by A to be the infinite word c′ defined by c′ [i] := f(c[i - 1], c[i], c[i + 1]). We write c →A c′ .

Figure 2 shows the transition function f110 graphically and some successive configurations.

3 We use 'symbol' instead of 'cell state', to avoid confusion with a knowledge state.

A cellular automaton is deemed universal if it can simulate any Turing machine; the quest for finding such small universal cellular automata started in the 1960s. A common hypothesis is to assume a blank background: we consider that alphabets always contain a special symbol and that transition functions map to . Furthermore, we assume that configurations are finite, in the sense that almost all cell symbols are except a finite number - configurations are of the form ω α ω where α is a finite word, called the support of the configurations. Starting from a finite configuration only leads to finite configurations.

Smith proved that any m-symbol n-state Turing machine can be simulated by a one-dimensional (m + 2n)-symbol 4 3-neighbor cellular automaton with a blank background (see Theorem 4 in [Smith, 1968]). As Minsky constructed a 4symbol 7-state universal Turing machine MMinsky [Minsky, 1967], there exists a 4+2×7 = 18-symbol universal cellular automaton ASmith = (ΣSmith, fSmith), that simulates MMinsky. As a consequence, we obtain the following undecidability result for the reachability problem for ASmith with blank background.

Theorem 1 There exists a finite word 5 hSmith such that it is undecidable to determine, given a finite word α, whether ω α ω →∗ASmith c where the configuration c contains the pattern hSmith.

3.2 Finite Linear States

The main result of this section is Corollary 1 which provides bounds to the parameters of the epistemic planning problem. This is achieved by simulating executions of cellular automata with blank background. First of all, we introduce sufficiently many propositions to encode symbols of the alphabet. Typically, for alphabet ΣSmith with 18 symbols that we respectively write ℓ0, ℓ1, . . . , ℓ17, only 5 propositions p1, . . . , p5 suffice. Given a symbol ℓ, we note enc(ℓ) the encoding of ℓ: enc(ℓ0) = ¬p1 ∧ . . . ¬p5, enc(ℓ1) = p1 ∧ ¬p2 . . . ¬p5, etc. W.l.o.g., we suppose that symbol is ℓ0 and is encoded by the valuation making all pi's false. In the rest, ⃗ p denotes the sequence of propositions pi's.

Now, we encode the finite supports of configurations by means of finite linear states - such states appear in real epistemic puzzles such as the consecutive number puzzle [van Ditmarsch and Kooi, 2015]. They are states of the form In = ({-n, . . . , -1, 0, 1, . . . n}, (Ra)a∈Ag, V, 0) with odd n and:

1. Ra = {(k, k) | k ∈ J1; nK} ∪{(2k, 2k + 1), (2k + 1, 2k) | -n+1 2 ≤ k ≤ n-1 2 };

1. ♥ ∈ V (k) iff k is even;
2. for all i, pi ̸∈ V (-n), V (-n+1), V (n-1), V (n).

A finite linear state In encodes a finite configuration c whose support is of length smaller than 2n - 3 when V (k)

4 Referred to as (m+ 2n)-state in [Smith, 1968].

5 According to the notation of Table 14.8-1 p. 279 in [Minsky, 1967], word hSmith is q30.

makes enc(ℓi) true iff c[k] = ℓi; we require that the two terminal (-n and n) and the two pre-terminal (n - 1, -n + 1) worlds encode (Condition 4). For instance, the ASmith configuration ω ℓ9ℓ5ℓ2 ω where c[-1] = 9 can be represented by:

Given a finite word α, let us set once and for all what finite linear state Sα will encode α: substituting α m for α with m ∈ {0, 1, 2, 3} so that |α| be congruent to 3 modulo 4, we set Sα = (I |α|+3 2 , (Ra)a∈Ag, V, 0) where V (k- |α|-1 2 ) makes enc(ℓi) true iff α[k] = ℓi for 0 ≤ k ≤ |α| - 1, and makes enc( ) true outside of this range. These are only technicalities ensuring a sufficiently large odd index for the interval state to respect constraints with a pseudo-centered word.

3.3 Simulating Cellular Automata in DEL

We define action F mimicking one computation step of the cellular automaton: if S is a finite linear state encoding a configuration c, then S ⊗F is (isomorphic to) a finite linear state encoding the successor of c.

Action F is partially given by Figure 3. Intuitively, the actual event e0 copies every non-terminal world; event e-1 keeps the left-tip world, while e-2 and e-3 clone it to append two new worlds to the left. Events e1, e2, e3 play a similar part. In the end, action F adds two new worlds on each side, while preserving the canonical knowledge state structure that we aim for, including the tips' asymmetry relatively to the agents.

We finish the definition of F by adding postconditions for pj's, corresponding to the application of a transition function f. Suppose w.l.o.g. that ♥ holds in a given world k ∈ {-n+1, . . . , n-1}. Bits of c[k - 1] are obtained by taking the b-transition from the ¬♥-world of world k. They are: 〈 ˆKb(¬♥∧pi)〉i. In the same way, the values of ⃗ p in world k+1 are given by the vector 〈 ˆKa(¬♥∧pi)〉i. The case where ♥ does not hold in the current world is symmetric. We model f by Boolean formulas fj(⃗ p -, ⃗ p, ⃗ p +) over three sequences of atomic propositions ⃗ p - (left cell symbol), ⃗ p (middle cell symbol), ⃗ p + (right cell symbol) that return the value of the j th bit of the new symbol at the middle cell. Bits of the new symbol are: 〈fj(⃗ p -, ⃗ p, ⃗ p +)〉j .

The postconditions for pj's in F is thus defined as follows. First, post(ek)(pj) = ⊥ for all k ̸= 0. Only e0 effectively applies f and post(e0)(pj) is formula

We will refer to FSmith for the action model that corresponds to the transition function fSmith of the cellular automaton ASmith.

On top of proposition ♥, when considering the particular cellular automaton ASmith, we need no more than 5 extra propositions to encode all symbols of alphabet ΣSmith of cardinal 18, so that an overall set of 6 propositions suffices.

Now, we define formulas encoding the occurrence of a pattern h in the configuration. We first define the formula wenc(h) := wenc♥(h) ∨ wenc¬♥(h) where formulas wenc♥(h) and wenc¬♥(h) are inductively defined by:

• wenc♥(ϵ) = ♥ and wenc¬♥(ϵ) = ¬♥;
• for all letters ℓ, wenc♥(ℓh)=♥∧enc(ℓ)∧ ˆKawenc¬♥(h);
• for all letters ℓ, wenc¬♥(ℓh)=¬♥∧enc(ℓ)∧ ˆKbwenc♥(h).

We can now state the following theorem that derives from our ability to simulate the behavior of the cellular automaton ASmith and the use of the dual of the common knowledge operator ˆ CAg to search over a finite linear state for the pattern wenc(hSmith).

Theorem 2 Given a finite linear state S over 6 propositions, it is undecidable to determine whether or not a state satisfying ˆ CAgwenc(hSmith) is reachable from S by executing a finite sequence of actions FSmith.

PROOF.

By reduction from the undecidable reachability problem of Theorem 1. An instance α of the latter is translated into Sα.

■Corollary 1 The epistemic planning problem over 2-agent S5 finite models is undecidable, even if the repertoire is {FSmith}, the goal is ˆ CAgwenc(hSmith) and we only use at most 6 different propositions.

The interested reader can run simulations in DEL of cellular automata using the online software Hintikka's world [Schwarzentruber, 2018] available at the following address: http://hintikkasworld.irisa.fr.

4 Epistemic Planning over Infinite States

We extend the epistemic planning problem to structures that can be infinite, but which can be fully described by a finite presentation, in the sense of automatic structures [Blumensath and Grädel, 2000].

Automatic structures should be understood as all logical structures whose domain and relations can be represented by an encoding in some regular finite-word language and (multitape) synchronous 6 finite-state automata operating on said encoding, respectively.

In our setting, we let a state S = (W, (Ra)a∈Ag, V, w0) be automatic if the following holds 7 .

6 All heads of the tapes progress synchronously, provided the inputs have been "aligned" with a technical trick.

7 We take the convention to use letter B for (multi-tape) finitestate automata.

• W can be encoded as a regular language, hence accepted by some one-tape finite-state automaton BW over some alphabet;
• both relations Ra and Rb are characterized by some twotape automata Ba and Bb respectively: for two finite words η and ζ accepted by BW (henceforth, they are encodings of two worlds wη and wζ) of S, the pair (η, ζ) is accepted by the two-tape automaton Ba if, and only if, wηRawζ (similarly for Bb);
• for each proposition p ∈ AP, there is a one-tape automaton Bp accepting exactly words η s. th. p ∈ V (wη).

If the word η encodes world w0, the tuple (BW, (Ba)a∈Ag, (Bp)p, η) is called an automatic presentation of (W, (Ra)a∈Ag, V,w0). We can now introduce the following epistemic planning problem.

Definition 7 The epistemic planning problem over automatic structures is the following.

• input: an automatic presentation of a state S, a finite set of actions A and a formula ϕ;
• output: yes if there exists a sequence of actions (a plan) A1, . . . ,Am ∈ A such that S ⊗A1, . . . ,Am |= ϕ; no otherwise.

In order to prove this problem to be undecidable, we first recall a well-known result on universal cellular automata with periodic background.

4.1 Cellular Automata with Periodic Background

In an attempt to reduce the number of possible cell symbols of universal cellular automata as introduced in Section 3, the notion of periodic background was introduced: a periodic background is of the form αω βγ ω , where α, β, γ ∈ Σ∗ and |α|, |γ| > 1.

Lindgren and Nordahl exhibited a 7-symbol universal cellular automaton [Lindgren and Nordahl, 1990]. Their results were subsumed by Wolfram's AR110 cellular automaton with only 2 symbols [Wolfram, 2002]. Automaton AR110 displays complex behaviors, and more importantly, is universal [Cook, 2008; 2004; Sutner, 2003]. As stated in [Larsson, 2013] (Th. 5.1), the following reachability problem is undecidable.

Theorem 3 ([Cook, 2008]) Given three finite words α, β, γ ∈ {0, 1}∗ with |α|, |γ| ≥ 1, deciding whether αω βγ ω →∗AR110 c where c contains the finite word hR110 = 01101001101000 is undecidable.

We now explain how the behavior of AR110 can be simulated in DEL. We first show how to represent configurations by infinite linear states.

4.2 Infinite Linear States

To represent infinite configurations of cellular automata, we introduce infinite linear states that are states Z = (Z, (Ra)a∈Ag, V, 0) where:

• Ra = {(k, k), (2k, 2k + 1), (2k + 1, 2k) | k ∈ Z};
• Rb = {(k, k), (2k, 2k - 1), (2k - 1, 2k) | k ∈ Z};
• ♥ ∈ V (k) iff k is even.

For a configuration (a two-way infinite word) c ∈ {0, 1}Z , we define Sc to be the infinite linear state such that p ∈ V (k) iff c[k] = 1. For example, consider the infinite word (100)ω 110(100)ω , where word 110 in the middle is anchored in 0, namely, σ[0] = 1, σ[1] = 1, σ[2] = 0. Its corresponding infinite linear state 8 S(100)ω 110(100)ω has the form (with the convention that we do not draw self-loops):

. . .

. . .

Proposition 1 Given three finite words α, β, γ ∈ {0, 1}∗ with |α|, |γ| ≥ 1, Sαω βγω is automatic and has an effectively computable automatic presentation.

We now turn to simulating the dynamics of AR110 which will entail Theorem 4.

4.3 Epistemic Planning over Automatic Structures

The simulation of the cellular automaton AR110 (see Definition 1) over the configuration αω βγ ω follows the spirit of Section 3, but by simplifying action F since linear states are infinite: the initial configuration of AR110 is represented by the infinite linear state Sαω βγω. The application of f110 to each cell is simulated by executing the public action FR110 consisting of a single event eR110 with pre(eR110) = ⊤ and whose postcondition reflects f110 and leaves ♥ unchanged.The postcondition of eR110 is a 'single-bit' version of the postcondition for event e0 for action F of Section 3, as only one proposition is involved. post(eR110)(p) is:

It is easy to see that the reachability problem for the cellular automaton AR110 over a periodic background (given an initial periodic background αω βγ ω , does there exist a reachable configuration c that contains the finite word hR110?) can be rephrased as the epistemic planning problem over input (Sαω βγω, {FR110}, ˆ CAg(wenc(hR110))).

Theorem 4 Given an automatic presentation of an infinite linear state S (that requires only the 2 propositions ♥ and p), it is undecidable to know whether or not some state satisfying ˆ CAgwenc(hR110) can be reached by executing finitely many times the public action FR110.

PROOF.

We show a reduction from the undecidable reachability problem of Theorem 3. An instance (α, β, γ) of the latter is effectively translated into an automatic presentation of Sαω βγω thanks to Proposition 1. ■

By Theorem 4, where only 1 public action (FR110) and 2 propositions (♥ and p) were involved, we get the following corollary.

Corollary 2 The epistemic planning problem over automatic 2-agent S5 models is undecidable, even if the repertoire is fixed to 1 public action, the goal is fixed to ˆ CAgwenc(hR110) and if we use at most 2 different propositions.

8 We deliberately forget the word's anchor in our notation.

5 Common Knowledge Elimination

In this section, we explain how to remove the dual common knowledge operator ˆ CAg from the two goal formulas. Since the halting word (hSmith or hR110) can be far from the actual world, the basic idea is to apply shifts (whether rightward or leftward) so that the window of the halting word is at the actual world. It can then be checked by a ˆ CAg-free goal formula. Any new plan (if any) will then be comprised of an old plan mingled with a shifting phase (i.e. a sequence of shifts).

We sketch a proof for finite states in Section 5.1, and then proceed in a similar fashion with infinite ones in Section 5.2.

5.1 Finite States

We wish to clearly express the epistemic planning problem with common knowledge associated to Smith's cellular automaton (EPCSmith). As we only consider ASmith with its DEL simulation as described in Section 3.3, both the checked goal formula ( ˆ CAgwenc(hSmith)) and the set of actions ASmith (= {FSmith}) are fixed, and so is the set of 6 propositions; the only input is the initial state Sα, which depends on finite word α, as defined in the aforementioned section.

Now, we will define the epistemic planning problem without common knowledge associated to Smith's cellular automaton (EPKSmith), where the goal formula is now merely wenc(hSmith) and the new set of actions A′Smith will also be fixed, with the intent to reduce EPCSmith to EPKSmith. Incidentally, the initial input state will be the same.

We enrich the set of actions ASmith of the initial DEL model: we choose to set A′Smith = {FSmith,RSmith,LSmith}; the two new actions are defined below:

• RSmith (right shift) is defined by the same structure as FSmith is, except for the following postconditions on event e0:for all i, pi's assignement is replaced with pi := (♥∧ ˆKb(¬♥∧ pi)) ∨ (¬♥∧ ˆKa(♥∧ pi));
• LSmith (left shift) is akin to RSmith; let us just give the postcondition for pi on e0 since nothing else differs: pi := (♥∧ ˆKa(¬♥∧ pi)) ∨ (¬♥∧ ˆKb(♥∧ pi)).

This construction amounts to allowing nondeterministic shifts at any time, while still enforcing growth of the state in order to avoid information overflow on each side. We can now state the following theorem.

Theorem 5 EPCSmith reduces to EPKSmith.

In a nutshell, the proof relies on the two following lemmas; here and later, we use the exponent and update product notations somewhat freely to indicate iterating some action application, as there is no ambiguity.

Lemma 1 If S is a finite linear state 9 , then, for all n ∈ N, (S, k) |= wenc(hSmith) iff (S ⊗RnSmith , k +n) |= wenc(hSmith) iff (S ⊗LnSmith , k -n) |= wenc(hSmith).

9 Recall that terminal and pre-terminal worlds encode ; this property - which is an invariant - guarantees that there is no information loss about non-blank symbols after any shift, since actions RSmith and LSmith are designed in such a way that only those worlds' encodings cannot be transferred.

Lemma 2 If S is a finite linear state, then S⊗RSmith⊗FSmith is isomorphic to S⊗FSmith⊗RSmith; the result still holds when replacing LSmith for RSmith.

Now, any plan in EPCSmith can be completed to a plan in EPKSmith: indeed, if (Sα ⊗ π, k) |= wenc(hSmith) where π is a plan in EPCSmith, then, by Lemma 1, if k ≥ 0, π ⊗ LkSmith is a plan in EPKSmith, and if k < 0, π ⊗R-k Smith is a plan in EPKSmith.

Conversely, given a plan π in EPKSmith, Lemma 2 allows us to change its order to get an equivalent plan made up of π′ with no shifts catenated with a sequence of shifts; using Lemma 1, we assert that π′ is a plan for EPCSmith.

Since we enriched the initial DEL model with exactly 2 actions, we have the following corollary.

Corollary 3 The epistemic planning problem over finite linear initial states with 6 atomic propositions, with the fixed set of actions {FSmith, LSmith,RSmith}, and the fixed goal wenc(hSmith) is undecidable.

5.2 Infinite States

We now turn to the Rule 110 cellular automaton with the same mindset: the epistemic planning problem with common knowledge associated to the Rule 110 cellular automaton EPCR110 relies on the simulation of Section 4, where AR110 = {FR110}, AP = {♥, p} and the goal formula is ˆ CAgwenc(hR110). Recall that the input (α, β, γ) defines initial state Sαω βγω .

Problem EPKR110 will have wenc(hR110) as its goal formula and the remainder of its setting will be that of EPCR110, while its fixed set of actions is A′R110 = {FR110,LR110,RR110}. As states are infinite linear states, these two shifting actions can be defined as public actions:

• RR110 (right shift) is a public action whose single event precondition is ⊤ and whose postcondition for p is p := (♥∧ ˆKb(¬♥∧ p)) ∨ (¬♥∧ ˆKa(♥∧ p));
• LR110 (left shift) is akin to RR110; let us just give the postcondition for p since nothing else differs: p := (♥∧ ˆKa(¬♥∧ p)) ∨ (¬♥∧ ˆKb(♥∧ p)).

Theorem 6 EPCR110 reduces to EPKR110.

Informally, the proof of Theorem 6 can be viewed as a fairly straightforward deduction from the demonstration of Theorem 5, through a projection of finite linear states onto infinite ones, while reinterpreting FR110, RR110 and LR110 as pruned versions of FSmith, RSmith and LSmith respectively, and adjusting propositions to the Rule 110 setting.

Notice that in the previous construction, both RR110 and LR110 are public actions as well as FR110, which gives us the following corollary.

Corollary 4 The epistemic planning problem over automatic structures with 2 atomic propositions, with the fixed set of public actions {FR110,LR110,RR110}, and the fixed goal wenc(hR110) is undecidable.

Notice that actions FR110 and RR110 can be merged (so that the final phase of any successful plan is some - possibly empty - sequence of left shifts), although we did not proceed with this optimization here for the sake of clarity.

6 Conclusion

This work makes a connection between epistemic planning in DEL and cellular automata. We claim that many other similar undecidability results could be transferred to epistemic planning. Decidability techniques (see [Codd, 1968]) could be of use for finding decidable cases and for sharpening the decidability/undecidability frontier of epistemic planning.

Acknowledgments

We thank Maurice Margenstern for email discussions about Lindgren and Nordhal's cellular automaton. We are also grateful for our reviewers' helpful remarks.