A Complete Epistemic Planner without the Epistemic Closed World Assumption

1 Introduction

Planning with epistemic goals has received attention from both the dynamic logic and planning communities. Bolander and Andersen [2011] formalized multi-agent epistemic planning based on dynamic epistemic logic [van Ditmarsch et al., 2007] and showed that it is undecidable in general. Further, Aucher and Bolander [2013] showed that multi-agent epistemic planning is undecidable in the presence of only purely epistemic actions. Meanwhile, Yu et al. [2013] identified two important decidable fragments of multi-agent epistemic planning. Recently, Kominis and Geffner [2015], and Muise et al. [2015] showed how to exploit classical planning to solve restricted versions of multi-agent epistemic planning problems.

There are earlier works on single-agent epistemic planning. Herzig et al. [2003] proposed a framework for epistemic planning where knowledge bases (KBs) are expressed as positive epistemic formulas, and showed how progression, regression and plan generation can be achieved in their framework. Bienvenu et al. [2010] identified two normal forms of epistemic formulas called S5-CNFCNF,DNF and S5-DNFDNF,CNF, and showed that progression is tractable when the KB is in S5-DNFDNF,CNF, and entailment is tractable when the KB is in S5-DNFDNF,CNF and the query is in S5-CNFCNF,DNF. However, the above works are only theoretical studies. Petrick and Bacchus [2002; 2004] presented a first-order epistemic planning system PKS based on the idea of progression. The kinds of knowledge they consider include literal knowledge, knowing-whether knowledge, and exclusive-or knowledge. However, their progression and reasoning algorithms are both incomplete, and hence their planner is incomplete.

∗Corresponding author

In the single-agent case, under the epistemic closed-world assumption (ECWA) [Herzig et al., 2003], that is, if I cannot prove that I know ϕ, then I don't know ϕ, epistemic planning can be reduced to contingent planning [Peot and Smith, 1992]. Bertoli et al. [2006] used binary decision diagrams [Bryant, 1986] to represent knowledge bases and proposed a planner MBP based on symbolic model checking. To et al. [2011] used minimal DNF formulas to represent knowledge bases, and proposed an algorithm PrAO with pruning techniques used in AND/OR forward search to solve contingent planning problems.

However, in some epistemic planning scenarios, it is inappropriate to make the ECWA. To illustrate this, consider the following modified wolf-sheep-cabbage example. Every Monday, a farmer has to take at least two objects of a wolf, a sheep and a basket of cabbages to cross a river. The wolf will eat the sheep, and the sheep will eat the cabbages, if the farmer is not with them. What is a plan for the farmer to cross the river? The initial knowledge base of the planning problem can be represented as K(wi∧si)∨K(si∧ci)∨K(wi∧ci), where wi denotes that a wolf is on the left bank of the river initially. Also, si and ci are similar. Although the initial KB does not entail any of Kwi, Ksi, and Kci, we cannot draw the conclusions ¬Kwi, ¬Ksi, and ¬Kci.

In general, the following are some scenarios where it is inappropriate to make the ECWA. Firstly, the agent is not fully introspective; hence the agent is not able to infer what she does not know from an explicit representation of what she knows. Secondly, the agent wants to devise a generic plan that can be used for a wide range of situations. Thirdly, the agent is doing planning for the purpose of intention recognition; hence the agent is not sure about the observed agent's mental state and can only make reasonable assumptions about what the observed agent knows and does not know.

In this paper, we propose a complete single-agent epistemic planner without the epistemic closed-world assumption. We begin with a theoretical formulation of single-agent epistemic planning without the ECWA. Then we identify two normal forms of epistemic formulas: weak minimal epistemic DNF, in short WM-EDNF, and weak minimal epistemic CNF, in short WM-ECNF. We present the progression and entailment algorithms based on the above representations, and show that the entailment algorithm is tractable when the KB is in WM-EDNF and the query is in WM-ECNF. Next we adapt the PrAO algorithm [To et al., 2011] as the main planning algorithm and develop a complete epistemic planner called EPK. Our experimental results show that EPK can generate solutions effectively for most of the epistemic planning problems we have considered including those without the ECWA.

2 Preliminaries

