Complexity Results in Epistemic Planning

Complexity Results in Epistemic Planning

Thomas Bolander DTU Compute

Tech. University of Denmark Copenhagen, Denmark

tobo@dtu.dk

Martin Holm Jensen DTU Compute

Tech. University of Denmark Copenhagen, Denmark

martin.holm.j@gmail.com

Francois Schwarzentruber IRISA

ENS Rennes Rennes, France

francois.schwarzentruber@ens-rennes.fr

Abstract

Epistemic planning is a very expressive framework that extends automated planning by the incorpora- tion of dynamic epistemic logic (DEL). We provide complexity results on the plan existence problem for multi-agent planning tasks, focusing on purely epistemic actions with propositional preconditions.

We show that moving from epistemic preconditions to propositional preconditions makes it decidable, more precisely in EXPSPACE. The plan existence problem is PSPACE-complete when the underly- ing graphs are trees and NP-complete when they are chains (including singletons). We also show PSPACE-hardness of the plan verification problem, which strengthens previous results on the complex- ity of DEL model checking.

1 Introduction

An all-pervading focus of artificial intelligence (AI) is the de- velopment of rational, autonomous agents. An important trait of such an agent is that it is able to exhibit goal-directed be- haviour, and this overarching aim is what is studied within the field of automated planning. At the same time, such goal-directed behaviour will naturally be confined to what- ever model of the underlying domain is used. In automated planning the domain models employed are formulated using propositional logic, but in more complex settings (e.g. multi- agent domains) such models come up short due to the lim- ited expressive power of propositional logic. By extending (or replacing) this foundational building block of automated planning we obtain a more expressive formalism for studying and developing goal-directed agents, enabling for instance an agent to reason about other agents.

For the above reasons automated planning has recently seen an influx of formalisms that are colloquially referred to as epistemic planning [Bolander and Andersen, 2011; L¨owe et al., 2011; Aucher and Bolander, 2013; Yu et al., 2013;

Andersenet al., 2012]. Common to these approaches is that they take dynamic epistemic logic (DEL) [Baltaget al., 1998]

as the basic building block of automated planning, which greatly surpasses propositional logic in terms of expressive power. Briefly put, DEL is a modal logic with which we

can reason about the dynamics of knowledge. In the single- agent case, epistemic planning can capture non-deterministic and partially observable domains [Andersenet al., 2012]. An even more interesting feature of DEL is the inherent ability to reason about multi-agent scenarios, lending itself perfectly to natural descriptions of multi-agent planning tasks.

In [Bolander and Andersen, 2011] it is shown that the plan existence problem (i.e. deciding whether a plan exists for a multi-agent planning task) is undecidable, and this re- mains so even when factual change is not allowed, that is, when we only allow actions that changes beliefs, not on- tic facts [Aucher and Bolander, 2013]. Allowing for factual change, a decidable fragment is obtained by restricting epis- temic actions to only have propositional preconditions [Yuet al., 2013] (in the full framework, preconditions of actions can be arbitraryepistemic formulas). The computational com- plexity of this fragment belongs to(d+ 1)-EXPTIME for a goal whose modal depth isd[Maubert, 2014].

In this work we consider exclusively the plan existence problem for classes of planning tasks where preconditions are propositional (as in most automated planning formalisms) and actions are non-factual (changing only beliefs). We show this problem to be in EXPSPACE in the general case, but also identify fragments with tight complexity results. We do so by using the notion of epistemic action stabilisation [van Ben- them, 2003; Miller and Moss, 2005; Sadzik, 2006], which allows us to put an upper bound on the number of times an action needs to be executed in a plan. This number depends crucially on the structural properties of the graph underlying the epistemic action. To achieve our upper bound complex- ity results we generalise a result of [Sadzik, 2006] on action stabilisation. We also tackle lower bounds, thereby showing a clear computational separation between these fragments.

Our contributions to the complexity of the plan existence problem are summarised in Table 1 (second column from the left), where we’ve also listed related contributions. The fragments we study have both a conceptual and technical motivation. Singleton epistemic actions correspond to pub- lic announcements of propositional facts, chains and trees to certain forms of private announcements, and graphs capture any propositional epistemic action. Possible applications of such planning fragments could e.g. be planning in games like Clue/Cluedo where actions can be seen as purely epistemic;

or synthesis of protocols for secure communication (where

Types of epistemic actions Underlying

graphs of actions

Non-factual, propositional preconditions

Factual, propositional preconditions

Factual, epistemic preconditions SINGLETONS

NP-complete (Theorem 5.1)

PSPACE-hard [Jensen, 2014]

PSPACE-hard [Jensen, 2014]

CHAINS

NP-complete

(Theorem 5.2)

?

(open question)

?

(open question) TREES PSPACE-complete

(Theorem 5.3, Theorem 5.4)

?

(open question)

?

(open question) GRAPHS

in EXPSPACE (Theorem 5.8)

in NON- ELEMENTARY [Yuet al., 2013]

Undecidable [Bolander and

Andersen, 2011]

Table 1: Complexity results for the plan existence problem.

the goal specifies who are allowed to know what).

Technically our fragments increase in complexity as we loosen the restrictions put on the underlying graph. Some planning tasks might therefore be simplified during a prepro- cessing phase so that a better upper bound can be guaranteed.

As a case in point, we can preprocess any planning task and replace each graph action with a tree action that is equiva- lent up to a predetermined modal depthk (by unravelling).

