Tristan Charrier

Bastien Maubert

François Schwarzentruber

On the Impact of Modal Depth in Epistemic Planning (Extended Version)

Epistemic planning is a variant of automated planning in the framework of dynamic epistemic logic. In recent works, the epistemic planning problem has been proved to be undecidable when preconditions of events can be epistemic formulas of arbitrary complexity, and in particular arbitrary modal depth. It is known however that when preconditions are propositional (and there are no postconditions), the problem is between Pspace and Expspace. In this work we bring two new pieces to the picture. First, we prove that the epistemic planning problem with propositional preconditions and without postconditions is in Pspace, and is thus Pspace-complete. Second, we prove that very simple epistemic preconditions are enough to make the epistemic planning problem undecidable: preconditions of modal depth at most two suffice.

Introduction

A key objective in artificial intelligence is to develop autonomous agents able to plan their actions towards achieving their goals, and to reason about their own and other agents' knowledge. Planning, which consists in finding a sequence of actions to reach a given objective from an initial situation, is a central research domain in artificial intelligence. Concerning reasoning about knowledge, dynamic epistemic logic (DEL) is now recognised as a very promising framework [START_REF] Van Ditmarsch | Dynamic epistemic logic[END_REF]. Recently, planning and dynamic epistemic logic have been combined in the so-called epistemic planning problem [START_REF] Bolander | Epistemic planning for single and multiagent systems[END_REF].

In DEL, events can deal with high-order reasoning. For instance we may model the following event:

"Anne receives a letter revealing that ϕ is true and Bob knows that Anne receives the truth value of ϕ but Anne is unsure whether Bob knows that or not."

In DEL, ϕ is called a precondition: ϕ needs to be true for this event to occur, and therefore its occurence brings the information that ϕ is true. This event is purely informative, but DEL also allows physical (ontic) effects on the world; these are referred to as postconditions.

One natural question is: how does the nesting of knowledge in pre-and postconditions impact the complexity of the epistemic planning problem? On the one hand, when only propositional preconditions are used, such as ϕ = "Bob is married", the problem is decidable if postconditions are also propositional [START_REF] Yu | Multi-agent epistemic explanatory diagnosis via reasoning about actions[END_REF]. In this case it is in k-Exptime, where k is the maximal modal depth of goal formulas [START_REF] Aucher | Automata techniques for epistemic protocol synthesis[END_REF] postconditions (events are purely epistemic), the problem is in Expspace [START_REF] Bolander | Complexity results in epistemic planning[END_REF]. On the other hand, epistemic preconditions such as ϕ = "Bob considers it possible that Anne knows that Bob does not know that it is raining" yield undecidability: if propositional postconditions are allowed, then the problem is already undecidable with preconditions of modal depth one [START_REF] Bolander | Epistemic planning for single and multiagent systems[END_REF].

It is also known to be undecidable without postconditions, if we allow for preconditions of unbounded modal depth [START_REF] Aucher | Undecidability in epistemic planning[END_REF]. See Table 1 for a summary of results about epistemic planning.

In this paper, our contribution is twofold:

1. With propositional preconditions and no postconditions, epistemic planning is in Pspace (Theorem 1). The key point is that in this case events commute [START_REF] Löwe | DEL planning and some tractable cases[END_REF]. This allows for a succinct representation of tuples of events, and we build upon a model checking procedure from [START_REF] Aucher | On the complexity of dynamic epistemic logic[END_REF] to devise a polynomial space decision procedure.

2. Epistemic planning without postconditions is already undecidable with preconditions of modal depth two (Theorem 2). The proof, by reduction from the halting problem for two counter machines, refines the one given in [START_REF] Aucher | Undecidability in epistemic planning[END_REF], which requires preconditions with unbounded modal depth. By designing more involved gadgets to code the configurations and instructions of the machines, we manage to bound the modal depth of preconditions.

We first recall the background on epistemic planning in Section 2. We establish our two contributions, described above, in Section 3 and Section 4 respectively. We briefly discuss future work in Section 5.

Background on epistemic planning

In this section, we recall the necessary background about dynamic epistemic logic and epistemic planning.

Dynamic epistemic logic

Let AP be a countably infinite set of atomic propositions, and let Ag = {1, . . . , n} be a finite set of agents. The epistemic language L EL is the language of propositional logic extended with one knowledge modality for each agent. Intuitively, Kaϕ reads as "agent a knows that ϕ holds". The syntax of L EL is given by the following grammar:

ϕ ::= p | ¬ϕ | (ϕ ∨ ϕ) | Kaϕ where p ∈ AP and a ∈ Ag.
The semantics of L EL is given in terms of epistemic models that represent how the agents perceive the world.

Definition 1 An epistemic model is a tuple M = (W, {Ra}a∈Ag, V ) where:

• W is a non-empty finite set of possible worlds,

• Ra ⊆ W × W is an accessibility relation for agent a, • V : AP → 2 W is a valuation function.
We write w ∈ M for w ∈ W , |M| for |W |, and (M, w) is called a pointed epistemic model. The intended meaning of wRaw is that in world w agent a considers that w might be the actual world.

The semantics of L EL is defined as follows:

• M, w |= p if w ∈ V (p); • M, w |= ¬ϕ if it is not the case that M, w |= ϕ; • M, w |= (ϕ ∨ ψ) if M, w |= ϕ or M, w |= ψ; • M, w |= Kaϕ if for all w s.t. wRaw , M, w |= ϕ.
Dynamic epistemic logic (DEL) extends epistemic logic with modalities that represent the occurrence of events. In DEL, events are represented by event models that we define below. In general DEL events can bring information and modify the world, and such events are called ontic events [START_REF] Van Ditmarsch | Semantic results for ontic and epistemic change[END_REF]; in this work however we focus on purely informative events, called epistemic events [START_REF] Baltag | The logic of public announcements, common knowledge, and private suspicions[END_REF].

Definition 2 An event model is a tuple E = (E, {→a}a∈Ag, pre) where:

• E is a non-empty finite set of possible events,

• →a⊆ E × E is an accessibility relation on E for agent a, • pre : E → L EL is a precondition function.

We write e ∈ E for e ∈ E, |E| for |E|, and (E, e) is called a pointed event model, where e represents the actual event of (E, e). An event e can occur in a world w of an epistemic model M if, and only if, its precondition is verified, i.e. M, w |= pre(e), which leads to the following definition: Definition 3 Given M = (W, {Ra}a∈Ag, V ) an epistemic model and E = (E, {→a}a∈Ag, pre) an event model, the update product of M and E is the epistemic model M⊗E = (W ⊗ , {R ⊗ a }a∈Ag, V ⊗ ) where: We now define the syntax and semantics of DEL. The syntax is given by the following grammar: E,e) where the precondition of the actual event e is p, and the one of event f is . (E, e) represents the event where agent 1 learns that p is true while agent 2 believes that nothing happens. Figure 1(c) shows the product (M, w)⊗(E, e), which represents the situation after event (E, e). Observe that agent 1 knows p and agent 2 does not.

W ⊗ = {(w, e) ∈ W × E | M, w |= pre(e)},
ϕ ::= p | ¬ϕ | (ϕ ∨ ϕ) | Kiϕ | E,
Remark 1 We do not make any assumption on the nature of the accessibility relations in epistemic and event models. In particular we do not assume S5.

w : p u : 1, 2 1, 2 1, 2 e : p f : 2 1 1, 2 (w, e) : p (w, f ) : p (u, f ) : 2 2 1, 2 1 1, 2 1, 2 (a) (b) (c)
Figure 1: Example of a product.

Epistemic planning

Let C be a class of pointed event models. The epistemic planning problem restricted to C is the following:

Definition 4 (Epistemic planning problem)

• Input: a pointed epistemic model (M, w), a finite set of pointed event models E ⊆ C, and an epistemic goal formula ϕg;

• Output: yes if there exists a sequence of pointed event models (E1, e1), . . . , (Ep, ep) ∈ E (a plan) such that M, w |= E1, e1 . . . Ep, ep ϕg; no otherwise.

We now establish the precise complexity of this problem for propositional event models.

Propositional preconditions

Let C0 be the class of (pointed) epistemic event models where preconditions are propositional formulas. For instance, the pointed event model depicted in Figure 1(c) is in C0 since both p and are propositional formulas. The epistemic planning restricted to C0 is known to be Pspace-hard [START_REF] Bolander | Complexity results in epistemic planning[END_REF]. We establish that it is actually Pspace-complete.

As pointed out in [START_REF] Löwe | DEL planning and some tractable cases[END_REF], epistemic event models with propositional preconditions commute. Formally:

Lemma 1 For all pointed epistemic models (M, w), for all pointed event models (E1, e1) and (E2, e2) in C0, M ⊗ E1 ⊗ E2, (w, e1, e2) exists iff M ⊗ E2 ⊗ E1, (w, e2, e1) exists, and in that case they are bisimilar.