In this section, we first introduce propositional logic and two notions: minimal DNF/CNF and strong entailment. Then, we extend the above notions to epistemic logic, and identify two forms of epistemic formulas: WM-EDNF which represents the KBs and WM-ECNF which represents the preconditions of actions and the goals of problems. Finally, we give the definitions of ontic actions and sensing actions, and the modeltheoretic definition of progression wrt actions.

2.1 Propositional logic

Throughout this paper, we fix X = {x1, · · · , xn} be a finite set of propositions. The propositional language Lprop is generated from X, the usual connectives and two boolean constants ⊤ and ⊥. A state is a subset of X, e.g., {x1, x2} is a state where both x1 and x2 hold and other propositions do not. A literal is either a proposition x or its negation ¬x. l denotes the complement of a literal l. For a set of literals L, L = {l | l ∈ L}. We call ϕ a term (resp. clause) if it is in the form of ∧i li (resp. ∨i li) where every li is a literal. Term (resp. clause) is often represented as a set of literals. So the union of two terms and the difference of two terms can be considered as terms. For example, suppose that t1 = x1∧¬x2 and t2 = ¬x2 ∧ x3. Then t1 ∪ t2 = x1 ∧ ¬x2 ∧ x3 and t1 \ t2 = x1. A DNF (resp. CNF) φ is form of ∨i ψi (resp. ∧i ψi) where every ψi is a term (resp. clause).

Definition 2.1 (Minimal DNF/CNF) A DNF (resp. CNF) φ whose form is ∨iψi (resp. ∧iψi) is minimal if for any two distinct terms (resp. clauses) ψi and ψj, ψi ̸|= ψj and ψj ̸|= ψi .

Obviously, we can transform a DNF (resp. CNF) φ to an equivalent minimal one, denoted by min(φ), by removing the redundant terms (resp. clauses).

Definition 2.2 Let φ and φ′ be two DNFs where φ = ∨i ψi and φ′ = ∨j ψ′j . We say that φ strongly entails φ′ , denoted by φ ↦→φ′ , if for all ψi, there exists ψ′j s.t. ψi |= ψ′j .

Proposition 2.1 Let φ and φ′ be two DNFs. If φ ↦→ φ′ , then φ |= φ′ .

The above proposition says that if φ strongly entails φ′ , then φ entails φ′ , but not vice versa. For example, let φ = a ∨ ¬a and φ′ = b ∨ ¬b. Since φ ≡ φ′ ≡ ⊤, we get that φ |= φ′ . But φ ̸↦→ φ′ because a ̸|= b and a ̸|= ¬b. Similarly, we can extend the concept to CNFs.

Definition 2.3 Let φ and φ′ be two CNFs where φ = ∧i ψi and φ′ = ∧j ψ′j . We say that φ strongly entails φ′ , denoted by φ ↦→φ′ , if for all ψ′j , there exists ψi s.t. ψi |= ψ′j .

Proposition 2.2 Let φ and φ′ be two CNFs. If φ ↦→ φ′ , then φ |= φ′ .

2.2 Epistemic logic

Objective facts can be represented as propositional formulas. In epistemic planning, we model what the agent knows about the current state, which is an subjective formula, in epistemic logic. We will illustrate the syntax and semantics of epistemic logic LK as follows.

Definition 2.4 The language of epistemic logic LK is defined as follows using BNF notation:

For distinguishing two kinds of formulas, we use capital letters to denote the epistemic formulas, i.e., Φ, Ψ etc. The propositional formulas are denoted by lowercase letter, i.e., φ, ψ etc.

Definition 2.5 (Epistemic state) An epistemic state, in short e-state, is a finite non-empty set of states.

Intuitively, the agent considers every state in an epistemic state is possible.

Definition 2.6 Let M be an e-state. We interpret formulas in LK as follows:

• for φ ∈ Lprop , M |= Kφ if for every s ∈ M, s |= φ;
• M |= Φ ∧ Ψ if M |= Φ and M |= Ψ;
• M |= ¬Φ if M ̸|= Φ.

We let Mod(Φ) = {M ⊆ 2X | M ̸= ∅ andM |= Φ}, which is the set of e-states satisfying Φ. We remark that Mod(⊥) ≡ ∅ since there are no e-states satisfying ⊥.