Lettingkbe the modal depth of the goal formula we obtain an equivalent planning task that can be solved using at most space polynomial inkand the size of the planning task. In au- tomated planning such preprocessing is often used to achieve scalable planning systems.

Our results also allow us to prove that the plan verification problem (a subproblem of DEL model checking) is PSPACE- hard, even without non-deterministic union, thereby improv- ing the result of [Aucher and Schwarzentruber, 2013].

Sections 2 and 3 present the core notions from epistemic planning. In Section 4 we improve the known upper bounds on the stabilisation of epistemic actions. This is put to use in Section 5 where we show novel results on the complexity of the plan existence problem. Section 6 presents our improve- ment to the plan verification problem, before we conclude and discuss future work in Section 7.

2 Background on Epistemic Planning

For the remainder of the paper we fix both an infinitely count- able set of atomic propositionsPand a finite set of agentsAg.

2.1 Dynamic epistemic logic

Definition 2.1(Epistemic models and states). Anepistemic modelis a triple M = (W, R, V) where the domainW is a non-empty set of worlds; R : Ag → 2^W×W assigns an epistemic (accessibility) relationto each agent; andV :P → 2^W assigns avaluationto each atomic proposition. We write Ra for R(a) andwRav for (w, v) ∈ Ra. We often write W^M for W,R_a^M forR_a andV^M forV. Forw ∈ W, the pair(M, w)is called anepistemic statewhoseactual world isw. (M, w)isfinitewhenW is finite. Epistemic states are typically denoted by symbols such assands0.

The language of propositional logic overP is referred to asLProp, or sometimes simply thepropositional language.

Definition 2.2(Propositional action models and epistemic actions). A propositional action model is a triple A = (E, Q, pre)whereE is a non-empty and finite set ofevents called thedomainofA;Q : Ag → 2^E×E assigns anepis- temic (accessibility) relationto each agent; andpre : E → LPropassigns apreconditionof the propositional language to each event. We writeQ_aforQ(a)andeQ_affor(e, f)∈Q_a. We often writeE^AforE,Q^A_a forQaandpre^Aforpre. For e ∈ E, the pair (A, e)is called anepistemic action whose actual event is e. Epistemic actions are typically denoted α, α⁰, α1, etc.

Propositional action models are defined to fit exactly our line of investigation here, though other presentations consider preconditions of more complex languages and postconditions that allow for factual (ontic) change [Bolander and Andersen, 2011; Yuet al., 2013].

Thedynamic languageLDis generated by the BNF:

ϕ:=p| ¬ϕ|(ϕ∧ϕ)|aϕ| hαiϕ

wherea ∈ Ag,p ∈ P andαis an epistemic action. Here a denotes theknowledge (or, belief) modalitywhereaϕ reads as “aknows (or, believes)ϕ”, andhαiis thedynamic modality wherehαiϕreads as “αis applicable andϕholds after executingα”. Theepistemic languageLEis the sublan- guage ofL_Dthat does not contain the dynamic modality. As usual we use♦^aϕ:=¬^a¬ϕ, and define by abbreviation>,

⊥and the boolean connectives∨,→,↔. Lastly, we define hαi⁰ϕ:=ϕandhαi^kϕ:=hαi(hαi^k−1ϕ)fork >0.

Definition 2.3(Semantics). Let(M, w)be an epistemic state whereM = (W, R, V). Fora∈Ag,p∈P andϕ, ϕ⁰ ∈L_D we inductively define truth of formulas as follows, omitting the propositional cases:

(M, w)|=aϕ iff(M, v)|=ϕfor allwR_av (M, w)|=hαiϕ iff(M, w)|=pre(e)

and(M ⊗A,(w, e))|=ϕ whereα= (A, e)is an epistemic action s.t.A= (E, Q, pre), and the epistemic modelM ⊗A = (W⁰, R⁰, V⁰)is defined via theproduct updateoperator⊗by:

W⁰ = {(v, f)∈W×E|(M, v)|=pre(f)}, R⁰_a = {((v, f),(u, g))∈W⁰×W⁰|vR_au, f Q_ag}, V⁰(p) = {(v, f)∈W⁰|v∈V(p)}forp∈P.

For any epistemic states= (M, w)and epistemic action α= (A, e)satisfying(M, w)|=pre^A(e), we defines⊗α= (M ⊗A,(w, e)). The epistemic states⊗αrepresents the result of executingαins. Note that we haves |=hαiϕiff (M, w) |=pre^A(e)ands⊗α|=ϕ. Two formulasϕ, ϕ⁰ of L_Dare calledequivalent(written asϕ≡ϕ⁰) whens|=ϕiff s|=ϕ⁰for every epistemic states.

Example 2.4. Consider the epistemic state s1 of Figure 1.

It represents a situation where pholds in the actual world (w), but where the two agents, a and b, don’t know this:

s₁ |= p∧ ¬ap∧ ¬bp. Consider now the epistemic ac- tionα1 = (A, e)of the same figure. It represents a private announcement ofpto agenta, that is, agentais told thatp holds (the actual event,e), but agentbthinks that nothing is

w:p v:

s1 a, b a, b a, b

e:p f:>

α1 a b a, b (w, e) :p

(w, f) :p

(v, f) :

s1⊗α1

b b a a, b

a, b

a, b

