A General Multi-agent Epistemic Planner Based on Higher-order Belief Change

1 Introduction

Many intelligent tasks involve the interaction of multiple agents, raising the need of reasoning about knowledge and beliefs, and their change. For illustration, consider the following example from [Kominis and Geffner, 2015]. There is a corridor of several rooms, and a number of boxes that are in some of the rooms. Two agents can move along this corridor. The task is for the two agents to collaborate via communication in finding out the positions of the boxes. Performance of actions results in the change of not only the world but also agents' knowledge and beliefs. In some cases, it is even necessary to reason about higher-order knowledge and beliefs, i.e., knowledge and beliefs about other agents' knowledge and beliefs. For example, agent a may wish to know a secret s with agent b knowing she knows s, or without b knowing she knows s, or even with b believing she does not know s.

In recent years, multi-agent epistemic planning has received attention from both dynamic logic and planning communities. On the theory side, Bolander and Andersen [2011] formalized multi-agent epistemic planning based on dynamic epistemic logic (DEL) [van Ditmarsch et al., 2007] and showed that it is undecidable in general. In the DEL-based formalization, states are represented as Kripke models, and actions are represented as action models, which are Kripke models of actions, describing agents' abilities to distinguish among actions. 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. On the implementation side, 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. By resorting to classical planning, both methods can only generate linear plans, doing conformant planning. Moreover, Kominis and Geffner assumed all actions are public, and hence dealt with knowledge. In contrast, Muise et al. focused on beliefs; however, they can only handle bounded-depth belief literals, disallowing disjunctive beliefs. In the single-agent case, Wan et al. [2015] presented a complete epistemic planner without the epistemic closed world assumption. They proposed normal forms for epistemic formulas which support tractable reasoning and progression, and adapted the PrAO algorithm for contingent planning [To et al., 2011].

Belief change studies how an agent modifies her beliefs on receiving new information. Two main types of belief change are revision and update: revision concerns belief change about static environments due to partial and possibly incorrect information, whereas update concerns belief change about dynamic environments due to the performance of actions. Various guidelines for belief change have been proposed, and the most popular ones are the AGM postulates for belief revision [Alchourr´on et al., 1985], the KM postulates for belief update [Katsuno and Mendelzon, 1991], and the DP postulates for iterated belief revision [Darwiche and Pearl, 1997]. Katsuno and Mendelzon [1991] briefly discussed how belief revision and update can be used for reasoning about actions: if a condition φ is found true, the KB is revised with φ; if an action with postcondition ψ is performed, the KB is updated with ψ. There has been work extending belief change from propositional logic to epistemic logic. Aucher [2010] generalized the AGM postulates to multi-agent settings. Also, Aucher [2011] explored the progression of KBs wrt actions, where both KBs and actions are represented as canonical formulas in modal logics, which capture Kripke models up to certain depths [Moss, 2007]. Recently, Caridroit et al. [2016] investigated several measures of distances between KD45n Kripke models, and use them to define the revision of beliefs represented by such models. Finally, Miller and Muise [2016] studied belief update for KBs consisting of belief literals.

In this paper, we consider multi-agent epistemic planning from the viewpoint of a third person. We treat contingent rather than conformant planning, resulting in nonlinear plans. We model private actions and hence handle beliefs, formalized with the multi-agent modal logic KD45n [Fagin et al., 1995]. We do not support arbitrary common knowledge, but we handle static propositional common knowledge, which we call constraints. For such planning settings, we propose a general representation framework where the initial KB and the goal, the preconditions and effects of actions can be arbitrary KD45n formulas, progression of KBs wrt actions is achieved through the operation of belief revision or update, and the solution is an action tree branching on sensing results. To support efficient reasoning and progression, we make use of a normal form for KD45n called alternating cover disjunctive formulas (ACDFs) [Hales et al., 2012]. We propose basic revision and update algorithms for ACDF formulas. Based on our reasoning, revision and update algorithms, adapting the PrAO algorithm, we implemented a multi-agent epistemic planner called MEPK. Our experimental results show the viability of our approach.

2 Preliminaries

In this section, we introduce the background work of our paper, i.e., the multi-agent modal logic KD45n, alternating cover disjunctive formulas, and belief revision and update.

2.1 Multi-agent Modal Logic KD45n

Consider a finite set of agents A and a finite set of atoms P. We use φ and ψ for formulas, Φ and Ψ for sets of formulas.

Definition 2.1 The language LKC of multi-agent modal logic with common knowledge is generated by the BNF:

p∈P, a∈A, φ, ψ∈LKC. We use LK for the language without the C operator, and L0 for the propositional language.

Intuitively, Cφ means commonly knowing φ. In this paper, we restrict our attention to the case of propositional common knowledge, i.e., Cφ where φ ∈ L0, and we call φ a constraint. We use C ∗φ to denote φ ∧ Cφ.

We let Laφ stand for ¬Ka¬φ. We let ⊤ and ⊥ represent true and false respectively. We let ∨ Φ (resp. ∧ Φ) denote the disjunction (resp. conjunction) of members of Φ; and we use LaΦ to represent the conjunction of Laφ where φ ∈ Φ. The modal depth of a formula φ in LK is the depth of nesting of modal operators in φ.

Definition 2.2 A frame is a pair (W,R), where W is a nonempty set of possible worlds; for each agent a ∈ A, Ra is a binary relation on W, called the accessibility relation for a.