Let Φ be an epistemic formula. We say that Φ is an epistemic literal if it is in the form of Kφ or ˆKφ where φ ∈ Lprop. We also say that Φ is an epistemic term (resp. clause) if it is in the formof Kψ∧∧i ˆKηi (resp. ˆKψ∨∨i Kηi). Throughout this paper, we require ψ and all ηi's are DNF (resp. CNF) for an epistemic term (resp. clause).

Definition 2.7 (Epistemic DNF/CNF) An epistemic formula Φ is an epistemic DNF (resp. CNF), in short EDNF (resp. ECNF) is in the form of ∨i Ψi (resp. ∧i Ψi) where Ψi is an epistemic term (resp. clause).

Definition 2.8 (Separable)

• An epistemic termKψ ∧ ∧i ˆKηi is separable if ηi |= ψ for each i.

• An epistemic clause ˆKψ∨∨i Kηi is separable if ψ |= ηi for each i.
• An EDNF ∨i Ψi is separable if every Ψi is separable.
• An ECNF ∧i Ψi is separable if every Ψi is separable.

We can transform an epistemic formula to an equivalent separable one. For example, Kψ ∧ ∧i ˆKηi is equivalent to Kψ ∧ ∧i ˆK(ψ ∧ ηi). The latter is separable.

Definition 2.9 (Strong entailment) Let Φ and Φ′ be two separable epistemic terms where Φ = Kψ ∧ ∧i ˆKηi and Φ′ = Kψ′ ∧ ∧j ˆKη′j . We say that Φ strongly entails Φ′ , denoted by Φ ↦→ Φ′ if ψ ↦→ ψ′ and for all η′j , either ψ ↦→ η′j or there exists ηi s.t. ηi ↦→ η′j .

Similar to propositional logic, we can get the following proposition.

Proposition 2.3 Let Φ and Φ′ be two separable EDNFs. If Φ ↦→ Φ′ , then Φ |= Φ′ .

Now, we can define weak minimal EDNFs.

Definition 2.10 (Weak minimal EDNF) A separable EDNF Φ whose form is ∨i Ψi is weak minimal if for any two distinct epistemic terms Ψi and Ψj, Ψi ̸↦→Ψj and Ψj ̸↦→Ψi.

For space limitations, we omit a similar notion weak minimal ECNF. We use wmin(Φ) to denote the weak minimal of Φ.

Proposition 2.4 Every epistemic formula can be transformed to a WM-EDNF (resp. WM-ECNF) equivalently.

2.3 Actions and Progression

In this paper, we extend the preconditions of actions so as to be represented as epistemic formulas.

A conditional effect is a pair 〈con, lit〉 where con and lit are sets of literals. Intuitively, it means that literals in lit, both positive and negative, become true if a certain action is executed when con holds. The definitions of ontic actions and sensing actions are as follows.

Definition 2.11 (Ontic action) An ontic action ao is a pair 〈pre, eff〉, where

• pre: an epistemic formula, which specifies precondition;
• eff: a set of conditional effects.

Throughout this paper, we require the preconditions of actions including sensing actions to be WM-ECNFs. Given a state s and an ontic action ao, the positive effect pe(ao, s) of executing ao in s is defined as

The negative effect, denoted by ne(ao, s), is similar. The new state resulting from s by executing ao, denoted by s⊛ao, is s \ ne(ao, s) ∪ pe(ao, s). We also require that ontic actions are not self-contradictory. For an ontic action ao, there do not exist a proposition x, a state s and two conditional effects e, e′ ∈ eff(ao) such that the following hold: (1) x ∈ lit(e); (2) ¬x ∈ lit(e′ ); (3) s |= con(e); and (4) s |= con(e′ ).

We say an action a is applicable in an e-state M iff M |= pre(a). We say a is executable in Φ iff a is applicable in every e-state of Φ. On performing ao in M, the new e-state M ⊗ao is {s ⊛ao | s ∈M}.

Definition 2.12 (Progression wrt ontic actions) Let Φ ∈ LK, ao be an ontic action executable in Φ. Then Φ′ , denoted by prog(Φ, ao), is a progression of Φ for ao if

We give the definition of sensing actions below.

Definition 2.13 (Sensing action) A sensing action as is a pair 〈pre, res〉 , where

• pre: an epistemic formula, which specifies precondition;
• res: a formula in Lprop, which is the sensing result.