Figure 1: (Top left) An epistemic states1. We mark each world (circle) with its name and the atomic propositions that are true. The actual world is coloured black. Edges show epistemic relations of the agents. (Bottom left) An epistemic action α₁. We use the same conventions as for epistemic states, except an event (square) is marked by its name and its precondition. (Right) The epistemic model to the right is the result of execution ofα1ins1, that is,s1⊗α1.

happening (eventf). The dynamic modality allows us to rea- son about the result of executingα₁ins₁, so for instance we haves1|=hα1i(^ap∧ ¬^bp∧ ¬^bap): After agentahas been privately informed aboutp, she will know it, butbwill still not knowp, and will believe thatadoesn’t either. This fact can be verified by observing that^ap∧ ¬^bp∧ ¬^bap is true in the epistemic states₁⊗α₁of Figure 1.

2.2 Plan existence problem

Definition 2.5 (Planning tasks). An (epistemic) planning task is a triple T = (s0,L, ϕg) wheres0 is a finite epis- temic state called the initial state, L is a finite set of epis- temic actions called theaction libraryandϕg ∈LEis called the goal. Aplan for T is a finite sequence α₁, . . . , α_j of epistemic actions fromLs.t. s0|=hα1i · · · hαjiϕg. The se- quenceα₁, . . . , α_jcan contain any number of repetitions, and can also be empty. We say thatT issolvableif there exists a plan for T. The size of a planning task T = (s0,L, ϕg) is given as follows. Following [Aucher and Schwarzen- truber, 2013], for any α = (A, e) in L we define |α| =

|Ag| · |E^A|²+P

e∈E|pre(e)|as thesize ofα, where|pre(e)|

denotes the length of the (propositional) formulapre(e). The size of an epistemic action is always a finite number, since the domain of any propositional action model and Ag are both fi- nite. LetP⁰ ⊆P be the finite set of atomic propositions that occur either in some precondition of anα∈ Lor inϕg. The sizeT is then|T|=|P⁰| · |Ag| · |W^M|²+P

α∈L|α|+|ϕg| wheres₀= (M, w).

Note that a plan is nothing more than a sequence of epis- temic actions leading to a goal. It is not hard to show that this definition is equivalent to the definition of a solution [Aucher and Bolander, 2013] and an explanatory diagnosis [Yuet al., 2013], which are both special cases of a solution to a classical planning task as defined in [Ghallabet al., 2004] (for the re- lation to classical planning tasks, see [Aucher and Bolander, 2013]).

Example 2.6. Consider again Figure 1. We’ll useα₂to refer to the private announcement of pto b, obtained simply by swapping the epistemic relations ofaandbinα₁. Consider the planning taskT = (s,{α1, α2}, ϕg)withϕg = ^ap∧

^bp∧ ¬^abp∧ ¬^bap. It is a planning task in which the only available actions are private announcements ofpto eitheraorb, and the goal is for bothaandbto knowp, but without knowing that the other knows. A plan forTisα1, α2, sinces |= hα₁ihα₂iϕ_g. In other words, first announcingp privately toaand then privately tobwill achieve the goal of them both knowingpwithout knowing that each other knows.

Definition 2.7(Plan existence problem). LetX denote a class of planning tasks. Theplan existence problem forX, called PLANEX(X)is the following decision problem: Given a planning taskT ∈X, does there exists a plan forT?

3 Background on Iterating Epistemic Actions

To get to grips on the plan existence problem, we now con- sider the result of iterating a single epistemic action. We then proceed to derive a useful characterisation of exactly when a planning task is solvable.

Definition 3.1(n-ary product). Letα= (A, e)be an epis- temic action whereA = (E, Q, pre). We denote byAⁿ = (Eⁿ, Qⁿ, preⁿ)then-ary product ofA. We defineE⁰={e}, eQ⁰_aefor eacha∈Ag, andpre⁰(e) =>. Forn >0we de- fine

– Eⁿ ={(e1, . . . , en)|ei∈Efor alli= 1, . . . , n}, – Qⁿ_a ={((e1, . . . , en),(f1, . . . , fn))|eiQafi

for alli= 1, . . . , n}for eacha∈Ag, and – preⁿ((e1, . . . , en)) =V

i=1,...,npre(ei).

Then-ary product ofαis defined asαⁿ = (Aⁿ, eⁿ), where eⁿdenotes(e, e, . . . , e)

| {z }

n

.

This is not the standard definition of then-ary product of an action model, which instead goes via a definition of the product update operator on action models. Definition 3.1 is equivalent to the standard definition when preconditions are ofLProp. The following lemma is derived from the axioma- tization of [Baltaget al., 1998] (relying in particular on ac- tion composition), and is here stated for the case of then-ary product and utilising that preconditions are ofL_Prop.

Lemma 3.2. For any epistemic actionαand anyϕ∈LEwe have thathαiⁿϕ≡ hαⁿiϕ.

This lemma expresses that executing an epistemic actionn times is equivalent to executing itsn-ary product once.

3.1 Bisimilarity and Stabilisation

Concerningn-ary products of epistemic actions, an interest- ing case is when executing the n-ary product is equivalent to executing the (n+ 1)-ary product. This puts an upper bound on the number of times the action needs to occur in a plan since epistemic actions with propositional preconditions commute [L¨oweet al., 2011]. To analyse this, we introduce notions of bisimulation andn-bisimulation on action models (slightly reformulated from [Sadzik, 2006]).