We say Ra is serial if for any w ∈ W, there is w′ ∈ W s.t. wRaw′ ; we say Ra is Euclidean if whenever wRaw1 and wRaw2, we get w1Raw2. A KD45n frame is a frame whose accessibility relations are serial, transitive and Euclidean.

Definition 2.3 A Kripke model is a triple M = (W, R, V ), where (W,R) is a frame, and V is a valuation map, which maps each w ∈ W to a subset of P. A pointed Kripke model is a pair s = (M, w), where M is a Kripke model and w is a world of M, called the actual world.

Definition 2.4 Let s = (M,w) be a Kripke model where M =(W, R, V ). We interpret formulas in LKC by induction:

• M, w |= p iff p ∈ V (w);
• M, w |= ¬φ iff M, w ⊭ φ;
• M, w |= φ ∧ ψ iff M, w |= φ and M, w |= ψ;
• M, w |= Kaψ iff for all v s.t. wRav, M, v |= φ;
• M,w |= Cφ iff for all v s.t. wRAv, M, v |= φ, where RA is the transitive closure of the union of Ra for a ∈ A.

We say φ is satisfiable if there is a KD45n model (M,w) s.t. M, w |= φ. We say φ entails ψ, written φ |= ψ, if for any model (M, w), M, w |= φ implies M, w |= ψ. We say φ and ψ are equivalent, written φ ⇔ ψ, if φ |= ψ and ψ |= φ.

We say that φ is satisfiable wrt constraint γ ∈ L0 if φ∧C ∗γ is satisfiable; we say that φ entails ψ wrt constraint γ, written φ |=γ ψ, if φ ∧C ∗γ |= ψ ∧C ∗γ.

2.2 Alternating Cover Disjunctive Formulas

Janin and Walukiewicz [1995] introduced the notion of disjunctive formulas for modal µ-calculus and showed that every formula is equivalent to a disjunctive formula. D'Agostino and Lenzi [2006] gave the definition of disjunctive formulas for modal logics, using a cover modality. Ten Cate et al. [2006] showed that every formula in the multi-agent modal logic Kn is equivalent to a disjunctive formula whose length is at most singly exponential in the length of the original formula. We slightly vary the definition, and use the name cover disjunctive formulas.

Definition 2.5 Let a ∈ A, and Φ a set of formulas. We use ∇aΦ to denote the formula Ka(∨ Φ) ∧ LaΦ.

We use Φ ∧ ψ to denote the set {φ ∧ ψ | φ ∈ Φ}.

Definition 2.7 The set of cover disjunctive formulas (CDFs) is inductively defined as follows:

1. A propositional term, i.e., a conjunction of propositional literals, is a CDF;
2. If φ0 is a propositional CDF, and for each a ∈ B ⊆ A, Φa is a finite set of CDFs, then φ0 ∧ ∧a∈B∇aΦa is a CDF, called a CDF term;

1. If Φ is a non-empty finite set of CDF terms, then ∨ Φ is a CDF, called a disjunctive CDF.

So a propositional CDF is in DNF (disjunctive normal form).

Moss [2007] introduced the concept of canonical formulas, very similar to formulas introduced by Fine [1975], and showed that every formula in Kn is equivalent to a disjunction of a finite set of canonical formulas. However, in the definition of canonical formulas, no disjunction is allowed. As a result, the conversion may cause a non-elementary blowup in size, as compared to a single exponential blowup for CDFs.

We now define a complexity measure ‖ · ‖ for CDFs.

Definition 2.8 The complexity measure ‖ · ‖ for CDFs is inductively defined as follows:

1. ‖t‖= 0, where t is a propositional term;
2. ‖φ0 ∧ ∧a∈B∇aΦa‖= Σa∈B(1+Σφ∈Φa ‖φ‖);
3. ‖ ∨ Φ‖= Σφ∈Φ ‖φ‖.

Hales et al. [2012] introduced the notion of alternating cover disjunctive formulas, and showed that in KD45n, every formula in LK is equivalent to such a formula.

Definition 2.9 We say that a formula has the alternating agent modality property if it has the property that modal operators of an agent do not directly occur inside those of the same agent. We call a CDF with the alternating agent modality property an alternating cover disjunctive formula (ACDF).

For example, ∇a{⊤, q}∧∇b{⊤, ∇a{⊤, ¬q}} is an ACDF, but the CDF ∇a{¬p ∧ q, ∇b{p, q}, ∇a{¬p ∧ q}} is not.

Proposition 2.10 In KD45n, every formula in LK can be transformed to an equivalent ACDF whose length is at most singly exponential in the length of the original formula.

Proof: We first convert the formula into negation normal form, and then we apply the following transformation rules until the formula satisfies the alternating agent modality property: Ka(φ ∧ ψ) ⇔ Kaφ ∧ Kaψ, La(φ ∨ ψ) ⇔ Laφ ∨ Laψ; La(φ ∧ Kaψ) ⇔ Laφ ∧ Kaψ, La(φ ∧ Laψ) ⇔ Laφ ∧ Laψ; Ka(φ∨Kaψ) ⇔ Kaφ∨Kaψ, Ka(φ∨Laψ) ⇔ Kaφ∨Laψ. Now by Lemma 7 of [ten Cate et al., 2006], this formula can be converted to an equivalent CDF with at most a single exponential blowup in size. Since the conversion preserves the alternating agent modality property, the result is an ACDF.

A modal term is a conjunction of propositional formulas and modal atoms of the form Kaφ or Laφ. We call a modal term with the alternating agent modality property an alternating modal term. In the following, we present a result concerning how to check satisfiability of alternating modal terms and its easy corollaries, which will be used later in our paper.

