On the Impact of Modal Depth in Epistemic Planning

1 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 [van Ditmarsch et al., 2007]. Recently, planning and dynamic epistemic logic have been combined in the so-called epistemic planning problem [Bolander and Andersen, 2011].

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?

Franc¸ois Schwarzentruber ENS Rennes / IRISA francois.schwarzentruber

@ens-rennes.fr

)

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

On the one hand, when only propositional preconditions are used, such as ' = "Bob is married", the problem is decidable if postconditions are also propositional [Yu et al., 2013]. In this case it is in k-EXPTIME, where k is the maximal modal depth of goal formulas [Aucher et al., 2014]; if there are no postconditions (events are purely epistemic), the problem is in EXPSPACE [Bolander et al., 2015].

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 [Bolander and Andersen, 2011]. It is also known to be undecidable without postconditions, if we allow for preconditions of unbounded modal depth [Aucher and Bolander, 2013]. 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 [L¨owe et al., 2011]. This allows for a succinct representation of tuples of events, and we build upon a model checking procedure from [Aucher and Schwarzentruber, 2013] 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 [Aucher and Bolander, 2013], 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.

2 Background on epistemic planning

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

2.1 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 LEL 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 LEL is given by the following grammar:

The semantics of LEL is given in terms of epistemic models that represent how the agents perceive the world.

Definition 1 An epistemic model M = (W↪ ¶Ra♦a2Ag↪ V ) is a tuple where:

• ÷ W is a non-empty finite set of possible worlds,
• ÷ V : AP ! 2W is a valuation function.
• ÷ Ra ✓ W ⇥W is an accessibility relation for agent a,

We write w 2 M for w 2 W, ♣M♣ for ♣W♣, and (M↪w) is called a pointed epistemic model. The intended meaning of wRaw0 is that in world w agent a considers that w0 might be the actual world.

The semantics of LEL is defined as follows:

• ÷ M↪ w ♣= p if w 2 V (p);
• ÷ M↪w ♣= ≻' if it is not the case thatM↪w ♣= ';
• ÷ M↪w ♣= ('_ ) ifM↪w ♣= ' orM↪w ♣= ;
• ÷ M↪w ♣=Ka' if for all w0 s.t. wRaw0 ,M↪w0 ♣= '.

Dynamic epistemic logic (DEL) extends epistemic logic with modalities that represent the occurrence of events. In DEL events are represented by event models, defined below. In general DEL events can bring information and modify the world, and such events are called ontic events [van Ditmarsch and Kooi, 2006]; in this work however we focus on purely informative events, called epistemic events [Baltag et al., 1998].

Definition 2 An event model E = (E↪ ¶!a♦a2Ag↪ pre) is a tuple where:

• ÷ E is a non-empty finite set of possible events,
• ÷ pre : E!LEL is a precondition function.
• ÷ !a✓ E⇥E is an accessibility relation on E for agent a,

We write e 2 E for e 2 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♦a2Ag↪ V ) an epistemic model and E = (E↪ ¶!a♦a2Ag↪ pre) an event model, the update product of M and E is the epistemic model M⌦ E = (W ⌦↪ ¶R⌦a ♦a2Ag↪ V ⌦) where:

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)) ifM↪ w ♣= pre(e), otherwise it is undefined.

We can now define the syntax and semantics of DEL. The syntax is given by the following grammar:

The semantics is the same as for LEL, with the following additional case:

where p 2 AP , i 2 Ag and (E↪ e) is a pointed event model.

• ÷ M↪ w ♣= hE↪ ei' if M↪ w ♣= pre(e), and (M↪w) ⌦ (E↪ e) ♣= '.

Example 1 Consider the pointed epistemic model (M↪w) in Figure 1(a). Proposition p is true in the actual world w but both agents a↪ b do not know that p holds: M↪ w ♣= ≻K1p ^ ≻K2p. Figure 1(b) shows a pointed event model (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.

Remark 1 We do not make any assumption on the nature of the accessibility relations in epistemic and event models.

2.2 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) 2 E (a plan) such that M↪ w ♣= hE1↪ e1i ▷ ▷ ▷ hEp↪ epi'g; no otherwise.

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