Definition 3.3 (Bisimilarity). Two epistemic actions α = (A, e)andα⁰ = (A⁰, e⁰)are calledbisimilar, writtenα↔α⁰, if there exists a (bisimulation) relationZ ⊆E^A×E^A0 con- taining(e, e⁰)and satisfying for everya∈Ag:

– [atom]If(f, f⁰)∈Zthenpre^A(f)≡pre^A0(f⁰), – [forth]If(f, f⁰)∈Zandf Q^A_agthen there is ag⁰ ∈E^A0

such thatf⁰Q^A_a⁰g⁰and(g, g⁰)∈Z, and

– [back]If(f, f⁰) ∈ Z andf⁰Q^A_a⁰g⁰ then there is ag ∈ E^Asuch thatf Q^A_agand(g, g⁰)∈Z.

Definition 3.4(n-bisimilarity). Letα = (A, e)andα⁰ = (A⁰, e⁰)be epistemic actions. They are0-bisimilar, written α↔₀α⁰, ifpre^A(e) ≡ pre^A0(e⁰). Forn > 0, they are n- bisimilar, writtenα↔_nα⁰, if for everya∈Ag:

– [atom]pre^A(e)≡pre^A0(e⁰),

– [forth] IfeQ^A_af then there is an f⁰ ∈ E^A0 such that e⁰Q^A_a⁰f⁰and(A, f)↔_n−1(A⁰, f⁰), and

– [back]Ife⁰Q^A_a⁰f⁰ then there is anf ∈ E^A such that eQ^A_af and(A, f)↔_n−1(A, f⁰).

The modal depth md(ϕ) of a formula ϕ is defined as: md(p) = 0; md(¬ϕ) = md(ϕ); md(ϕ ∧ ψ) = max{md(ϕ), md(ψ)}; md(^aϕ) = 1 + md(ϕ);

md(hαiϕ) =md(ϕ). As epistemic actions have only propo- sitional preconditions,hαi-operators do not count towards the modal depth. This definition of modal depth, Lemma 3.5 and Definition 3.6 are all due to [Sadzik, 2006] (slightly reformu- lated).

Lemma 3.5. Letα,α⁰be two epistemic actions andϕ∈L_D. 1) Ifα↔α⁰, thenhαiϕ≡ hα⁰iϕ.

2) Ifmd(ϕ)≤nandα↔_nα⁰, thenhαiϕ≡ hα⁰iϕ.

Definition 3.6(Stabilisation). Letαbe an epistemic action.

1) αis↔-stabilising at stageiifαⁱ↔α^i+kfor allk≥0.

2) αis↔_n-stabilising at stageiifαⁱ↔_nα^i+kfor allk≥ 0.

Example 3.7. The2-ary productα²₁ofα1of Figure 1 is:

(e, e) :p∧p (f, f) :> ∧ >

(f, e) :> ∧p

(e, f) :p∧ >

a a, b

a

a b

b b

It is easy to check that α1↔α²₁, using Z = {(e,(e, e)),(f,(f, f))}, This argument can be extended to show thatα1is indeed↔-stabilising at stage1.

Since any epistemic action is finite, we have:

Lemma 3.8. If two epistemic actions aren-bisimilar for all n, then they are bisimilar.

3.2 Bounding the Number of Iterations

We’re now ready to present our characterisation of when a planning task is solvable. We note that Proposition 3.9 below echoes the sentiment of [Yuet al., 2013, Theorem 5.15], in that it states the conditions under which we can restrict the search space when looking for a plan.

Proposition 3.9. LetT = (s₀,{α1, . . . , α_m}, ϕg)be a plan- ning task andB ∈N. Suppose one of the following holds:

1) Everyαiis↔-stabilising at stageB, or

2) md(ϕg) =nand everyαiis↔_n-stabilising at stageB.

ThenTis solvable iff there existsk₁, . . . , k_m≤Bs.t. s₀ |= hα^k₁¹i · · · hα_m^kmiϕg.

Proof. Assume 2) holds (the case of 1 is similar). Assume T is solvable, and letαi₁, . . . , ai_j be a plan forT. Due to commutativity of propositional action models so is any per- mutation ofαi₁, . . . , αi_j [Yuet al., 2013]. We therefore have s₀|=hα1i^k01· · · hαmi^k0mϕ_gfor some choice ofk⁰_i≥0. Using Lemma 3.2, it follows thats0|=hα^k₁¹⁰i · · · hα^km^0miϕg. We now letk_i = min(k_i⁰, B)for alli. By assumption,md(ϕ_g) = n and so by definitionmd(hαiϕg) =nfor any epistemic action α. Combining this with the assumption that everyα_iis↔_n- stabilising at stageB ≥ ki, we apply 2) of Lemma 3.5 m times to conclude thats₀ |=hα₁^k1i · · · hα^k_m^miϕg, as required.

The proof of the other direction follows readily from Lemma 3.2 and the definition ofhαi^k.

LetT = {s0,L, ϕg}be a planning task with md(ϕg) = n. Given the proposition above, to show that T is solvable we only need to find the correct number of times to iterate each of the actions inL, and these numbers never have to exceedBfor actions that are↔_n-stabilising at stageB. The following result, due to [Sadzik, 2006], shows that such a boundBexists for any epistemic action.