Proposition 2.11 An alternating modal term δ = φ0 ∧ ∧a∈B (Kaφa ∧ LaΨa) is satisfiable wrt constraint γ iff the following hold:

1. φ0 ∧ γ is propositionally satisfiable;
2. for each a ∈ B, φa is satisfiable wrt γ;
3. for each a ∈ B, for each ψ ∈ Ψa, φa ∧ ψ is satisfiable wrt γ.

Proof: The only-if direction is easy; we prove the if direction. Since La⊤ ⇔ ⊤, without loss of generality, we assume that for each a ∈ B, Ψa is not empty. Construct a model (M,w) as follows. By condition 1, create a new world w satisfying φ0 ∧ γ. By condition 3, for each a ∈ B, for each ψ ∈ Ψa, there is a KD45n model (Mψ, wψ) satisfying φa ∧ ψ ∧ C ∗γ, add a new copy of (Mψ,wψ) into M, and let wRawψ; then add a-edges between all the a-children of w. Since δ is an alternating modal term, φa and ψ ∈ Ψa do not use Ka or La as outmost modalities. Also, all worlds of M satisfy γ. Thus M, wψ |= φa ∧ψ ∧C ∗γ. So (M, w) is a KD45n model satisfying δ.

As easy corollaries, we get

Proposition 2.12 Let δ = φ0 ∧ ∧a∈A(Kaφa ∧ LaΨa) and δ′ = φ′0 ∧ ∧a∈A(Kaφ′a ∧ LaΨ′a ) be two alternating modal terms satisfiable wrt constraint γ. Then δ |=γ δ′ iff the following hold:

1. φ0 ∧ γ |= φ′0 propositionally;
2. for each a ∈ A, φa |=γ φ′a ;
3. for each a ∈ A, for every ψ′ ∈ Ψ′a there is a ψ ∈ Ψa s.t. φa ∧ψ |=γ ψ′ .

Proposition 2.13 An ACDF term φ0 ∧ ∧a∈B∇aΦa is satisfiable wrt a DNF γ iff the following hold:

1. φ0 ∧ γ is propositionally satisfiable;
2. for all a ∈ B, Φa is not empty;
3. for all a ∈ B and all φ ∈ Φa, φ is satisfiable wrt γ.

Thus it is tractable to check the satisfiability of ACDFs.

2.3 Belief Revision and Update

We use ◦ to denote a revision operator, and ⋄ an update operator. Let ψ be the original formula, and µ the revision or update formula. To formalize the distinction between revision and update, Katsuno and Mendelzon [1991] presented model-theoretic definitions of them: intuitively, ψ ◦ µ selects from the models of µ those that are closest to models of ψ, while ψ ⋄ µ selects, for each model M of ψ, the set of models of µ that are closest to M. As easy properties of the definitions: when ψ ∧ µ is satisfiable, ψ ◦ µ is equivalent to ψ ∧ µ; update is distributive over the initial formula, i.e., (ψ1∨ψ2)⋄µ is equivalent to (ψ1 ⋄ µ ∨ ψ2 ⋄ µ).

Let's illustrate the difference between revision and update with an example. Take the notion of closeness based on set inclusion, that is, a model I is closer to M than a model J if Diff(I,M) ⊆ Diff(J,M), where Diff(I,M) is the set of atoms where I and M assign different truth values. Then the above model-theoretic definitions give us Satoh's revison operator ◦s [Satoh, 1988] and Winslett's update operator ⋄w [Winslett, 1988]. For example, let ψ = (a ∧ b ∧ c) ∨ (a ∧ ¬b∧¬c), and µ = a∧c. The models of ψ are M1 = {a, b, c} and M2 = {a, ¬b, ¬c}; the models of µ are M1 and M3 = {a, ¬b, c}. Then ψ ◦s µ = a∧b∧c, equivalent to ψ∧µ, since M1 is closet to models of ψ. On the other hand, ψ ⋄w µ = a ∧ c, since M1 is closest toM1, but M3 is closest toM2.

3 Our Modeling Framework

In this section, we present our modeling framework for multiagent epistemic planning (MEP), which is adapted from that for single-agent epistemic planning in [Wan et al., 2015].

We illustrate our framework with the collaboration via communication example from the introduction.

Example 1 There is a corridor of three rooms p1, p2 and p3. Two boxes b1 and b2 are located in some of the rooms. Two agents 1 and 2 can move back and forth along this corridor. When an agent gets into a room, he can see if a box is in the room. An agent can communicate information to another agent. Initially, the two agents are in p2 and the two boxes are not there. The goal is for agent 1 to know the position of b1, and for agent 2 to know the position of b2.

We begin with the definition of MEP problems, then give the definition of different kinds of actions and the associated progression operations, and end with the definition of MEP solutions. The actions we consider include ontic, communication and sensing actions. The first two kinds share the same representation, and we call them deterministic actions.

Definition 3.1 A multi-agent epistemic planning problem Q is a tuple 〈A, P, D, S, I, G, γ〉, where A is a set of agents; P is a set of atoms; D is a set of deterministic actions; S is a set of sensing actions; I ∈ LK is the initial KB; G ∈ LK is the goal; and γ ∈ L0 is the constraint.

The main reason we consider constraints in this paper is for natural modeling of planning domains: we use constraints to express static propositional common knowledge, as will be illustrated in our formalization of Example 1.

We now formalize Example 1.