3 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 [Bolander et al., 2015]. We establish that it is actually PSPACE-complete.

As pointed out in [L¨owe et al., 2011], 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 h(E↪ e)` i 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 Lit C0 , is exponentially more succinct than DEL. Classically, the model checking problem for Lit C0 is, given a pointed epistemic model (M↪ w) and a formula Φ 2 Lit C0 , to decide whether M↪ w ♣= Φ.

Proof We design a deterministic algorithm that takes as an input a pointed epistemic model (M↪w0) and a formula Φ 2 Lit C0 , 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↪ ei1 ↪ ▷ ▷ ▷ ↪ eip ) are equivalent in the sense that either they all are worlds inM⌦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 repre-

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 2 M, all integers n1↪ ▷ ▷ ▷ ↪ n♣E♣ and all subformula ' of Φ, the following property P holds:

Property P is proven by induction on '. We omit the boolean cases and case h(E↪ ei)` i which are trivial.

Case Ka : the algorithm has to check that holds in all a-successors of w÷~n in M⌦ E P♣E♣ i=1 ni . 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 P♣E♣ i=1 ni . 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 2 ¶1↪ ▷ ▷ ▷ ↪ ♣E♣♦, if `i > 0 then pre(ei) is true in u. Next, we check that some permutation of u÷~` is indeed arelated to w÷~n: we should first have u 2 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)2¶1↪▷▷▷↪♣E♣♦2 ♣ej2Ra(ei) , where xi↪j is the number of times ej is chosen as a-successor for ei, such that:

This is done by calling succ(E↪ a↪ ~n↪ ~`).

Spatial complexity. The maximal number of nested calls is bounded by ♣Φ♣, so that the number of local variables to be stored is polynomial in ♣Φ♣. Next, the space used to store vector ~n in each call is in O(♣Φ♣2 ) (see [Charrier et al., 2016] for details). Finally, checking consistency of a system (S) can be done in non-deterministic time polynomial in the number of bits needed to encode ~n and ~` [Papadimitriou, 1981], and therefore in deterministic space polynomial in ♣Φ♣. ⌅

Theorem 1 The epistemic planning problem restricted to C0 is in PSPACE.

Proof We adapt the algorithm given in [Bolander et al., 2015] (Theorem 5.8). First it is proved in [Sadzik, 2006] that, noting 'd the d-bisimulation 1 for event models (see [Bolander et al., 2015; Sadzik, 2006; van Ditmarsch et al., 2007]), for every d ≥ 0, every pointed event model (E↪ e) is 'dstabilizing 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:

1. Compute d, the modal depth of the goal formula 'g;
2. For each i 2 ¶1↪ ▷ ▷ ▷ ↪m♦, non-deterministically guess ni 2 {0↪ ▷ ▷ ▷ ↪ ♣Ei♣d ;

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

1 Bisimulation up to modal depth d.

2 Actually a better bound is proved in [Bolander et al., 2015].

and thus in ♣'g♣, but its binary representation uses polynomial space. Since h(E1↪ e1)n1 i ▷ ▷ ▷ h(Em↪ em)nm i'g is an Lit C0 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 [Savitch, 1970]. ⌅

We now turn to the case of modal preconditions with bounded modal depth.

4 Preconditions of bounded modal depth

Let C2 be the class of event models with preconditions of modal depth at most two. In this section, we prove the following theorem by refining the reduction given in [Aucher and Bolander, 2013].

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 [Minsky, 1967], and then we reduce it to the epistemic planning problem restricted to C2.

4.1 Two-counter machines

We present two-counter machines as introduced in [Minsky, 1967].

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

• ÷ For each ` < N, I` is either inc(i), goto(`0 ) or gotocond(i↪ `0 ), with i 2 ¶1↪ 2♦, `0  N and ` 6= `0 ;

We call program line a pair k:Ik.

• ÷ IN = halt.

Example 2 The four program lines shown on the right define a twocounter 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 ` 2 ¶0↪ ▷ ▷ ▷ ↪N♦ is the program counter and c1↪ c2 2 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) 2 CM:

• ÷ If I` = inc(1), (`↪ c1↪ c2) !M (` + 1↪ c1 + 1↪ c2);
• ÷ If I` = inc(2), (`↪ c1↪ c2) !M (` + 1↪ c1↪ c2 + 1);
• ÷ If I` = goto(`0 ), (`↪ c1↪ c2) !M (`0 ↪ c1↪ c2) ;
• ÷ If I` = gotocond(1↪ `0 ), (`↪ c1↪ c2) !M ⇢(`0 ↪ 0↪ c2) if c1 = 0; (` +1↪ c1 -1↪ c2) otherwise;

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 twocounter machine, whether it halts or not. This problem is well known to be undecidable [Minsky, 1967].

4.2 The reduction

We define an effective reduction tr that, given a twocounter 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) = h(M0↪w0); E; 'gi and justifying its correctness (Proposition 2). As in [Aucher and Bolander, 2013], 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(`↪c1↪c2)↪w(`↪c1↪c2)) (shortened as (M↪w)(`↪c1↪c2)) that represents (`↪ c1↪ c2). For instance, Figure 3 shows (M↪ w)(1↪3↪2). It is a tree-like structure rooted at w(`↪c1↪c2). 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(`↪c1↪c2) verifies no atomic proposition, and it has three groups of children, one for each counter:

Program counter. For each program line `0 : I`0 , w(`↪c1↪c2) has one reflexive child labeled by proposition a`0 . The a`-child of w(`↪c1↪c2) has a child also labeled by a`, without any outgoing edge: we say that there is an a`-strip.

Data counter ci. For each i 2 ¶1↪ 2♦, w(`↪c1↪c2) has a reflexive pi-child that has an irreflexive qi-child, and is followed by a chain of irreflexive pi-worlds of length ci.

