# small_undecidable_problems_in_epistemic_planning__fbdf4dcd.pdf

Small Undecidable Problems in Epistemic Planning

Sébastien Lê Cong1, Sophie Pinchinat1, François Schwarzentruber1

1 Univ Rennes, CNRS, IRISA sebastien.le-cong@irisa.fr, sophie.pinchinat@univ-rennes1.fr, francois.schwarzentruber@ens-rennes.fr

Epistemic planning extends classical planning with knowledge and is based on dynamic epistemic logic (DEL). The epistemic planning problem is undecidable in general. We exhibit a small undecidable subclass of epistemic planning over 2-agent S5 models with a fixed repertoire of one action, 6 propositions and a fixed goal. We furthermore consider a variant of the epistemic planning problem where the initial knowledge state is an automatic structure, hence possibly infinite. In that case, we show the epistemic planning problem with 1 public action and 2 propositions to be undecidable, while it is known to be decidable with public actions over finite models. Our results are obtained by reducing the reachability problem over small universal cellular automata. While our reductions yield a goal formula that displays the common knowledge operator, we show, for each of our considered epistemic problems, a reduction into an epistemic planning problem for a common-knowledge-operatorfree goal formula by using 2 additional actions.

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).

Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence (IJCAI-18)

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 by M, 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: w Raw holds1 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].

(a) A state.

post : q :=

pre : post : r :=

(b) An action.

(c) Product.

Figure 1: A state, an action and their product.

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 ϕ

1This 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. w Raw , (W, (Ra)a Ag, V, w ) |= ϕ;

(W, (Ra)a Ag, V, w) |= CGϕ if for all w s.t. w S a G Ra w , (W, (Ra)a Ag, V, w ) |= ϕ

where S 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 models2 [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 w Raw and e Rae ;

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.

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

Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence (IJCAI-18)

. . . 1 0 1 1 1 1 0 1 0 . . .

. . . 1 1 1 0 0 1 1 1 0 . . .

. . . 1 0 1 0 1 1 0 1 1 . . .

. . . 1 1 1 1 1 1 1 1 0 . . .

Figure 2: Rule 110 transition function (f110(1, 0, 1) = 1, etc.) and some successive configurations.

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 1D Cellular 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 symbol3 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.

3We 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)-symbol4 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, f Smith), 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 word5 h Smith such that it is undecidable to determine, given a finite word α, whether

ωα ω ASmith c where the configuration c contains the pattern h Smith.

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; n K} (2k, 2k + 1), (2k + 1, 2k) | n+1

2. Rb = {(k, k) | k J1; n K} (2k, 2k 1), (2k 1, 2k) | n+1

3. V (k) iff k is even; 4. 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)

4Referred to as (m + 2n)-state in [Smith, 1968]. 5According to the notation of Table 14.8-1 p. 279 in [Minsky, 1967], word h Smith is q30.

Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence (IJCAI-18)

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:

0 1 2 3 1 2 3 b a b a b a

, p1, p3 p2 p1, p4

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.

e0 e 1 e 2 e 3 e1 e2 e3 b a b a b a

pre: ˆKa ˆKb pre: ˆKa pre: ˆKa pre: ˆKa pre: ˆKb pre: ˆKb pre: ˆKb post: := post: :=

Figure 3: Skeleton of action F.

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 jth 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 fj( ˆKb( pi) i, p, ˆKa( pi) i) fj( ˆKa( pi i), p, ˆKb( pi) i) .

We will refer to FSmith for the action model that corresponds to the transition function f Smith 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(h Smith).

Theorem 2 Given a finite linear state S over 6 propositions, it is undecidable to determine whether or not a state satisfying ˆCAgwenc(h Smith) 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(h Smith) 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) synchronous6 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 holds7.

6All heads of the tapes progress synchronously, provided the inputs have been aligned with a technical trick. 7We take the convention to use letter B for (multi-tape) finitestate automata.

Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence (IJCAI-18)

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 h R110 = 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 state8 S(100)ω110(100)ω has the form (with the convention that we do not draw self-loops):

. . . 0 1 2 3 4 1 2 3 4 b a b a a b a b

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 e R110 with pre(e R110) = and whose postcondition reflects f110 and leaves unchanged.The postcondition of e R110 is a single-bit version of the postcondition for event e0 for action F of Section 3, as only one proposition is involved. post(e R110)(p) is: f110( ˆKb( p), p, ˆKa( p)) f110( ˆKa( p), p, ˆKb( p)) . 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 h R110?) can be rephrased as the epistemic planning problem over input (Sαωβγω, {FR110}, ˆCAg(wenc(h R110))).

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(h R110) 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(h R110) and if we use at most 2 different propositions.

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

Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence (IJCAI-18)

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 (h Smith or h R110) 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(h Smith)) 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(h Smith) 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 state9, then, for all n N, (S, k) |= wenc(h Smith) iff (S Rn Smith, k + n) |= wenc(h Smith) iff (S Ln Smith, k n) |= wenc(h Smith).

9Recall 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(h Smith) where π is a plan in EPCSmith, then, by Lemma 1, if k 0, π Lk Smith 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(h Smith) 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(h R110). Recall that the input (α, β, γ) defines initial state Sαωβγω. Problem EPKR110 will have wenc(h R110) 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(h R110) 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.

Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence (IJCAI-18)

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.