Lemma 3.10. Letα= (A, e)be an epistemic action andna natural number. Thenαis↔_n-stabilising at stage|E^A|ⁿ.

4 Better Bounds for Action Stabilisation

In this section, we prove an original contribution, Lemma 4.2, that generalises Sadzik’s Lemma 3.10 by giving a better bound for action stabilisation. The overall point is this:

Sadzik gets an unnecessarily high upper bound on when an epistemic action(A, e)stabilises by considering it possible that any event can have up to|E^A|successors. We get a bet- ter bound by counting paths.

Definition 4.1(Underlying graphs). Let(A, e)be an epis- temic action. We defineQ^A = ∪a∈AgQ^A_a. Theunderlying graphof(A, e)is the directed graph(A,Q^A)with roote.

Let(A, e)denote an epistemic action. Note that(e, f) ∈ Q^A iff there is an edge from etof inA labelled bysome agent. Standard graph-theoretical notions carry over to epis- temic actions via their underlying graphs. For instance, we define apath of lengthn in(A, e)as a path of lengthnin the underlying graph, that is, a sequence(e₁, e₂, . . . , e_n+1) of events such that(ei, ei+1)∈Q^Afor alli= 1, . . . , n(we allown= 0and hence paths of length0). Apath of length

≤nis a path of length at mostn. Amaximal path of length

≤nis a path of length≤nthat is not a strict prefix of any other path of length≤n. We usempaths_n(e)to denote the number of distinct maximal paths of length≤nrooted ate. If all nodes have successors, this number is simply the number of distinct paths of lengthn. Note thatmpaths_n(e)is always a positive number, as there is always at least one path rooted ate(even ifehas no outgoing edges, there is still the path of length0). Note also that for anyn > 0 and any evente having at least one successor in the underlying graph:

mpaths_n(e) =P

eQ^Afmpaths_n−1(f). (1) In the epistemic action α1 of Figure 1 we have mpaths₂(e) = 3, since there are three paths of length 2, (e, e, e),(e, e, f)and(e, f, f), and no shorter maximal paths.

Lemma 4.2. Let α = (A, e0)be an epistemic action and n any natural number. Then αis ↔_n-stabilising at stage mpaths_n(e₀).

Proof. Whenf = (f₁, . . . , f_m) ∈ E^Am and e ∈ A, we use occ(e,f) to denote the number of occurrences of e in f₁, . . . , f_m. For instance we haveocc(e,(e, e, f, f)) = 2. We now prove the following propertyP(n) by induction onn.

P(n): Ife ∈ E^Ak+1 ande⁰ ∈ E^Ak only differ by some evente^∗occurring at leastmpaths_n(e^∗)+1times ineand at leastmpaths_n(e^∗)times ine⁰, then(A^k+1,e)↔_n(A^k,e⁰).

Base case P(0): Since mpaths₀(e^∗) = 1, e and e⁰ as described above must contain exactly the same events (but not necessarily with the same number of occurrences).

By definition of the n-ary product of an epistemic ac- tion we get pre^Ak+1(e) ≡ pre^Ak(e⁰). This shows (A^k+1,e)↔₀(A^k,e⁰). For the induction step, assume that P(n−1)holds. Giveneande⁰as described inP(n), we need to show (A^k+1,e)↔_n(A^k,e⁰). [atom]is proved as P(0).

[forth]: Letaandf be chosen such thateQ^A_a^k+1f. We need to findf⁰such thate⁰Q^A_a^kf⁰and(A^k+1,f)↔_n−1(A^k,f⁰).

Claim. There exists an f^∗ such that e^∗Q^A_af^∗ and occ(f^∗,f)≥mpaths_n−1(f^∗) + 1.

Proof of Claim. By contradiction: Suppose occ(f,f) ≤ mpaths_n−1(f)for allf withe^∗Q^A_af. SinceeQ^A_a^k+1f, the number of occurrences of e^∗ ine is equal or less than the number of occurrences ofQ_a-successors ofe^∗ inf. Hence we get

occ(e^∗,e)≤P

e^∗Q^A_afocc(f,f)

≤P

e^∗Q^A_afmpaths_n−1(f) (by assumption)

≤P

e^∗Q^Afmpaths_n−1(f) (byQ^A=∪a∈AgQ^A_a)

= mpaths_n(e^∗) (by equation (1)).

However, this directly contradicts the assumption thate^∗oc- curs at leastmpaths_n(e^∗) + 1times ine, and hence the proof of the claim is complete.

Letf^∗be as guaranteed by the claim. Now we buildf⁰to be exactly likef, except we omit one of the occurrences off^∗ (we do not have to worry about the order of the elements of the vectors, since any two vectors only differing in order are bisimilar [Sadzik, 2006]). Sincefandf⁰now only differ inf^∗ occurring at leastmpaths_n−1(f^∗) + 1times inf and at least mpaths_n−1(f^∗)times inf⁰, we can use the induction hypoth- esisP(n−1) to conclude that(A^k+1,f)↔_n−1(A^k,f⁰), as required.[back]: This is the easy direction and is omitted.

Now we have proved P(n) for all n. Given n, fromP(n)it follows that(A^k+1, e^k+1₀ )↔_n(A^k, e^k₀)for all k≥mpaths_n(e₀). And from this it immediately follows that (A, e0)is↔_n-stabilising at stagempaths_n(e0).

r: s0

w1:p1

w2:p2 w3:p3 wm:pn