After executing a sensing action as, the agent will know whether res(as) holds. The applicability and executability of sensing actions are similar to those of ontic actions. Given an e-state M and a propositional formula φ, the new epistemic state M ⊘ φ is {s ∈ M | s |= φ}, i.e., the set of states of M satisfying φ.

Definition 2.14 (Progression wrt sensing actions) Let Φ be an epistemic formula, as a sensing action executable in Φ. Then a pair (Φ+,Φ-), denoted by prog(Φ, as), is a progression of Φ for as where

• Mod(Φ+) = {M ⊘ res(as) | M ∈ Mod(Φ)} \ {∅};
• Mod(Φ-) = {M ⊘ ¬res(as) | M ∈ Mod(Φ)} \ {∅}.

3 Epistemic planning

In this section, we introduce the definitions of epistemic planning problem and its solution.

Definition 3.1 (Epistemic planning problem) An epistemic planning problem P is a tuple 〈O, S, I, G〉, where

• O: a set of ontic actions;
• S: a set of sensing actions;
• I: an epistemic formula specifying the initial KB;
• G: an epistemic formula specifying the goal formula.

O and S are separate, i.e., O ∩ S = ∅.

Throughout this paper, we require I to be a WM-EDNF and G to be a WM-ECNF.

Example 1 We now formalize the example from the introduction as follows. Here, we only give several ontic actions about that the farmer moving from the right bank to the left bank. The other ontic actions are similar. We let sa denote that the sheep is alive, ce denote that the cabbages are not eaten, d denote that the boat can load two objects (excluding the farmer), and fl, wl, sl and cl denote that the farmer, the wolf, the sheep or the cabbages are on the left bank of the river respectively.

1. left: the farmer moves to the left bank without taking anything.
2. pre(left) ≡ K¬fl
3. eff(left) = {〈∅, {¬fl}〉,

〈{wi, si, sa, ¬wl, ¬sl}, {¬sa}〉,

〈{si, sa, ci, ce, sl, cl}, {¬ce}〉,

〈{si, sa, ci, ce, ¬sl, ¬cl}, {¬ce}〉}

1. wLeft: the farmer tries to take the wolf to the left bank.

• pre(wLeft) ≡ K(¬fl ∧¬d)

Intuitively, the farmer will move alone if the wolf is on the left bank or there does not exist a wolf initially.

1. wsLeft: the farmer tries to take the wolf and the sheep to the left bank.
2. pre(wsLeft) ≡ K(¬fl ∧ d)
3. eff(wsLeft) = {〈∅, {fl}〉, 〈{wi, ¬wl}, {wl}〉, 〈{si, sa, ¬sl}, {sl}〉}

Similar to wLeft, the farmer will take the wolf (resp. the sheep) if it is on the right bank.

1. senseD: the farmer inquires whether the boat can load two objects.
2. pre(senseD) ≡ K⊤
3. res(senseD) ≡ d
4. I = (K(ci∧si)∨K(wi∧si)∨(ci∧si))∧K(fl∧(ci → ce ∧ cl) ∧ (si → sa ∧ sl) ∧ (wi → wl)) ∧ ˆKd ∧ ˆK¬d.
5. G = K((ci → ce ∧ ¬cl) ∧ (si → sa ∧ ¬sl) ∧ (wi → ¬wl)).

We formalize the notion of conditional plans through action trees as follows.

Definition 3.2 (Action tree) Let P be an epistemic planning problem where P = 〈O, S, I, G〉. An action tree T is defined inductively as follows:

• ϵ: the empty tree
• ao; T ′ , where ao ∈ O, and T ′ is an action tree
• as; (T +|T -), where as ∈ S and T + and T - are action trees.

Let us denote undefined by undef. Now, we define the progression wrt action trees.

Definition 3.3 (Progression wrt action trees) Let Φ be an epistemic formula, and T an action tree. The progression of Φ wrt T , denoted by prog(Φ, T ), is defined inductively as follows:

• prog(Φ, ϵ) = {Φ}, if Φ ̸≡ ⊥;
• prog(Φ, ϵ) = undef, otherwise;
• prog(Φ, ao; T ′ ) = {prog(prog(Φ, ao), T ′ )}, if Φ |= pre(ao) and Φ ̸≡ ⊥;
• prog(Φ, ao; T ′ ) = undef, otherwise;
• prog(Φ, as;(T +|T -))=prog(Φ+, T +)∪prog(Φ-, T -), if Φ |= pre(as) and Φ ̸|= Kres(as) and Φ ̸|= K¬res(as) and Φ ̸≡ ⊥;
• prog(Φ, as; (T +|T -)) = undef , otherwise.