As a consequence, in the rest of the section, the order in which events are applied in an initial world is indifferent. Only the number of times each event occurs is relevant, and the proof of our result heavily relies on this property.

We first establish a preliminary result on the model checking problem for a dedicated language: we extend the dynamic epistemic language with iterations of event models in C0, that is, constructions of the form (E, e) ψ where (E, e) is a pointed event model in C0 and is a positive integer. We suppose here that is written in binary so that this language, called L it C 0 , is exponentially more succinct than DEL. The size |ϕ| of a formula ϕ is defined as usual, with the following additional inductive case: | (E, e) ψ| = 1 + |E| + log 2 + |ψ| (by convention log 2 0 = 0). Classically, the model checking problem for L it C 0 is, given a pointed epistemic model (M, w) and a formula Φ ∈ L it C 0 , to decide whether M, w |= Φ.

Proposition 1 Model checking L it C 0 is in Pspace. function mc(M, w, E, n, ϕ) match ϕ case p: return (p is true in w) case ¬ψ: return not mc(M, w, E, n, ψ) case (ψ 1 ∨ ψ 2 ) : return mc(M, w, E, n, ψ 1 ) or mc(M, w, E, n, ψ 2 ) case K a ψ : for u ∈ R a (w), ∈ N |E| s.t. |E| i=1 i = |E| i=1 n i if    preok(M, u, E, )
and succ(E, a, n, ) and not mc(M, u, E, , ψ) Proof We design a deterministic algorithm that takes as an input a pointed epistemic model (M, w0) and a formula Φ ∈ L it C 0 , and decides whether M, w0 |= Φ. Without loss of generality, we suppose that all event models appearing in the formula are the same, noted E = (E, →, pre) (if not, we replace each one by their disjoint union). Let e1, . . . , e |E| be an enumeration of the possible events in E. By Lemma 1, all permutations of events in a tuple (w, ei 1 , . . . , ei p ) are equivalent in the sense that either they all are worlds in M ⊗ E p and they all are bisimilar, or none of them exists: only the number of times each event occurs is relevant. For a world w and a vector n = (n1, . . . , n |E| ), we thus let w• n denote the representative permutation (w, e1, . . . , e1 ).

   then return false return true case (E, e i ) ψ : if pre(e i ) is false in w then return false return mc(M, w, E, (n 1 , .., n i-1 , n i + , n i+1 , .., n k ), ψ)
Let mc be the algorithm given in Figure 2, and let 0 |E| denote the null |E|-vector. We claim that mc(M, w0, E, 0 |E| , Φ) returns true iff M, w0 |= Φ. To prove this claim we establish that for all w ∈ M, all integers n1, . . . , n |E| and all subformula ϕ of Φ, the following property P holds:

If M ⊗ E |E| i=1 n i , w• n exists then mc(M, w, E, (n1, . . . , n |E| ), ϕ) returns true iff M ⊗ E |E| i=1 n i , w• n |= ϕ.
Property P is proven by induction on ϕ. We omit the boolean cases and case (E, ei) ψ which are trivial.

Case Kaψ: the algorithm has to check that ψ holds in all a-successors of w

• n in M ⊗ E |E| i=1 n i .
Every a-successor of w• n is a permutation of some u• and is bisimilar to it. We thus need to enumerate all worlds u and vectors that represent some a-successor, and verify that ψ holds in u• . Given a tuple u• , to check whether it is a permutation of some a-successor of w• n, we first check that it is an existing world in M ⊗ E |E| i=1 n i . Since events are purely epistemic and propositional, preconditions of successive events can all be checked in the initial world u. This is done by calling function preok(M, u, E, ), which checks that for all i ∈ {1, . . . , |E|}, if i > 0 then pre(ei) is true in u. Next, we check that some permutation of u• is indeed a-related to w• n: we should first have u ∈ Ra(w); then, it should be possible to map each occurrence of an event ei in w• n to some occurrence of some a-related event ej in u• so as to form a bijection. Deciding whether such a bijection exists amounts to solving the following integer linear program: checking whether there exist positive integers (xi,j) (i,j)∈{1,...,|E|} 2 |e j ∈Ra(e i ) , where xi,j is the number of times ej is chosen as a-successor for ei, such that:

(S)
ni = j|e j ∈Ra(e i ) xi,j for all i ∈ {1, . . . , |E|}, and j = i|e i ∈Ra(e j ) xi,j for all j ∈ {1, . . . , |E|}.