• The atoms are: at(i, p), meaning agent i is in room p; and in(b, p), meaning box b is in room p.
• The ontic actions are: left(i), agent i moves left; and right(i), i moves right.
• The communication actions are: tell(i, j, b, p), agent i tells j whether b is in p.
• The sensing actions are: find(i, b, p): i sees if b is in p.
• The initial KB is at(1, p2) ∧ at(2, p2) ∧ ¬in(b1, p2) ∧ ¬in(b2, p2)∧K1(at(1, p2)∧¬in(b1, p2)∧¬in(b2, p2))∧ K2(at(2, p2) ∧ ¬in(b1, p2) ∧ ¬in(b2, p2));
• The goal is ∧2i=1 (Kiin(bi, p1) ∨ Kiin(bi, p2) ∨ Kiin(bi, p3)), meaning agent 1 knows the position of box b1, and agent 2 knows the position of box b2.
• The constraint is γ1 ∧ γ2, where γ1 = ∧2i=1 (at(i, p1) ∧ ¬at(i, p2) ∧ ¬at(i, p3) ∨ ¬at(i, p1) ∧ at(i, p2)∧¬at(i, p3)∨¬at(i, p1)∧¬at(i, p2)∧at(i, p3)), meaning each agent is at exactly one room, and γ2 is similar, representing each box is in exactly one room.

The reason that we have in the initial KB at(1, p2) ∧ K1at(1, p2) instead of simply K1at(1, p2) is that we model beliefs rather than knowledge.

Definition 3.2 A deterministic action is a pair 〈pre, eff〉, where pre ∈ LK is the precondition; eff is a set of conditional effects, each of which is a pair 〈con, cef〉, where con, cef ∈ LK indicate the condition and the effect, respectively.

For example, left(i) = 〈pre, {eff1, eff2}〉, where pre = ¬at(i, p1) ∧ Ki¬at(i, p1), eff1 = 〈at(i, p2), at(i, p1) ∧ Kiat(i, p1)〉, and eff2 is similarly defined. For another example, tell(i, j, b, p) = 〈pre, {eff1, eff2}〉, where pre = Kiin(b, p) ∨ Ki¬in(b, p), eff1 = 〈Kiin(b, p), Kj in(b, p)〉, and eff2 = 〈Ki¬in(b, p), Kj¬in(b, p)〉.

Actually, when Kiin(b, p), tell(i, j, b, p) should result in common knowledge of in(b, p) between the two agents. Since we do not support arbitrary common knowledge, we have to approximate common knowledge with higher-order knowledge. For example, we can express the conditional effect with Kjin(b, p) ∧ KiKjin(b, p) ∧ KjKiin(b, p) ∧ KiKjKiin(b, p) ∧ KjKiKj in(b, p).

Definition 3.3 A sensing action is a triple 〈pre, pos, neg〉 of LK formulas, where pre, pos, and neg indicate the precondition, the positive result, and the negative result, respectively.

For the example of find(i, b, p), pre = at(i, p) ∧ Kiat(i, p), pos = in(b, p) ∧ Kiin(b, p), and neg = ¬in(b, p) ∧ Ki¬in(b, p).

An action a is executable wrt a KB φ ∈ LK if φ |=γ pre(a). Suppose a is executable wrt φ. The progression of φ wrt a is defined by resorting to a revision operator ◦γ and an update operator ⋄γ for LK: we use update for deterministic actions and revision for sensing actions.

Definition 3.4 Let φ ∈ LK, and ad a deterministic action where eff(ad) = {〈c1, e1〉, . . . , 〈cn, en〉}. Let ci1 , . . . , cim be all the ci's s.t. φ |=γ ci. Then φ′ , denoted by prog(φ, ad), is a progression of φ wrt ad if φ′ = ((φ ⋄γ ei1 ) . . .) ⋄γ eim .

Definition 3.5 Let φ ∈ LK, and as a sensing action. Then a pair (φ+, φ-), written prog(φ, as), is a progression of φ wrt as if φ+ = φ ◦γ pos(as), and φ- = φ ◦γ neg(as).

A solution of a MEP problem is an action tree branching on sensing results.

Definition 3.6 Let Q be a MEP problem 〈A, P, D, S, I,G,γ〉. The set T of action trees is inductively defined:

1. ϵ is in T , here ϵ represents the empty tree;
2. if ad ∈ D and T ∈ T , then ad; T is in T ;
3. if as ∈ S, T +, T - ∈ T , then as; (T + | T -) is in T .

Definition 3.7 Let φ ∈ LK, T an action tree. The progression of φ wrt T , written prog(φ, T ), is inductively defined:

1. prog(φ, ϵ) = {φ};
2. if φ |=γ pre(ad), prog(φ, ad; T ′ ) = prog(φ′ , T ′ ), where prog(φ, ad) = φ′ ;
3. if φ |=γ pre(as), prog(φ, as; (T +|T -)) = prog(φ+, T +) ∪prog(φ-, T -), where prog(φ, as) = (φ+, φ-);
4. otherwise, prog(φ, T) is undefined.

Definition 3.8 Let Q be a MEP problem 〈A, P, D, S, I,G,γ〉. An action tree T is a solution of Q if prog(I, T) is defined, and for each formula φ in prog(I, T), φ |=γ G.

Figure 1 shows a solution for Example 1. First, Agent 1 moves left. Then she senses if b1 is in p1. If b1 is in p1, agent 2 moves right, and senses if b2 is in p3. If b1 is not in p1, agent 1 senses if b2 is in p1, and tells the result to agent 2.

4 Our Algorithms

In this section, we present our reasoning, belief change, and planning algorithms.