· · ·

a a a a

ei:¬pi

αi

a

Figure 2: Initial state and actions used in Theorem 5.1.

procedurePlanExists (s₀,{α₁, . . . , α_m}, ϕ_g), B a) Guess a vector(k₁, . . . , k_m)∈ {0, . . . , B}^m. b) Accept whens0|=hα1i^k1· · · hαmi^kmϕg.

Figure 3: Non-deterministic algorithm for the plan existence problem.

5 Complexity of the Plan Existence Problem

We define SINGLETONS as the class of planning tasks (s0,L, ϕg), where everyα= (A, e)inLis asingleton; i.e.

E^Acontains a single event.

Theorem 5.1. PLANEX(SINGLETONS)is NP-complete.

Proof. For any singleton epistemic action there is at mostone maximal path of length≤nfor alln. Hence, by Lemma 4.2 and 3.8, such actions are↔-stabilising at stage 1.In NP:Fol- lows from Theorem 5.2 below as SINGLETONSis contained in CHAINS. NP-hard: We give a polynomial-time reduc- tion from SAT. Letϕ(p1, . . . , pm)be a propositional formula wherep₁, . . . , p_mare the atomic propositions inϕ. We con- struct T = (s0,{α1, . . . , αm}, ϕg) s.t. s0 and each αi are as in Figure 2 andϕ_g =ϕ(♦ap₁, . . . ,♦ap_m)is the formula ϕin which each occurrence ofpi is replaced by♦^api. For any propositional valuationν, letsν be the restriction ofs0

s.t. there is ana-edge fromrtowi insν iffν |= pi. This means ν |= pi iffsν |= ♦^api, and so from our construc- tion ofϕ_gwe haveν |= ϕiffs_ν |= ϕ_g. Observe now that s0⊗αi is exactly the restriction ofs0 so that there is noa- edge fromrtow_i, and thatα_iis the only action affecting this edge. Letν(pi) = 0ifν |=piandν(pi) = 1otherwise. We now have thatϕis satisfiable iff there is aν s.t. ν |= ϕiff sν |= ϕg iffs0 |= hα1i^ν(p1)· · · hαmi^ν(pm)ϕg iffT is solv- able, where the last equivalence follows from Proposition 3.9 sinceν(pi)∈ {0,1}and eachαiis↔-stabilising at stage 1.

This shows thatϕis satisfiable iffTis solvable.

For an epistemic actionα= (A, e)we say thatαis achain if its underlying graph(A,Q^A)is a 1-ary tree whose unique leaf may beQ^A-reflexive. We define CHAINSas the class of planning tasks(s₀,L, ϕg)where every epistemic action inL is a chain.

Theorem 5.2. PLANEX(CHAINS)is NP-complete.

Proof. In NP:For any chain epistemic action there is at most one maximal path of length≤nfor all n, hence any such action is ↔-stabilising at stage 1 using Lemmas 4.2 and 3.8. It therefore follows from Proposition 3.9 that, for any T ∈ CHAINS,PlanExists(T,1)of Figure 3 is accepting iff T is solvable. We must show step b) to run in polynomial

time. Now ifαis a chain andsan epistemic state, then the number of worlds reachable from the actual world ins⊗αis at most the number of worlds ins. By only keeping the reach- able worlds after each successive product update, we get the required, as the goal is inL_E.¹ NP-hard:Follows from The- orem 5.1 as SINGLETONSis contained in CHAINS.

5.2 Tree Epistemic Actions

We now turn to epistemic actions whose underlying graph is a any tree. Formally, an epistemic action(A, e)is called atree when the underlying graph(A,Q^A) is a tree whose leaves may beQ^A-reflexive. We call TREES the class of planning tasks(s₀,L, ϕg)where all epistemic actions inLare trees.

Theorem 5.3. PLANEX(TREES)is in PSPACE.

Proof. Consider any tree action α = (A, e) and let l(α) denote its number of leaves. As α is a tree, we get mpaths_n(e) ≤ l(α)for anyn. Using Lemma 4.2 and 3.8, any tree epistemic action α is ↔-stabilising at stage l(α).

From Proposition 3.9 we therefore have, for anyT ∈TREES, that PlanExists(T,max(l(α₁), . . . , l(α_m))) of Figure 3 is accepting iffTis solvable. Step b) can be done in space poly- nomial in the size of the input [Aucher and Schwarzentruber, 2013]. Hence, the plan existence problem for TREES is in NPSPACE and therefore in PSPACE by Savitch’s Thm.

We now sketch a proof of PSPACE-hardness of PLANEX(TREES), by giving a polynomial-time reduction from the PSPACE-hard problem QSAT (satisfiability of quan- tified boolean formulas) to PLANEX(TREES). For any quan- tified boolean formula Φ = Q₁p₁· · ·Q_np_nϕ[p₁, . . . , p_n] with Qi ∈ {∀,∃}, we define the planning task TΦ = (s₀,{α₁, . . . , α_n}, ϕ_sat∧ϕ_all)wheres₀ and each α_i are as in Figure 4 (every edge implicitly labelled bya),

ϕ_sat=O₁· · ·O_nϕ[♦¹aa⊥, . . . ,♦ⁿaa⊥], and ϕ_all=♦ⁿ⁺¹a a⊥ ∧ · · · ∧♦²ⁿa a⊥,