We now define the first component of tr(M): (M0↪w0) := (M↪w)(0↪0↪0), depicted in Figure 4. We call configuration model a pointed epistemic model of the form (M↪ w)(`↪c1↪c2).

Pointed event models

For each program line `:I` of M where I` is of the form goto(`0 ) 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 6 and 8). For each program line `:gotocond(i↪ `0 ) of M, we define two pointed event models (E↪ e)`:gotocond(i↪`0 ) and (E >0 ↪ e>0 )`:gotocond(i↪`0 ), respectively for the case ci = 0 and ci > 0 (Figure 9). These pointed event models form the second component of tr(M):

In model (M↪w)(`↪c1↪c2) 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:

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 ` 2 ¶0↪ ▷ ▷ ▷ ↪N♦ and a pi-child for each i 2 ¶1↪ 2♦.

Note that by definition, every configuration model is valid. Further down, we will define event models of E such that:

Lemma 2 For every configuration (`↪ c1↪ c2), it holds that a`0

Figure 6: Event model for `:goto(`0 ).

1. (M↪w)(`↪c1↪c2) ⌦ E(`↪ c1↪ c2) is isomorphic 3 to (M↪ w)(`0 ↪c01 ↪c02 ), where (`↪ c1↪ c2) !M (`0 ↪ c01 ↪ c02 ).
2. The product of (M↪w)(`↪c1↪c2) with any other event model from E is defined but not valid.
3. For any set of event models (E1↪ ▷ ▷ ▷ ↪ En) and any event model En+1, if (M↪w)(`↪c1↪c2) ⌦ E1 ⌦ · · · ⌦ En is not valid, (M↪ w)(`↪c1↪c2) ⌦ 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 6, 8, 9), 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(`0 ). The pointed event model (E↪ e)`:goto(`0 ), that mimics the effect of `:goto(`0 ), is depicted in Figure 6. Portion repl(`↪ `0 ) concerns the program counter group and is described in Figure 5. The two other groups leave the data counter groups c1 and c2 unchanged.

• ÷ The product (M↪w)(`↪c1↪c2)⌦(E↪ e)`:goto(`0 ) is isomorphic to (M↪ w)(`0 ↪c1↪c2): indeed, portion repl(`↪ `0 ) removes the a`-strip and adds an a`0 -strip in the program counter group (recall that ` 6= `0 ).
• ÷ The product (M↪ w)(`00 ↪c1↪c2) ⌦(E↪ e)`:goto(`0 ) with `00 6= ` is not valid. Indeed, as (M↪w)(`00 ↪c1↪c2) does not have an a`-strip in its program counter group, its a`-world violates precondition a` ^ ⌃⇤? in portion repl(`↪ `0 ). As a consequence, (M↪ w)(`00 ↪c1↪c2) ⌦ (E↪ e)`:goto(`0 ) has no a`-child at its root and is thus not valid.

Event model for ` : inc(i). Figure 8 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 pi ^ ≻⌃qi pi ^ ≻⌃qi ^ ⌃>

3 More precisely, the reachable parts of the pointed epistemic models are isomorphic.

Figure 8: Event model for `:inc(1).

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

• ÷ The product (M↪w)(`↪c1↪c2) ⌦ (E↪ e)`:inc(1) is isomorphic to (M↪ w)(`+1↪c1+1↪c2).
• ÷ For the same reason as for (E↪ e)`:goto(`0 ), the product (M↪ w)(`00 ↪c1↪c2) ⌦ (E↪ e)`:inc(1) with `00 6= ` is not valid.

Event models for ` : gotocond(i↪ `0 ). Figure 9 describes models (E↪ e)`:gotocond(1↪`0 ) and (E >0 ↪ e>0 )`:gotocond(1↪`0 ). They mimic the effect of ` : gotocond(1↪ `0 ) in case c1 = 0 and case c1 > 0, respectively (for ` : gotocond(2↪ `0 ), constructions are symmetric).