To support efficient reasoning and belief change, we represent KBs as ACDFs, queries as the negation of ACDFs, revision or update formulas as ACDFs, and constraints as DNFs. Thus, for a planning problem, our planner first compiles the initial KB, the effects of conditional effects of deterministic actions, and the positive and negative results of sensing actions into ACDFs, the preconditions of actions, the conditions of conditional effects, and the goal into the negation of ACDFs, and finally the constraint into DNF.

For Example 1, after compilation, we get

• I = at(1, p2) ∧ at(2, p2) ∧¬in(b1, p2) ∧¬in(b2, p2)∧ ∇1{at(1, p2) ∧ ¬in(b1, p2) ∧ ¬in(b2, p2)} ∧ ∇2{at(2, p2) ∧ ¬in(b1, p2) ∧ ¬in(b2, p2)};
• pre(left(i)) = ¬(at(i, p1) ∨∇i{⊤, at(i, p1)});
• cef(eff1(left(i))) = at(i, p1) ∧∇i{at(i, p1)};
• pos(f ind(i, b, p)) = in(b, p) ∧ ∇i{in(b, p)};
• G = ¬∨2i=1∇i{⊤, ¬in(bi, p1),¬in(bi, p2),¬in(bi, p3)};
• γ is a DNF of 34 terms.

4.1 Strong Entailment and Equivalence

Our planner searches through the space of KBs, represented as ACDFs, and performs loop detection during search. Unfortunately, it is not tractable to check the equivalence of two ACDFs. Thus we introduce a stronger notion of equivalence which can be checked in polynomial time.

Definition 4.1 Let φ and φ′ be two ACDFs, γ a DNF. The strong entailment relation φ ↦→γ φ′ is recursively defined:

1. For propositional terms φ and φ′ , φ ↦→γ φ′ if φ∧γ |= φ′ .
2. When φ = φ0∧∧a∈A∇aΦa and φ′ = φ′0 ∧∧a∈A∇aΦ′a , φ ↦→γ φ′ if the following hold:
3. (a) φ0 ↦→γ φ′0 ;
4. (b) for each a ∈ A, for each φa ∈ Φa there exists φ′a ∈ Φ′a s.t. φa ↦→γ φ′a ;
5. (c) for each a ∈ A, for each φ′a ∈ Φ′a there exists φa ∈ Φa s.t. φa ↦→γ φ′a .
6. When φ = ∨ Φ and φ′ = ∨ Φ′ , φ ↦→γ φ′ if for all φ ∈ Φ there exists φ′ ∈ Φ′ s.t. φ ↦→γ φ′ .

Clearly, the strong entailment relation can be checked in polynomial time. By Proposition 2.12, it is easy to prove:

Proposition 4.2 Let φ and φ′ be two ACDFs, and γ a DNF. If φ ↦→γ φ′ , then φ |=γ φ′ .

We say that two ACDFs φ and φ′ are strongly equivalent wrt constraint γ if both φ ↦→γ φ′ and φ′ ↦→γ φ.

4.2 Reasoning

As mentioned earlier, to support efficient reasoning, we represent KBs as ACDFs, and queries as the negation of ACDFs. By Propositions 2.6 and 2.13, it is easy to prove

Proposition 4.3 Let φ and φ′ be two ACDFs, γ a DNF.

1. If φ and φ′ are propositional terms, φ |=γ ¬φ′ iff for each term t in γ, φ ∧ t ∧ φ′ has complementary literals.
2. If φ = φ0 ∧ ∧a∈A∇aΦa and φ′ = φ′0 ∧ ∧a∈A∇aΦ′a , then φ |=γ ¬φ′ iff one of the following holds:
3. (a) φ0 |=γ ¬φ′0 ;
4. (b) there exist a ∈ A and φ ∈ Φa s.t. for all φ′ ∈ Φ′a , φ |=γ ¬φ′ ;
5. (c) there exist a ∈ A and φ′ ∈ Φ′a s.t. for all φ ∈ Φa, φ |=γ ¬φ′ .
6. If φ = ∨ Φ and φ′ = ∨ Φ′ , then φ |=γ ¬φ′ iff for all φ ∈ Φ and φ′ ∈ Φ′ , φ |=γ ¬φ′ .

The above proposition gives us a recursive algorithm for deciding if φ |=γ ¬φ′ , or equivalently, if φ ∧ φ′ is satisfiable wrt γ. Clearly, the algorithm has polynomial complexity.

For Example 1, to check if I |=γ pre(left(1)), by Rule 3, we check if both I |=γ ¬at(1, p1) and I |=γ ¬∇1{⊤, at(1, p1)} hold. By Rule 1, the former holds. By Rule 2.a, the latter holds, since at(1, p2) |=γ ¬at(1, p1).

4.3 Higher-order Belief Change

The basic idea behind our belief change operators is to reduce change of epistemic formulas to that of lower-order epistemic formulas, and as basis we resort to change of propositional formulas. The essential difference between revision and update is: revision satisfies the conjunction property that when φ∧φ′ is satisfiable, φ◦φ′ ⇔ φ∧φ′ , while update satisfies the distribution property that when both φ1 and φ2 are satisfiable, (φ1 ∨ φ2) ⋄ φ′ ⇔ (φ1 ⋄ φ′ ∨ φ2 ⋄ φ′ ).