This is done by calling succ(E, a, n, ).

Spatial complexity. We justify that mc can be implemented in polynomial space in the size of the input (which is |M|+|Φ|).

m i=1 i) ≤ m i=1 log 2 i + log 2 m,
and because the ceiling of a sum is less than the sum of the ceilings, we get

k log 2 ( m i=1 i) ≤ |E|( m i=1 log 2 i + log 2 m ).
By definition of the size of L it C 0 formulas, k = |E| ≤ |Φ|, m i=1 log 2 i ≤ |Φ| and log 2 m ≤ m ≤ |Φ|, so that the space used to store n is in O(|Φ| 2 ). It only remains to note that checking consistency of a system (S) can be done in non-deterministic time polynomial in the number of bits needed to encode n and [START_REF] Papadimitriou | On the complexity of integer programming[END_REF], and therefore in deterministic space polynomial in |Φ|.

We now describe a (non-deterministic) algorithm for the epistemic planning problem, which consists in guessing a plan and then model-check an L it C 0 -formula to check that this plan realizes the goal. The crucial points here are, first, that we can restrict to plans of exponential length, second, that thanks to commutation of events they can be represented in polynomial space, and third, that verifying whether a plan works can be done in polynomial space (Proposition 1).

Theorem 1

The epistemic planning problem restricted to C0 is in Pspace.

Proof We adapt the algorithm given in [START_REF] Bolander | Complexity results in epistemic planning[END_REF]Theorem 5.8]. First it is proved in [START_REF] Sadzik | Exploring the Iterated Update Universe[END_REF] that, noting d the d-bisimulation 1 for event models (see [START_REF] Van Ditmarsch | Dynamic epistemic logic[END_REF], [START_REF] Bolander | Complexity results in epistemic planning[END_REF], [START_REF] Sadzik | Exploring the Iterated Update Universe[END_REF]), for every d ≥ 0, every pointed event model (E, e) is d -stabilizing at iteration |E| d ; formally, (E, ei) k d (E, ei) k+1 for all k ≥ |E| d . 2 Secondly, by Lemma 1, event models with propositional preconditions commute. Therefore, the following algorithm correctly solves the epistemic planning problem for event models with propositional preconditions:

Given input (M, w), {(E1, e1), . . . , (Em, em)}, ϕg :

1 Bisimulation up to modal depth d. 2 Actually a better bound is proved in [START_REF] Bolander | Complexity results in epistemic planning[END_REF]. This algorithm is non-deterministic. The first step is clearly performed in space polynomial in the size of the input. Concerning the second point, each ni can be exponential in d and thus in |ϕg|, but its binary representation uses polynomial space. Since (E1, e1) n 1 . . . (Em, em) nm ϕg is an L it C 0 formula, it follows from Proposition 1 that the last step can also be performed in polynomial space. The epistemic planning problem restricted to C0 is therefore in NPspace and thus in Pspace by Savitch's theorem [START_REF] Savitch | Relationships between nondeterministic and deterministic tape complexities[END_REF].

We now turn to the case of modal preconditions with bounded modal depth. A two-counter machine M halts if there exist c1, c2 such that (0, 0, 0) → * M (N, c1, c2), where → * M denotes the reflexive transitive closure of →M . For instance, the machine Mex given in Example 2 above does not halt. The halting problem for two-counter machines consists in deciding, given a two-counter machine, whether it halts or not. This problem is well known to be undecidable [START_REF] Minsky | Computation: finite and infinite machines[END_REF].

PC = 1 c 1 = 3 c 2 = 2 a 0 a 1 a N a 1 . . . a 2 p 1 q 1 p 1 p 1 p 1 p 2 q 2 p 2 p 2 Figure 3: Pointed epistemic model (M, w) (1,3,2) . PC = 0 c 1 = 0 c 2 = 0 a 0 a 1 a N a 0 . . . p 1 q 1 p 2 q 2

The reduction

We define an effective reduction tr that, given a two-counter machine M , computes an instance tr(M ) of the epistemic planning problem restricted to C2. We fix M and the rest of the section is devoted to defining tr(M ) = (M0, w0); E; ϕg and justifying its correctness (Proposition 2). As in [START_REF] Aucher | Undecidability in epistemic planning[END_REF], we only use one agent a ( stands for Ka and ♦ stands for ¬Ka¬), configurations of M are represented by pointed epistemic models, and the initial pointed epistemic model represents the initial configuration (0, 0, 0). Each program line :I is represented by one or two pointed event model(s), such that a plan corresponds to a sequence of program lines. The goal formula expresses that the final pointed epistemic model represents a halting configuration.