We define solutions to epistemic planning problems below, which are typically action trees.

Definition 3.4 (Epistemic planning solution) Let P be an epistemic planning problem where P = 〈O, S, I, G〉. An action tree T is a solution to P if T is finite, prog(I, T ) is defined, and for every epistemic formulas Φ of prog(I, T ), Φ entails the goal formula G.

Example 2 (Example 1 continued) The action tree, depicted in Figure 1, is a solution to this example. It states as follows. Firstly, the farmer senses whether a boat can load two objects. If the boat can load two objects, then the farmer will try to take the sheep and the cabbages to cross the river. Because the cabbages are eaten by the sheep if the farmer is not around, he tries to take the cabbages back to the left bank. Finally, he tries to take the wolf and the cabbages to the right bank. Otherwise, the farmer should obey the "eat rule", and has to take only one object to cross the river until all the objects are on the right bank of the river.

4 Progression and Reasoning

In this section, we introduce three core parts of EPK: (1) progression wrt ontic actions and sensing actions; (2) determining whether a KB entails the precondition of an action; (3) checking whether two KBs are strongly equivalent.

4.1 Progression

To update KBs according to the effects of ontic actions, we firstly transform a DNF φ to an equivalent one φ′ such that for every conditional effect and every term of φ′ , either the term entails the condition con of the conditional effect, or it entails ¬con.

Definition 4.1 Let t and t′ be two terms. The extension of t wrt t′ , denoted by ext(t, t′ ), is defined as

Intuitively, we keep t if it entails t′ or it entails the negation of t′ . Otherwise, we transform t to a DNF ext(t, t′ ) such that for each term of ext(t, t′ ), either it entails t′ or it entails the negation of t′ .

Proposition 4.1 Let t and t′ be two terms, and φ = min(ext(t, t′ )). Then φ ≡ t and for every term t∗ of φ, either t∗ |= t′ or t∗ |= ¬t′ holds.

For a DNF φ = ∨i ti, we can define a similar operation: ext(φ, t′ ) = min(∨i ext(ti, t′ )).

Definition 4.2 Let ao an ontic action. We say a term t is enabling for ao if for every conditional effect 〈con, lit〉 ∈ eff(ao), either t |=con or t |=¬con holds. We say a DNF φ is enabling for ao if every term t of φ is enabling for ao.

Proposition 4.2 Let φ be a DNF, ao an ontic action where eff(ao)={〈coni, liti〉}ki=1 , and φ′ =ext((ext(φ′ , con1),· · ·), conk). Then φ′ ≡ φ and φ′ is enabling for ao.

The above proposition shows how to transform a DNF to an equivalent one enabling for ontic actions.

Definition 4.3 Let t be a term, ao an ontic action which t is enabling for. The effect of ao in t, denoted by e(t, ao), is {l | ∃〈con, lit〉 ∈ eff(ao).t |= con and l ∈ lit}.

Definition 4.4 Let ao be an ontic action, and φ a DNF en-

abling for ao. The update of φ wrt ao, denoted by update(φ, ao), is min(∨t∈φ (t \ e(t, ao) ∪ e(t, ao))).

The above proposition tells us how to update a DNF according to the effect of an ontic actions. We are now ready to give the computation of the progression wrt ontic actions.

Proposition 4.3 Let Ψ = Kψ ∧ ∧i ˆKηi be a separate epistemic term, and ao an ontic action executable in Ψ, and Ψ′ = Kψ′ ∧ ∧i ˆKη′i where ψ′ = update(ψ, ao) and η′i = update(ηi, ao) for each i. Ψ′ is a progression of Ψ wrt ao.

Proposition 4.4 Let Φ = ∨i Ψi be a separable EDNF, and ao an ontic action executable in Φ. Then prog(Φ, ao) ≡ ∨i prog(Ψi, ao).

Even if Φ is a WM-EDNF, the progressed KB prog(Φ, ao) may not be a WM-EDNF. But we can transform it to an equivalent WM-EDNF.

Next, we introduce the progression of separable epistemic terms wrt observation.