We begin with some notation. If there exist φ ∈ Φ and φ′ ∈ Φ′ s.t. φ ∧ φ′ is satisfiable wrt γ, we let Φ ∗γ Φ′ = {(φ, φ′ ) | φ ∈ Φ, φ′ ∈ Φ′ , φ ∧ φ′ is satisfiable wrt γ}; otherwise, let Φ ∗γ Φ′ = {(φ, φ′ ) | φ ∈ Φ, φ′ ∈ Φ′ }. Intuitively, whenever possible, Φ ∗γ Φ′ restricts our attention to those consistent pairs of formulas. We let Φ ◦ φ′ denote the set {φ ◦ φ′ | φ ∈ Φ}, and similarly for ⋄.

Definition 4.4 Let φ and φ′ be ACDFs, γ a DNF. The revision of φ with φ′ under γ, φ ◦γ φ′ , is recursively defined:

1. When φ and φ′ are propositional, the result is φ ◦s (φ′ ∧ γ), where ◦s is Satoh's revision operator.
2. When φ = φ0 ∧ ∧a∈B∇aΦa, φ′ = φ′0 ∧ ∧a∈B′∇aΦ′a , φ ∧ φ′ is satisfiable wrt γ, φ ◦γ φ′ is defined as:

1. When φ = φ0 ∧ ∧a∈B∇aΦa, φ′ = φ′0 ∧ ∧a∈B′∇aΦ′a , φ ∧ φ′ is unsatisfiable wrt γ, φ ◦γ φ′ is defined as:

where Φ∗a = {φ◦γ φ′ | (φ, φ′ ) ∈ Φa ∗γ {∨ Φ′a }}, Φ′′ a = {φ′ ∈ Φ′a | there exists a φ ∈ Φ∗a s.t. φ |=γ ¬(¬φ′ )}, where ¬φ′ is converted to ACDF during compilation.

Rule 2 and 4 are for the purpose of the conjunction property. Recall that ∇aΦa ⇔Ka(∨ Φ) ∧LaΦ, hence ∨ Φa is the belief of agent a, and each φ ∈ Φa is a possibility for agent a. The intuition behind Rule 3 is as follows. When there exist old possibilities that are consistent with the new belief ∨ Φ′a , we just keep these possibilities, otherwise we revise each possibility with the new belief, which explains the definition of Φ∗a . Also, among all the new possibilities, we remove those weaker ones, getting Φ′a - Φ′′ a . This is because we would like to get a revision result as strong as possible. For example, suppose Φ∗a = {p ∧ q}, and Φ′a = {p}; then we obtain ∇a{p ∧ q}, which is strictly stronger than ∇a{p ∧ q, p}.

Note that except for a polynomial number of calls to propositional revision, the revision operation can be done in polynomial time.

We say that an ACDF is disjunct-wise satisfiable (dsatisfiable for short) wrt γ if it is a disjunctive CDF and each disjunct is satisfiable wrt γ, or it is a propositional or CDF term which is satisfiable wrt γ.

Proposition 4.5 Let φ and φ′ be ACDFs d-satisfiable wrt γ. Let φ∗ = φ ◦γ φ′ . Then φ∗ is d-satisfiable wrt γ, and φ∗ |=γ φ′ . Moreover, when φ∧φ′ is satisfiable wrt γ, φ∗ ⇔γ φ∧φ′ .

Proof: We prove by induction on ‖φ‖ + ‖φ′ ‖.

1. φ and φ′ are propositional. The properties follow from the definition of Satoh's revision.
2. φ = φ0 ∧ ∧a∈B∇aΦa, φ′ = φ′0 ∧ ∧a∈B′∇aΦ′a , φ ∧ φ′ is satisfiable wrt γ. Let a ∈ B∩B′ . Since φ∧φ′ is satisfiable wrt γ, by Proposition 2.11, for each φa ∈ Φa, φa ∧ ∨ Φ′a is satisfiable wrt γ. By induction, φa ◦γ ∨ Φ′a ⇔γ φa ∧ ∨ Φ′a . Similarly, for each φ′a ∈ Φ′a , φ′a ◦γ ∨ Φa ⇔γ φ′a ∧ ∨ Φa. By Proposition 2.6 (3), φ◦γ φ′ ⇔γ φ∧φ′ . It follows that φ◦γ φ′ is satisfiable wrt γ and φ ◦γ φ′ |=γ φ′ .
3. φ = φ0 ∧ ∧a∈B∇aΦa, φ′ = φ′0 ∧ ∧a∈B′∇aΦ′a , φ ∧ φ′ is unsatisfiable wrt γ. Let a ∈ B ∩ B′ . By induction, for each φa ∈ Φa, φa ◦γ ∨ Φ′a is d-satisfiable wrt γ, hence each element of Φ∗a is d-satisfiable wrt γ. Thus φ◦γ φ′ is satisfiable wrt γ. By induction, φ0 ◦γ φ′0 |=γ φ′0 , and for each φ∗a ∈ Φ∗a , φ∗a |=γ ∨ Φ′a . Also, by the definition of Φ′′ a , for each φ′a ∈ Φ′a , there exists φ∗a ∈ Φ∗a ∪ (Φ′a - Φ′′ a ) s.t. φ∗a |=γ φ′a . By Proposition 2.12, φ ◦γ φ′ |=γ φ′ .
4. φ = ∨ Φ, φ′ = ∨ Φ′ , φ ∧ φ′ is satisfiable wrt γ. Then Φ∗γΦ′ = {(φ1, φ′1 ) | φ1 ∈ Φ1, φ′1 ∈ Φ′1 , φ1∧φ′1 is satisfiable wrt γ}. By induction, for each (φ1, φ′1 ) ∈ Φ ∗γ Φ′ , φ1 ◦γ φ′1 is satisfiable wrt γ, and φ1 ◦γ φ′1 ⇔γ φ1 ∧ φ′1 . Thus φ ◦γ φ′ is d-satisfiable wrt γ, and φ ◦γ φ′ = ∨{φ1 ◦γ φ′1 | (φ1, φ′1 ) ∈ Φ ∗γ Φ′ } ⇔γ ∨{φ1 ∧ φ′1 | (φ1, φ′1 ) ∈ Φ ∗γ Φ′ } ⇔γ φ ∧ φ′ . It follows that φ ◦γ φ′ |=γ φ′ .