Pointed epistemic models

Let ( , c1, c2) be a configuration of M . We describe the pointed epistemic model

(M ( ,c 1 ,c 2 ) , w ( ,c 1 ,c 2 ) ) (shortened as (M, w) ( ,c 1 ,c 2 )
) that represents ( , c1, c2). For instance, Figure 3 shows (M, w) [START_REF] Van Ditmarsch | Dynamic epistemic logic[END_REF][START_REF] Yu | Multi-agent epistemic explanatory diagnosis via reasoning about actions[END_REF][START_REF] Bolander | Epistemic planning for single and multiagent systems[END_REF] . It is a tree-like structure rooted at w ( ,c 1 ,c 2 ) . In each world except the root, there is exactly one true atomic proposition, and we call p-world any world where p holds. The root w ( ,c 1 ,c 2 ) verifies no atomic proposition, and it has three groups of children, one for each counter:

Program counter. For each program line : I , w ( ,c 1 ,c 2 ) has one reflexive child labeled by proposition a . The a -child of w ( ,c 1 ,c 2 ) has a child also labeled by a , without

a 0 a N a 0 . . . a 2 p 1 q 1 p 1 p 1 p 1 p 2 q 2 p 2 p 2 a 0 a 1 a N a 1 . . . p 2 q 2 p 2 p 2 p 2 (a) (b)
Figure 5: Examples of non valid epistemic models.

any outgoing edge: we say that there is an a -strip. Intuitively, the a -strip represents the fact that I is the next instruction to be executed. Data counter ci. For each i ∈ {1, 2}, w ( ,c 1 ,c 2 ) has a reflexive pi-child that has an irreflexive qi-child, and is followed by a chain of irreflexive pi-worlds of length ci. Intuitively, the number of irreflexive pi-children represents the value of ci.

We define the first component of tr(M ): (M0, w0) := (M, w) (0,0,0) as depicted in Figure 4. We call configuration model a pointed epistemic model of the form (M, w) ( ,c 1 ,c 2 ) .

Pointed event models

For each program line :I of M where I is of the form goto( ) or inc(i), we define a pointed event model (E :I , e :I ) (shortened as (E, e) :I ) that mimics the semantics of :I (Figures 7 and9). For each program line :gotocond(i, ) of M , we define two pointed event models (E, e) :gotocond(i, ) and (E >0 , e >0 ) :gotocond(i, ) , respectively for the case ci = 0 and ci > 0 (Figure 10). These pointed event models form the second component of tr(M ):

E := {(E, e) :I | < N } ∪ {(E >0 , e >0 ) :I | < N and I = gotocond(i, )}.
In the model (M, w) ( ,c 1 ,c 2 ) where < N , the only pointed event model of E that should be applied is the one representing the behavior of program line :I in configuration ( , c1, c2). This event model is defined as follows:

E( , c1, c2) :=    (E >0 , e >0 ) :I if I = gotocond(i, )
and ci > 0, (E, e) :I otherwise.

The product with any other event model from E results in a model that is not valid according to the following definition: Definition 6 A pointed epistemic model (M, w) is valid if w has an a -child for each ∈ {0, . . . , N } and a pi-child for each i ∈ {1, 2}.

Example 3

The model shown in Figure 3, corresponding to (M, w) (1,3,2) , is valid. Note that by definition, every configuration model is valid. The two models shown in Figure 5 are not valid. Indeed:

• In the model shown in Figure 5(a), the root does not have a a1-child.

• In the model shown in Figure 5(b), the root does not have a p1-child.

Further down, we will define event models of E such that:

Lemma 2 For every configuration ( , c1, c2), it holds that

1. (M, w) ( ,c 1 ,c 2 ) ⊗ E( , c1, c2) is isomorphic 3 to (M, w) ( ,c 1 ,c 2 )
, where ( , c1, c2) →M

3 More precisely, the reachable parts of the pointed epistemic models are isomorphic. (E, e) :goto( ) ( , c 1 , c 2 ).

repl( , ) p 1 q 1 p 2 q 2
2. The product of (M, w) ( ,c 1 ,c 2 ) with any other event model from E is defined but not valid.

3. For any non-empty sequence of event models (E1, . . . , En, En+1) in E, if the model