whereOi =♦^a ifQi =∃andOi =^a ifQi =∀. Then

|TΦ|is polynomial in|Φ|andTΦ∈TREES. By Lemmas 5.6 and 5.7 below we getTΦis solvable iffΦis true. Hence:

Theorem 5.4. PLANEX(TREES)is PSPACE-hard.

w0:

s0

w1:

w2n+1: .. .

bⁱ₀:>

αi

bⁱ_i−1:>

tⁱ_i:>

tⁱ_n−1:>

f_iⁱ:>

f_n−1ⁱ :>

tⁱ_n:> f_nⁱ:>

tⁱ_n+1:>

tⁱ_2n+1:>

f_n+1ⁱ :>

f_2n+1ⁱ :>

cⁱ₁:>

cⁱ_i:>

..

.. ..

.. ..

..

Figure 4: Initial state and actions used in Theorem 5.4.

1Observe that even if each action inα1, . . . , αmis↔-stabilising at stage 1, this is not a sufficient condition for membership in NP as we must also be able to verify the plan in polynomial time.

(w0, b¹₀, b²₀)

(w₁, t¹₁, b²₁) (w₁, f₁¹, b²₁) (w2, t¹₂, t²₂) (w2, t¹₂, f₂²) (w2, f₂¹, t²₂) (w2, f₂¹, f₂²)

Noncⁱ_i-chain

c¹₁-chain c²₁, c²₂-chain

Figure 5: Binary decision tree simulated bys0 ⊗α1 ⊗α2

(n= 2).

The reduction is based on the idea that we can simulate a (complete) binary decision tree usings⁰=s0⊗α1⊗· · ·⊗αn. Each world at depthnofs⁰ simulates a valuation, using the convention thatpiis true iff there is a maximal chain of length iin this world. By nesting belief modalities we can check if such a chain exists. Each actionαimakes two copies of every node between depthiandn, which is how we can simulate every valuation.

A world w at depth i ≤ n of s⁰ is called an i-world.

It can now be verified that any i-world is of the form (wi, v¹_i, . . . , vⁱ_i, bⁱ⁺¹_i , . . . , bⁿ_i)wherev_i^j ∈ {t^j_i, f_i^j}. See also Figure 5. For anyi-worldw, we define a propositional valu- ationνwon{p1, . . . , pi}byνw|=pj ifft^j_i occurs inw. We usew0= (w0, b¹₀, . . . , bⁿ₀)to denote the single0-world ins⁰ (the actual world ofs⁰), and defineM⁰so thats⁰ = (M⁰,w₀).

Lemma 5.5. Let w be any n-world. Then (M⁰,w) |= ϕ[♦¹aa⊥, . . . ,♦ⁿaa⊥]iffν_w|=ϕ[p₁, . . . , p_n]is true.

Proof sketch. Due to thecⁱ₁, . . . , cⁱ_ichain in eachαi, we have for anyn-worldwandi≤nthat(M⁰,w)|=♦ⁱa^a⊥ifftⁱ_n occurs inw, from which the result readily follows.

We say that an n-world w is accepting if (M⁰,w) |= ϕ[♦¹aa⊥, . . . ,♦ⁿaa⊥], and for i < nwe say that the i- worldwis accepting if some (every) childw⁰ofwis accept- ing andOi=♦^a(Oi=^a).

Lemma 5.6. TΦis solvable iffw0is accepting.

Proof sketch. As acceptance fori < nexactly corresponds to the O1· · ·On prefix, we use Lemma 5.5 to show that (M⁰,w₀) |= ϕ_sat iffw₀ is accepting. Now we must show:

1)(M⁰,w0)|=ϕall, and then 2)TΦis solvable iffα1, . . . , αn

is plan forT_Φ. We omit proofs of both 1) and 2).

Lemma 5.7. Φis true iffw0is accepting.

Proof sketch. Letw denote anyi-world. Letνw(pi) = >

ifν_w |= p_i andν_w(p_i) = ⊥otherwise. We defineΦ_w = Qi+1pi+1· · ·Qnpnϕ[νw(p1), . . . , νw(pi), pi+1, . . . , pn].

By induction on k we now show: If k ≤ n and w is an (n−k)-world, then Φw is true iff w is accepting.

For the base case, k = 0 and w is an n-world, hence ϕ[νw(p1), . . . , νw(pn)](= Φw) is true iffwis accepting by Lemma 5.5. For the induction step we assume that for any (n−(k−1))-worldw⁰,Φ_w⁰ is true iffw⁰is accepting. Let wbe an(n−k)-world. By construction,whas two children vandu. We can then show thatΦ_vandΦ_uare asΦ_w, except theQ_n−k+1p_n−k+1prefix and that one setsp_n−k+2true and the other setsp_n−k+2false. ThusΦ_wis true iffQ_n−k+1=∃ (or,Qn−k+1 =∀) andΦw⁰is true for some (every) childw⁰

ofw. Using the induction hypothesis, we get thatΦwis true iffw⁰ is accepting for some (every) child w⁰ ofw. Hence, Φ_wis true iffw is accepting, by definition. This concludes the induction proof. Fork=nit follows thatΦw₀ is true iff w₀is accepting. SinceΦ = Φ_w0 we are done.

5.3 Arbitrary Epistemic Actions

We call GRAPHS the class of planning tasks (s0,L, ϕg) where all event models inLare arbitrary graphs. In this case, the original result by Sadzik (Lemma 3.10) is sufficient.