References [Aucher and Bolander, 2013] Guillaume Aucher and Thomas Bolander. Undecidability in epistemic planning. In Proceedings of the 23rd International Joint Conference on Artificial Intelligence, IJCAI 2013, Beijing, China, August 3-9, 2013, pages 27 33, 2013. [Baltag et al., 1998] Alexandru Baltag, Lawrence S. Moss, and Slawomir Solecki. The logic of public announcements and common knowledge and private suspicions. In Proceedings of the 7th Conference on Theoretical Aspects of Rationality and Knowledge (TARK-98), Evanston, IL, USA, July 22-24, 1998, pages 43 56, 1998. [Baral et al., 2017] Chitta Baral, Thomas Bolander, Hans van Ditmarsch, and Sheila Mc Ilraith. Epistemic Planning (Dagstuhl Seminar 17231). Dagstuhl Reports, 7(6):1 47, 2017. [Belardinelli et al., 2017] Francesco Belardinelli, Alessio Lomuscio, Aniello Murano, and Sasha Rubin. Verification of multi-agent systems with imperfect information and public actions. In Kate Larson, Michael Winikoff, Sanmay Das, and Edmund H. Durfee, editors, Proceedings of the 16th Conference on Autonomous Agents and Multi Agent Systems, AAMAS 2017, São Paulo, Brazil, May 8-12, 2017, pages 1268 1276. ACM, 2017. [Blumensath and Grädel, 2000] Achim Blumensath and Erich Grädel. Automatic structures. In Logic in Computer Science, 2000. Proceedings. 15th Annual IEEE Symposium on, pages 51 62. IEEE, 2000. [Bolander and Andersen, 2011] Thomas Bolander and Mikkel Birkegaard Andersen. Epistemic planning for single and multi-agent systems. Journal of Applied Non-Classical Logics, 21(1):9 34, 2011. [Bolander, 2017] Thomas Bolander. A gentle introduction to epistemic planning: The DEL approach. In Proceedings of the Ninth Workshop on Methods for Modalities, M4M@ICLA 2017, Indian Institute of Technology, Kanpur, India, 8th to 10th January 2017., pages 1 22, 2017. [Charrier et al., 2016] Tristan Charrier, Bastien Maubert, and François Schwarzentruber. On the impact of modal depth in epistemic planning. In Proceedings of the Twenty Fifth International Joint Conference on Artificial Intelligence, IJCAI 2016, New York, NY, USA, 9-15 July 2016, pages 1030 1036, 2016.

[Chellas, 1980] Brian F Chellas. Modal logic: an introduction. Cambridge university press, 1980. [Codd, 1968] Edgar F Codd. Cellular automata. Academic Press, 1968. [Cook, 2004] Matthew Cook. Universality in elementary cellular automata. Complex Systems, 15(1), 2004. [Cook, 2008] Matthew Cook. A concrete view of rule 110 computation. In Proceedings International Workshop on The Complexity of Simple Programs, CSP 2008, Cork, Ireland, 6-7th December 2008., pages 31 55, 2008. [Kominis and Geffner, 2015] Filippos Kominis and Hector Geffner. Beliefs in multiagent planning: From one agent to many. In Proceedings of the Twenty-Fifth International Conference on Automated Planning and Scheduling, ICAPS 2015, Jerusalem, Israel, June 7-11, 2015., pages 147 155, 2015. [Larsson, 2013] Urban Larsson. Impartial games emulating one-dimensional cellular automata and undecidability. J. Comb. Theory, Ser. A, 120(5):1116 1130, 2013. [Lindgren and Nordahl, 1990] Kristian Lindgren and Mats G. Nordahl. Universal computation in simple one-dimensional cellular automata. Complex Systems, 4(3), 1990. [Minsky, 1967] Marvin L Minsky. Computation: finite and infinite machines. Prentice-Hall, Inc., 1967. [Schwarzentruber, 2018] François Schwarzentruber. Hintikka s world: agents with higher-order knowledge (demo). In Proceedings of the 27th International Joint Conference on Artificial Intelligence (IJCAI) and the 23rd European Conference on Artificial Intelligence (ECAI), Stockholm, 13-19 July 2018, 2018. [Smith, 1968] Alvy Ray Smith. Simple computationuniversal cellular spaces and self-reproduction. In 9th Annual Symposium on Switching and Automata Theory, Schenectady, New York, USA, October 15-18, 1968, pages 269 277, 1968. [Sutner, 2003] Klaus Sutner. Almost periodic configurations on linear cellular automata. Fundam. Inform., 58(2003):223 240, 2003. [van Ditmarsch and Kooi, 2015] Hans van Ditmarsch and Barteld Kooi. One Hundred Prisoners and a Light Bulb. Springer, 2015. [van Ditmarsch et al., 2007] Hans van Ditmarsch, Wiebe van Der Hoek, and Barteld Kooi. Dynamic epistemic logic, volume 337. Springer Science & Business Media, 2007. [von Neumann, 1951] John von Neumann. The general and logical theory of automata. Cerebral mechanisms in behavior, 1(41):1 2, 1951. [Wolfram, 2002] Stephen Wolfram. A new kind of science. Wolfram-Media, 2002.

Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence (IJCAI-18)