Definition 4.5 Let Ψ = Kψ∧∧i ˆKηi be a separate epistemic term, and φ ∈ Lprop. The update of Ψ wrt φ, denoted by obs(Ψ, φ), is K(ψ ∧ φ) ∧ ∧ηi|=φ ˆKηi.

After observing φ, an agent remains her knowledge of ψ and keeps considering ηi possible if ηi |= φ. The latter is counterintuitive, but it is valid. This is because the possible state satisfying ηi may not satisfy φ when we do not make the ECWA.

Proposition 4.5 Let Φ = ∨i Ψi be an EDNF, and as a sensing action executable in Φ. A pair (Φ+,Φ-) is a progression of Φ wrt as where Φ+ ≡ ∨i obs(Ψi, res(as)) and Φ- ≡ ∨i obs(Ψi, ¬res(as)).

By Proposition 4.5, we can implement progression wrt sensing actions. Similarly, we transform Φ+ (resp. Φ-) to a WM-EDNF when it is not a WM-EDNF.

4.2 Reasoning

Firstly, we introduce a simple property of propositional logic.

Proposition 4.6 Let φ = ∨i ψi be a DNF and φ′ = ∧j ψ′j a CNF. Then φ |= φ′ iff for every i, j, we have ψi |= ψ′j .

Proposition 4.7 Let Ψ be a separable epistemic term whose form is Kψ ∧ ∧i ˆKηi and Ψ′ a separable epistemic clause whose form is ˆKψ′ ∨ ∨j Kη′j . Ψ |= Ψ′ iff one of the following conditions holds

1. ψ ∧¬ψ′ is inconsistent;
2. there exists i s.t. ¬ψ′ ∧ ηi is inconsistent;
3. there exists j s.t. ψ ∧¬η′j is inconsistent.

Proposition 4.8 Let Φ = ∨i Ψi be an EDNF and Φ′ = ∧j Ψj an ECNF. Φ |= Φ′ iff for every i, j, Ψi |= Ψj.

By Proposition 4.8, we can determine whether an action is executable in the current KB in polynomial time.

Theorem 4.1 Let Φ be an EDNF and Ψ be an ECNF. Deciding whether Φ |= Ψ is tractable.

Next, we show how to judge the equivalence of two KBs.

Definition 4.6 (Strong equivalence) Let Φ = ∨i Ψi and Φ′ = ∨j Ψ′j be two WM-EDNFs. We say Φ ∼= Φ′ if the following two conditions all hold:

1. for every i, there exists j s.t. Ψi ↦→Ψ′j ;
2. for every j, there exists i s.t. Ψ′j ↦→Ψi.

Proposition 4.9 Let Φ and Φ′ be two WM-EDNFs. If Φ ∼= Φ′ , then Φ ≡ Φ′ .

By Proposition 4.9, we can determine whether two WMENDFs are strongly equivalent. Here, we only give a sufficient condition, but not a sufficient and necessary condition. So, sometimes, twoWM-ENDFs are equivalent, but not strongly equivalent.

5 Planning Algorithm

In this section, we briefly describe PrAO algorithm [To et al., 2011], which is the main planning algorithm of EPK. The algorithm is based on progression and entailment which have been introduced in the last section.

A node n in a search graph is a knowledge base Φn with a state state(n) including four tags: goal, dead, unexplored, explored and an additional tag: connected. As depicted in Algorithm 1, Lines 1 to 5 check whether I entails G, if so, then return the empty plan; otherwise, initialize the search graph. Lines 6 to 15 construct the search graph until it finds a solution or guarantees that there are no solutions. Lines 7 to 10 select an unexplored and connected node n in N for exploration. If no such node exists then return no solution. Line 11 expands the selected node and updates the graph accordingly. Lines 12 to 15 check the state of the initial node. If its state is goal, return BuildPlan(N, T , n0) to generate a solution; if dead, return no solution. Otherwise, continue the loop.

For space limitations, we briefly introduce subroutine Explore and the heuristic function used in Algorithm 1.