Theorem 5.8. PLANEX(GRAPHS)is in EXPSPACE.

Proof. We consider(s₀,{α1, . . . , α_m}, ϕg)∈GRAPHSwith αi= (Ai, ei)andmd(ϕg) =d. By Lemma 3.10, eachαi is

↔_d-stabilising at stage|E^Ai|^d. It now follows from Propo- sition 3.9 thatPlanExists(T,max{|E^A1|^d, . . . ,|E^Am|^d})of Figure 3 is accepting iffT is solvable. The algorithm runs in NEXPSPACE = EXPSPACE.

6 Complexity of the Plan Verification Problem

The plan verification problem is defined as the following de- cision problem: Given a finite epistemic states0 and a for- mula of the formhα1i · · · hαjiϕg, doess0|=hα1i · · · hαjiϕg

hold? The plan verification problem can be seen as a restric- tion of the model checking problem in DEL. A similar reduc- tion as for Theorem 5.4 gives that:

Theorem 6.1. The plan verification problem (restricted to propositional action models that are trees) is PSPACE-hard.

Model checking in DEL with the non-determinism oper- ator ∪ included in the language has already been proved PSPACE-hard [Aucher and Schwarzentruber, 2013]. Theo- rem 6.1 implies that model checking in DEL is PSPACE-hard even without this operator. A similar result has been indepen- dently proved in [van de Polet al., 2015].

7 Future Work

We remind the reader that an overview of our contributions are found in Table 1 and proceed to discuss future work.

Since propostional STRIPS planning is PSPACE-complete [Bylander, 1994], efficient planning systems have used re- laxed planning tasks in order to efficiently compute precise heuristics. For instance, the highly influential Fast-Forward planning system [Hoffmann and Nebel, 2001] relaxes plan- ning tasks by ignoring delete lists. Our contributions here show that restrictions on the graphs underlying epistemic actions crucially affect computational complexity. This, in combination with restrictions on preconditions and postcon- ditions (factual change), provides a platform for investigating (tractable) relaxations of epistemic planning tasks, and hence for the development of efficient epistemic planning systems.

References

[Andersenet al., 2012] Mikkel Birkegaard Andersen, Thomas Bolander, and Martin Holm Jensen. Conditional epistemic planning. In Luis Fari˜nas del Cerro, Andreas Herzig, and J´erˆome Mengin, editors,JELIA, volume 7519

of Lecture Notes in Computer Science, pages 94–106.

Springer, 2012.

[Aucher and Bolander, 2013] Guillaume Aucher and Thomas Bolander. Undecidability in epistemic planning.

In Francesca Rossi, editor,IJCAI. IJCAI/AAAI, 2013.

[Aucher and Schwarzentruber, 2013] Guillaume Aucher and Franc¸ois Schwarzentruber. On the complexity of dynamic epistemic logic. InTARK, 2013.

[Baltaget al., 1998] Alexandru Baltag, Lawrence S. Moss, and Slawomir Solecki. The logic of public announce- ments, common knowledge, and private suspicions. In TARK, 1998.

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

[Bylander, 1994] Tom Bylander. The computational com- plexity of propositional strips planning. Artificial Intel- ligence, 69(1-2):165–204, 1994.

[Ghallabet al., 2004] Malik Ghallab, Dana S. Nau, and Paolo Traverso. Automated Planning: Theory and Prac- tice. Morgan Kaufmann, 2004.

[Hoffmann and Nebel, 2001] J¨org Hoffmann and Bernhard Nebel. The ff planning system: Fast plan generation through heuristic search. Journal of Artificial Intelligence Resesearch, 14(1):253–302, May 2001.

[Jensen, 2014] Martin Holm Jensen.Epistemic and Doxastic Planning. PhD thesis, Technical University of Denmark, 2014. DTU Compute PHD-2014.

[L¨oweet al., 2011] Benedikt L¨owe, Eric Pacuit, and An- dreas Witzel. Del planning and some tractable cases. In Hans van Ditmarsch, J´erˆome Lang, and Shier Ju, editors, Logic, Rationality, and Interaction, volume 6953 ofLec- ture Notes in Computer Science, pages 179–192. Springer Berlin Heidelberg, 2011.

[Maubert, 2014] Bastien Maubert. Logical foundations of games with imperfect information: uniform strategies.

PhD thesis, 2014. PhD thesis directed by Pinchinat, So- phie and Aucher, Guillaume. Universit´e de Rennes 1.

[Miller and Moss, 2005] Joseph S Miller and Lawrence S Moss. The undecidability of iterated modal relativization.

Studia Logica, 79(3):373–407, 2005.

[Sadzik, 2006] Tomasz Sadzik. Exploring the Iterated Up- date Universe. ILLC Publications PP-2006-26, 2006.

[van Benthem, 2003] Johan van Benthem. One is a lonely number: On the logic of communication. 2003.

[van de Polet al., 2015] Iris van de Pol, Iris van Rooij, and Jakub Szymanik. Parameterized complexity results for a model of theory of mind based on dynamic epistemic logic. InTARK, 2015.

[Yuet al., 2013] Quan Yu, Ximing Wen, and Yongmei Liu.

Multi-agent epistemic explanatory diagnosis via reason- ing about actions. In Francesca Rossi, editor, IJCAI. IJ- CAI/AAAI, 2013.