• ÷ (M↪w)(`↪0↪c2) ⌦ (E↪ e)`:gotocond(1↪`0 ) is isomorphic to (M↪w)(`0 ↪0↪c2): indeed, 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)(`↪c1↪c2) violates this precondition. It is thus removed, so that the product (M↪ w)(`↪c1↪c2) ⌦ (E↪ e)`:gotocond(1↪`0 ) is not valid.
• ÷ (M↪w)(`↪c1↪c2) ⌦ (E >0 ↪ e>0 )`:3gotocond(1↪`0 ) with c1 > 0 is isomorphic to (M↪w)(`+1↪c1-1↪c2). Indeed, portion shorten(1) (Figure 7) 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↪c2): indeed, this precondition checks that the length of the p1-chain is at least 1. The product (M↪ w)(`↪0↪c2)⌦(E >0 ↪ e>0 )`:gotocond(1↪`0 ) is thus not valid.
• ÷ For `00 6= `, (M↪w)(`00 ↪c1↪c2) ⌦ (E↪ e)`:gotocond(1↪`0 ) and (M↪ w)(`00 ↪c1↪c2) ⌦ (E >0 ↪ e>0 )`:gotocond(1↪`0 ) are not valid.

Note that the product of a non-valid pointed epistemic model with any pointed event model is not valid since no event model can create the missing children of the root without using postconditions.

Goal formula

The goal formula 'g in tr(M) is 'valid ^ 'halt, where:

• ÷ 'halt := ⌃(aN ^⌃⇤?).
• ÷ 'valid := VN`=0 ⌃a` ^⌃p1 ^⌃p2, and

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

The proof can be found in [Charrier et al., 2016].

4.3 Comparison

In [Aucher and Bolander, 2013] 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(`↪ `0 ) 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(`↪ `0 ) that only uses preconditions of modal depth two.

5 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 [Yu et al., 2013], with a non-elementary upper bound [Aucher et al., 2014] and a PSPACE lower bound [Bolander et al., 2015]; this a big gap that should be bridged.