Algorithm 1: P lan(O, S, I, G) Input : An epistemic problemP = 〈O, S, I, G〉 Output: A solution if it guarantees goal achievement or NULL otherwise. 1 if I |= G then 2 return an empty plan ϵ 3 else 4 Let n0 = I, state(n0) = unexplored, 5 connected(n0) = true, T = ∅ and N = {n0} 6 while true do 7 if {n ∈ N | state(n) = unexplored and 8 connected(n) = true} = ∅ then 9 return NULL 10 Let n be the unexplored and connected node with a heuristic function in N 11 Explore(n) 12 if state(n0) = goal then 13 return BuildP lan(N , T , n0) 14 if state(n0) = dead then 15 return NULL

Explore(n) can generate the children of n for actions executable in Φn with loop detection. The application of an ontic action starting from n results in a new node, while applying sensing actions produces two new nodes, i.e., n is split amongst the observations. It is a simple idea that the design of heuristic function for choosing nodes in N to explore. For each epistemic clause of goal in WM-ECNF, we count how many epistemic term which can entail that epistemic clause in current KB, and sum them up. Then we can get the heuristic value of current node via dividing total times by the number of epistemic clause of goal.

Finally, we have the following theorem stating that Algorithm 1 is sound and complete.

Theorem 5.1 Let P = 〈O, S, I, G〉 be an epistemic planning problem, and Ts an action tree constructed by the P lan(O, S, I, G). We have:

1. If Ts is NULL, then P has no solution; otherwise, Ts is a solution tree for P, and P has a solution;
2. If P has a solution, then Ts is a solution tree for P; otherwise, Ts is NULL.

6 Implementation and Experiments

Our planner EPK is implemented in C++, and our experiments were done on a PC with Intel i7-4700MQ (2.4GHz) CPU and 4GB RAM on Linux. 1 Results are in the form of t(d/s), where t, d and s denote the overall execution time, the depth of the solution tree and the number of nodes in the solution respectively. Usually, d and s are criteria for evaluation of the quality of a solution. "-" denotes out-of-memory or time-out (20 minutes limit). Heuristic, BFS, DFS and IDS stand for search with heuristic function, breadth-first search, depth-first search, and iterative-deepening search respectively.

1 .http://ss.sysu.edu.cn/%7ewh/epk.html

We experimentally compare EPK with PKS, and use a testbed of five domains, including two domains taken from PKS, other domains taken from contingent planning. Some domains in PKS contain functions and numerical representation, which EPK can not handle. Two domains in PKS are as follows: btc and unix series. In addition, other domains, doors, push and dispose are from classical contingent planning benchmarks.

Table 1 reports the comparative experimental results. We can observe that, generally speaking, our planner EPK are better than PKS in the performance except btc. In detail, the heuristic function is not suitable for these domains, since this search method is slower than BFS and DFS in EPK. For domains btc, unix series, PKS is faster than EPK, while the quality of epistemic planning solutions of EPK are better than PKS using BFS or DFS. For domains such as push, doors, dispose series, EPK is faster than PKS using BFS and PKS even can not solve push and doors series using DFS.

Table 2 shows that domains without the ECWA. Although heuristic search in domains such as block, farmer, medpks2 and medpks-3 is slower than BFS and DFS, it is obvious that heuristic function is very important especially for cube series and ebtcs-2-5.

7 Conclusions

We have introduced a general and effective approach to single-agent epistemic planning with deterministic actions without making the ECWA. We identify two compact representations: WM-EDNF and WM-ECNF. Based on the representations, we give the progression and entailment algorithms which are core modules in planning. Moreover, entailment is tractable when the KB is in WM-EDNF and the query is in WM-ECNF. We adapt the PrAO algorithm as the main planning algorithm, and our planner is complete. Our empirical evaluation shows that our planner is better than PKS in most of the epistemic planning problems we have tested. Also, EPK generates solutions effectively for most of the epistemic planning problems we have considered, especially those without the ECWA.

There are several possible directions for future study. Firstly, we want to improve the efficiency of our planner via designing a compact yet efficient and scalable representation and developing better heuristic functions, such as graph heuristics. Secondly, we want to extend the definition of ontic actions so that conditional effects can contain not only propositional literals but also epistemic literals, and give the semantics for these actions. Thirdly, we would also like to extend this work to multi-agent cases.

8 Acknowledgments

The authors would like to thank Andreas Herzig for his useful suggestions. Hai Wan thanks Guangzhou Science and Technology Project (No. 2013J4100058) for the support of this research. Liangda Fang and Yongmei Liu acknowledge the support of the National Natural Science Foundation of China under grant No. 61073053.