5. φ = ∨ Φ, φ′ = ∨ Φ′ , φ∧φ′ is unsatisfiable wrt γ. Then Φ ∗γ Φ′ = {(φ1, φ′1 ) | φ1 ∈ Φ1, φ′1 ∈ Φ′1 }. Since both φ and φ′ are d-satisfiable wrt γ, for each (φ1, φ′1 ) ∈ Φ ∗γ Φ′ , both φ1 and φ′1 are satisfiable wrt γ. By induction, φ1 ◦γ φ′1 is satisfiable wrt γ, and φ1 ◦γ φ′1 |=γ φ′1 . Hence φ ◦γ φ′ is d-satisfiable wrt γ, and φ ◦γ φ′ |= φ′ .

Definition 4.6 Let φ and φ′ be ACDFs, γ a DNF. The update of φ with φ′ under γ, denoted φ ⋄γ φ′ , is recursively defined:

1. When φ and φ′ are propositional, the result is φ⋄w (φ′ ∧ γ), where ⋄w is Winslett's update operator.
2. When φ = φ0∧∧a∈B∇aΦa and φ′ = φ′0∧∧a∈B′∇aΦ′a , φ ⋄γ φ′ is defined as follows:

where Φ∗a = Φa ⋄γ ∨ Φ′a , Φ′′ a = {φ′ ∈ Φ′a | there exists a φ ∈ Φ∗a s.t. φ |=γ ¬(¬φ′ )}, where ¬φ′ is converted to ACDF during compilation.

1. (∨ Φ) ⋄γ φ′ = ∨φ∈Φ φ ⋄γ φ′ .
2. When φ is a CDF term, φ ⋄γ (∨ Φ′ ) = ∨{φ ⋄γ φ′ | (φ, φ′ ) ∈ {φ} ∗γ Φ′ }.

Rule 3 and the definition of Φ∗a in Rule 2 are for the purpose of the distribution property. Rule 4 is to approximate the principle of minimal change: when there is φ′ ∈ Φ′ s.t. φ′ is consistent with φ, we simply ignore those which are not.

Note that except for a polynomial number of calls to propositional update, the update operation can be done in polynomial time.

Proposition 4.7 Let φ and φ′ be ACDFs d-satisfiable wrt γ. Let φ∗ = φ ⋄γ φ′ . Then φ∗ is d-satisfiable wrt γ, and φ∗ |=γ φ′ . Moreover, (φ1 ∨ φ2) ⋄γ φ′ ⇔γ (φ1 ⋄γ φ′ ∨ φ2 ⋄γ φ′ ).

Proof: We prove by induction on ‖φ‖ + ‖φ′ ‖.

1. φ and φ′ are propositional. The properties follow from the definition of Winslett's update.
2. φ = φ0 ∧ ∧a∈B∇aΦa, φ′ = φ′0 ∧ ∧a∈B′∇aΦ′a . Let a ∈ B ∩ B′ . By induction, for each φa ∈ Φa, φa ⋄γ ∨ Φ′a is d-satisfiable wrt γ, hence each element of Φ∗a is d-satisfiable wrt γ. Thus φ ⋄γ φ′ is satisfiable wrt γ. By induction, φ0 ⋄γ φ′0 |=γ φ′0 , and for each φ∗a ∈ Φ∗a , φ∗a |=γ ∨ Φ′a . Also, by the definition of Φ′′ a , for each φ′a ∈ Φ′a , there exists φ∗a ∈ Φ∗a ∪
3. (Φ′a -Φ′′ a ) s.t. φ∗a |=γ φ′a . By Proposition 2.12, φ⋄γφ′ |=γ φ′ . 3. φ = ∨ Φ. Clearly, the disjunction property holds. Since φ is d-satisfiable (wrt γ), each φ1 ∈ Φ is satisfiable. By induction, for each φ1 ∈ Φ, φ1⋄γφ′ is d-satisfiable and φ1⋄γφ′ |=γ
4. φ′ . Thus φ ⋄γ φ′ is d-satisfiable wrt γ and φ ⋄γ φ′ |=γ φ′ .
5. φ is a CDF term, φ′ = ∨ Φ′ . Since φ′ is d-satisfiable (wrt γ), each φ′1 ∈ Φ′ is satisfiable. By induction, for each φ′1 ∈ Φ′ , φ ⋄γ φ′1 is d-satisfiable and φ ⋄γ φ′1 |=γ φ′1 . Thus φ ⋄γ φ′ is d-satisfiable wrt γ and φ ⋄γ φ′ |=γ φ′ .

∇2{at(2, p2) ∧ ¬in(b1, p2) ∧ ¬in(b2, p2)}.

4.4 Planning