(M, w) ( ,c 1 ,c 2 ) ⊗ E1 ⊗ • • • ⊗ En is not valid, then (M, w) ( ,c 1 ,c 2 ) ⊗ E1 ⊗ • • • ⊗ En ⊗ En+1
is also not valid.

We now describe the event models in E and at the same time we prove Lemma 2. Each of these models has three groups (from left to right on Figures 7,[START_REF] Van Ditmarsch | Semantic results for ontic and epistemic change[END_REF][START_REF] Baltag | The logic of public announcements, common knowledge, and private suspicions[END_REF], that update respectively the program counter group, the data counter c1 group and the data counter c2 group of configuration models.

Event model for : goto( ). The pointed event model (E, e) :goto( ) , that mimics the effect of :goto( ), is depicted in Figure 7. Portion repl( , ) concerns the program counter group and is described in Figure 6. The two other groups leave the data counter groups c1 and c2 unchanged.

• The product (M, w) ( ,c 1 ,c 2 ) ⊗ (E, e) :goto( ) is isomorphic to (M, w) ( ,c 1 ,c 2 ) : indeed, portion repl( , ) removes the a -strip and adds an a -strip in the program counter group (recall that = ).

• The product (M, w) ( ,c 1 ,c 2 ) ⊗(E, e) :goto( ) with = is not valid. Indeed, as (M, w) ( ,c 1 ,c 2 ) does not have an a -strip in its program counter group, its a -world violates precondition a ∧ ♦ ⊥ in portion repl( , ). As a consequence, (M, w) ( ,c 1 ,c 2 ) ⊗ (E, e) :goto( ) has no a -child at its root and is thus not valid.

Event model for : inc(i). Figure 9 shows (E, e) :inc(1) that mimics the effect of : inc(1) (for inc(2), the construction is symmetric). Portion repl( , + 1) is meant to increment the program counter. Portion lengthen(1) (described in Figure 8) is meant to increment the data counter c1. The intermediate event of precondition p1 ∧ ♦q1 duplicates once the p1-child of the root: it adds one p1-world at the start of the p1-chain. The last group leaves data counter c2 unchanged. • For the same reason as for (E, e) :goto( ) , the product (M, w) ( ,c 1 ,c 2 ) ⊗ (E, e) :inc(1) with = is not valid.

• The product (M, w) ( ,c 1 ,c 2 ) ⊗ (E, e) :inc(1) is isomorphic to (M, w) ( +1,c 1 +1,c 2 ) . p i ∧ ♦q i q i p i ∧ ♦q i p i ∧ ¬♦q i p i ∧ ♦q i ∧ ♦(p i ∧ ¬q i ) q i p i ∧ ¬♦q i ∧ ♦
Event models for : gotocond(i, ). and (E >0 , e >0 ) :gotocond (1, ) . They mimic the effect of : gotocond(1, ) in case c1 = 0 and case c1 > 0, respectively (for : gotocond(2, ), constructions are symmetric).

• (M, w) ( ,0,c 2 ) ⊗ (E, e) :gotocond(1, ) is isomorphic to (M, w) ( ,0,c 2 ) : indeed, the precondition ¬♦(p1 ∧ ¬♦q1) checks that the p1-chain in the data counter c1 group is of length 0.

Here it is the case, so that the data counter group c1 remains unchanged. However, when c1 > 0, the p1-child of the root of (M, w) ( ,c 1 ,c 2 ) violates this precondition. It is thus removed, so that the product (M, w) ( ,c 1 ,c 2 ) ⊗ (E, e) :gotocond(1, ) is not valid.

• (M, w) ( ,c 1 ,c 2 ) ⊗ (E >0 , e >0 ) :gotocond(1, ) with c1 > 0 is isomorphic to (M, w) ( +1,c 1 -1,c 2 ) . Indeed, portion shorten(1) (Figure 8) is meant to decrement data counter c1 by one: precondition p1 ∧ ¬♦q1 ∧ ♦ checks that we are in the p1-chain (p1), but not at the start (¬♦q1) nor the end (♦ ) of the chain. The last world of the p1-chain is thus removed when c1 > 0. When c1 = 0, precondition ♦(pi ∧ ¬qi) is violated by the p1-child of the root of (M, w) ( ,0,c 2 ) : indeed, this precondition checks that the length of the p1-chain is at least 1. The product (M, w) ( ,0,c 2 ) ⊗ (E >0 , e >0 ) :gotocond(1, ) is thus not valid.

• For = , (M, w) ( ,c 1 ,c 2 ) ⊗(E, e) :gotocond(1, ) and (M, w) ( ,c 1 ,c 2 ) ⊗(E >0 , e >0 ) :gotocond(1, ) are not valid.

The explanations above can be shown by applying Definition 3. They prove points 1 and 2 of Lemma 2. We now prove point 3 of Lemma 2:

We first prove the following assertion An for all n ≥ 1: for all ( , c1, c2), for all E1 ⊗ • • • ⊗ En, if (M, w) ( ,c 1 ,c 2 ) ⊗ E1 ⊗ • • • ⊗ En is not valid then there exists p ∈ {a0, . . . , aN , p1, p2} such that there is no p-world in (M, w) ( ,c 1 ,c 2 ) ⊗ E1 ⊗ • • • ⊗ En. It is proven by recurrence on n ≥ 1.

• A1: if (M, w) ( ,c 1 ,c 2 ) ⊗ E1 is not valid, then:

-Either E1 contains a repl( , ) part such that = , then there is no a -world in (M, w) ( ,c 1 ,c 2 ) ⊗ E1, so we take p = a ; -Or I = gotocond(i, ) (with i ∈ {1, 2}) and E1 is (E, e) :gotocond(i, ) with ci > 0. In this case, there is no pi-world in (M, w) ( ,c 1 ,c 2 ) ⊗ E1, so we take p = pi.

of Lemma 2, follows the transition function of M . As the final product satisfies ϕ halt , it is isomorphic to (M, w) (N,c 1 ,c 2 ) for some c1, c2, so that the final configuration is (N, c1, c2). Therefore, M halts.

Comparison

In [START_REF] Aucher | Undecidability in epistemic planning[END_REF] the program counter as well as the data counters are represented with chains of worlds, and incrementation, decrementation and replacement of a value by another one are implemented on such chains. While the first two operations can be performed with preconditions of modal depth two, repl( , ) requires unbounded nesting in general to be implemented on chains. We observed that unlike data counters, the program counter is bounded so that we can avoid chains for its representation, and provide an alternative gadget for repl( , ) that only uses preconditions of modal depth two.

Future work

The natural continuation is to complete Table 1. First, is the epistemic planning problem decidable for preconditions of modal depth one and no postconditions, or do modalities in preconditions immediately bring about undecidability? Second, what is the exact complexity of the problem with propositional pre-and postconditions? It is known to be decidable [START_REF] Yu | Multi-agent epistemic explanatory diagnosis via reasoning about actions[END_REF], with a non-elementary upper bound [START_REF] Aucher | Automata techniques for epistemic protocol synthesis[END_REF] and a Pspace lower bound [START_REF] Bolander | Complexity results in epistemic planning[END_REF]; this a big gap that should be bridged. We would also like to see how different axioms of knowledge affect the picture. Indeed, our proof of undecidability does not work if accessibility relations must be equivalences, but it can surely be adapted to obtain a similar result for preconditions of modal depth three or four. Can we do better? Does the choice of axioms change the border between decidability and undecidability?

  R ⊗ a (w, e) = {(w , e ) ∈ W ⊗ | wRaw and e →a e }, V ⊗ (p) = {(w, e) ∈ W ⊗ | M, w |= p} The product of a pointed epistemic model (M, w) with a pointed event model (E, e) is defined as (M, w) ⊗ (E, e) := (M ⊗ E, (w, e)) if M, w |= pre(e), otherwise it is undefined.

Figure 2 :

 2 Figure 2: Algorithm mc for model checking L it C0 .

Figure 4 :

 4 Figure 4: Pointed epistemic model representing the initial configuration (0, 0, 0).

Figure 6 :

 6 Figure 6: Event model portion repl( , ) for = .

Figure 7 :

 7 Figure 7: Event model for :goto( ).

Figure 8 : 2 Figure 9 :

 829 Figure 8: Event model portions lengthen(i) and shorten(i).

Figure 10

 10 describes models (E, e) :gotocond(1, )

Table 1 :

 1 Overview (d: modal depth; gray: this paper).

	; if there are no

  The maximal number of nested calls is bounded by |Φ|, so that the number of local variables to be stored is polynomial in |Φ|. We now bound the space needed to store vector n in each call, which is in O( |E| i=1 log 2 ni ). Letting 1, . . . , m be an enumeration of the numbers appearing in Φ, it is clear that k i=1 ni ≤ m i=1 i, and thus for all i ∈ {1, . . . , |E|}, ni ≤ m j=1 j . We obtain

|E| i=1 log 2 ni ≤ |E| log 2 ( m i=1 i) . Now, it can be proven by studying the variation of function f : (x1, . . . , xm) → log 2 ( m i=1 xi)m i=1 log 2 xi -log 2 m, that since i ≥ 1 for all i ∈ {1, . . . , m}, we have log 2 (

  1. Compute d, the modal depth of the goal formula ϕg; 2. For each i ∈ {1, . . . , m}, non-deterministically guess ni ∈ 0, . . . , |Ei| d ; 3. Accept if M, w |= (E1, e1) n 1 . . . (Em, em) nm ϕg.

Acknowledgment.

We warmly thank anonymous reviewers that advised us to add examples in the JELIA version and move a part of the technicalities to this technical report.

Preconditions of bounded modal depth

Let C2 be the class of event models with preconditions of modal depth at most two. We prove the following theorem by refining the reduction given in [START_REF] Aucher | Undecidability in epistemic planning[END_REF].

Theorem 2

The epistemic planning problem restricted to C2 is undecidable.

We first recall the halting problem for two-counter machines, known to be undecidable [START_REF] Minsky | Computation: finite and infinite machines[END_REF], and then we reduce it to the epistemic planning problem restricted to C2.

Two-counter machines

We present two-counter machines as introduced in [START_REF] Minsky | Computation: finite and infinite machines[END_REF].

Definition 5 A two-counter machine M is a sequence of instructions (I0, . . . , IN ) where

We call program line a pair k:I k .

Example 2

The following four programs lines define a two-counter machine Mex: 0:inc(1) 1:gotocond(1, 3) 2:goto(0) 3:halt A configuration of a two-counter machine M is a triple ( , c1, c2) where ∈ {0, . . . , N } is the program counter and c1, c2 ∈ N are the two data counters. Let CM = {0, . . . , N } × N × N be the set of all possible configurations.

The transition function →M on CM is defined as follows. For all ( , c1, c2) ∈ CM :

shorten( 1) -Or I = gotocond(i, ) (with i ∈ {1, 2}) and E1 is (E >0 , e >0 ) :gotocond(i, ) with ci = 0. In this case, there is no pi-world in (M, w) ( ,c 1 ,c 2 ) ⊗ E1, so we take p = pi.

In other cases, (M, w) ( ,c 1 ,c 2 ) ⊗ E1 is valid by point 1 of Lemma 2.

• An ⇒ An+1: We suppose An holds for a given n ≥ 1. For any

En is valid and by points 1 and 2 of Lemma 2, it is isomorphic to some (M, w) ( ,c 1 ,c 2 ) . We apply A1 to conclude.

valid, so by An there exists p such that there is no p-world. By Definition 3, because there is no postcondition, there is no p-world in (M, w)

To conclude, we have proven that if (M, w)

An there is p ∈ {a0, . . . , aN , p1, p2} that is false in every world. Therefore, for any En+1, there is no p-world in (M, w)

This concludes the proof of point 3 of Lemma 2.

Goal formula

The goal formula ϕg in tr(M ) is ϕ valid ∧ ϕ halt , where:

Intuitively, formula ϕ valid forces the final pointed epistemic model of a plan to be valid (and therefore, by Point 3 of Lemma 2, all intermediate pointed epistemic models of the plan also are valid). Formula ϕ halt enforces the final pointed epistemic model to represent a halting configuration (N, * , * ).

Proposition 2 M halts iff there is a plan for tr(M ).

Proof ⇒ If M halts, let ( t , c t 1 , c t 2 )t=0,...,T be the sequence of configurations of the halting execution. We build a plan for tr(M ) by taking the sequence of pointed event models (E( t , c t 1 , c t 2 ))t=0,...,T -1. One can prove by recurrence, using point 1 of Lemma 2, that each intermediate product (M, w) (0,0,0) ⊗ E(0, 0, 0)

⇐ Suppose that there is a plan (Et, et)t=0,...,T -1 for tr(M ). As the final product satisfies ϕ valid , it is valid. Using point 3 of Lemma 2 we can prove by backward recurrence that all intermediate products are valid. By forward recurrence, using points 1 and 2 of Lemma 2, we can prove that each intermediate model is isomorphic to a model of the form (M, w) ( ,c 1 ,c 2 ) , and that the event model applied to it in the plan is E( , c1, c2). We extract a sequence of configurations ( , c1, c2)t=0,...,T that starts with (0, 0, 0) and that, by point 1