Like [Wan et al., 2015], we adapt the PrAO algorithm for contingent planning [To et al., 2011] as our planning algorithm. PrAO extends AND/OR forward search with pruning techniques. It uses the so-called minimal DNF formulas to represent states and employs the following basic operations: reasoning, equivalence checking, update wrt ontic actions, and update wrt sensing actions. We use ACDFs to represent states, and for the above operations, we plug in our operations of reasoning, strong equivalence checking, progression wrt deterministic actions, and progression wrt sensing actions.

5 Implementation and Experimentation

Based on the theoretic work, we have developed EPDDL - an extension of PDDL [McDermott et al., 1998], to describe multi-agent epistemic planning problems, and with naive implementations of Satoh's revision and Winslett's update operators, implemented a multi-agent epistemic planner MEPK. 1

We evaluate MEPK with Selective-communication (SC) and Collaboration-and-communication (CC) domains adapted from [Kominis and Geffner, 2015], and Grapevine from [Muise et al., 2015], where SC is called "Corridor". We also made up three domains: Assembly-line (AL), and domains adapted from the classic Gossip problem [Attamah et al., 2014] and the knowledge game Hexa [van Ditmarsch, 2001]. We didn't consider three domains from [Kominis and Geffner, 2015]: MuddyChildren, Sum, andWordRooms. The first two involve public announcements, which result in common knowledge, and so we are not able to model them. The third is a variant of CC. Below we give description of each domain we use.

Selective-communication: SC(n). There are n rooms in a corridor. The agents can move from a room to a neighboring room. When agent i tells some information, all the other agents in the same room or in a neighboring room can hear what was told. Initially, each agent is in one of the rooms. The goal is that some agents get to know some information while some other agents do not. Versions of SC(n) with higher modal depth result from approximation of common knowledge with higher-order knowledge.

Collaboration-and-communication: CC(k,n),*CC(k,n). These are variants of Example 1 where there are k boxes and n rooms. For efficiency reason, the *CC(k, n) variant adopts an encoding somewhat different from that for Example 1. The CC(k, n) variant imitates the version from [Kominis and Geffner, 2015] in that with one action, an agent can see which boxes are in a room.

Grapevine(n). A few guests attend a meeting in a villa with n rooms. Each guest has his own secret to share with others. Each guest can move between the rooms, and broadcast his secret to the guests in the same room. The goal is that only some of the guests obtain the designated secrets.

1 The link to our planner and domain sources is:

https://github.com/sysulic/MEPK.

Hexa Game. There are k agents and k cards, each with a unique color. Initially, everyone is holding a card, and can only see the color of his own card. A player can ask a question to another player whether his card is of a certain color. The question should always be honestly answered. The goal is for some agent to know the cards of all players.

Assembly-line (AL). There are two agents, each responsible for processing a part of a product. It is possible that an agent fails in processing his part. An agent can inform the other agent the status of his task. Two agents decide to assemble the product or restart depending on their knowledge of the status of the agents' tasks.

Gossip. Each of several friends has his own secret to share. Instead of sharing in public, they are only allowed to make a call to each other. In each call, they exchange all the secrets they know. The goal is that everyone knows all the secrets of other friends.

Our experiments were run on a Linux machine with 2.50GHz CPU and 4GB RAM. Our experimental results are shown in Table 1. The 2nd-5th columns indicate the number of agents, the number of sensing and deterministic actions, the number of atoms, and the modal depth of the KBs. If the number of sensing actions is 0, the planning problem is conformant, else it is contingent. In the MEPK column, A-B (X/Y) stands for A seconds of total time, B seconds spent on search, and depth X and Y nodes of solution tree. The results show the viability of our approach. Nonetheless, our planner does not scale well on Hexa. This is because the search performance is greatly influenced by the number of sensing actions. In Hexa, there are 48 (resp. 100) sensing actions when there are 4 (resp. 5) agents.

We reran the corresponding experiments of [Kominis and Geffner, 2015] and [Muise et al., 2015] using an FF planner and their domain sources, and the comparison results are shown in Table 2. In the last two columns, (X) stands for plan length X, and "na" means that the planning problem is not considered by the planner. For example, CC is not encoded by Muise et al. ; as to SC, K&G only encodes SC(4) with 3 agents and d = 1. The results show that the searching performance of MEPK is reasonable, but still worse than the two other planners. This is because MEPK uses more general and complex KBs, and hence spends more time on reasoning and progression. However, when it comes to total time, MEPK performs better than the two other planners, with the exception of SC(4) with 7 agents. This is because MEPK saves from the expensive compilation into classical planning.

6 Conclusions

In this paper, we have proposed a general representation framework for multi-agent epistemic planning where arbitrary multi-agent epistemic formulas are used and solutions are action trees. To support efficient reasoning and progression, we resort to alternating cover disjunctive formulas, and propose basic revision and update algorithms for them. Based on the theoretic work, we have implemented a native multiagent epistemic planner MEPK, which does not rely on compilation into classical planning. Experimental results have demonstrated the viability of our approach. In the future, we are interested in doing a model-theoretic study of higherorder belief change and improving our revision and update algorithms. Also, we would like to extend our current work to accommodate common knowledge.

Acknowledgments

We thank the anonymous reviewers for helpful comments. We are grateful to Liangda Fang for helpful discussions on the paper, and Hans van Ditmarsch for introducing us to the normal form of alternating cover disjunctive formulas. Xiao Huang and Yongmei Liu acknowledge support from the Natural Science Foundation of China under Grant Nos. 61572535 and 61463044. Biqing Fang and Hai Wan acknowledge support from National Natural Science Foundation of China under grant 61573386, and Natural Science Foundation of Guangdong Province under grant 2016A030313292.