Multi-agent Epistemic Planning with Common Knowledge

1 Introduction

Reasoning about knowledge and beliefs and their change plays an important role in many intelligent tasks, since actions may have preconditions involving agents' knowledge and beliefs, which may be changed by agents' actions. In some applications, even higher-order knowledge and beliefs, i.e., knowledge and beliefs about other agents' knowledge and beliefs, turn out to be insufficient, and common knowledge is needed. We say that φ is common knowledge of a group of agents if everybody knows φ, everybody knows everybody knows φ, and so on to infinity. For example, common knowledge is needed for agreement and coordination. To illustrate, suppose that Alice and Bob are trying to coordinate their actions. This involves the agents' agreeing on when to perform the actions, which we represent by φ. We expect that if Alice and Bob agree on something, then each of them knows that they have agreed on that. By induction, Alice and Bob have common knowledge of φ. The common knowledge modality adds a great deal of expressive power to multi-agent modal logics. As a result, deciding satisfiability becomes EXPTIME-complete [Halpern and Moses, 1992].

In the past decade, multi-agent epistemic planning has received much attention from both dynamic logic and planning communities. On the theory side, Bolander and Andersen [2011] formalized multi-agent epistemic planning (MEP) based on dynamic epistemic logic [Van Ditmarsch et al., 2007], where both states and actions are represented as Kripke models. Very recently, Huang et al. [2017] proposed a general representation framework for MEP, where the initial knowledge base (KB) and the goal, the preconditions and effects of actions can be arbitrary multi-agent epistemic formulas, progression of KBs wrt actions is achieved through higher-order belief revision or update based on effects of actions, and the solution is an action tree branching on sensing results. On the implementation side, Kominis and Geffner [2015] and Muise et al. [2015] solved restricted versions of MEP problems by compiling them into classical planning, and Huang et al. [2017] implemented a contingent MEP planner based on AND/OR forward search. However, the implementation of [Muise et al., 2015] does not support common knowledge, and those of [Kominis and Geffner, 2015] and [Huang et al., 2017] provide very limited support for common knowledge, basically static propositional common knowledge. To the best of our knowledge, LoTREC [del Cerro et al., 2001], a theorem prover for S5, is the only implementation capable of reasoning with common knowledge.

In this paper, we extend the MEP framework proposed by Huang et al. to incorporate general common knowledge. To support efficient reasoning in multi-agent KD45 logic, they made use of a normal form called alternating cover disjunctive formulas [Hales et al., 2012]. However, this normal form cannot be directly generalized to support reasoning with common knowledge. Thus we propose a novel normal form for multi-agent KD45 with common knowledge. This normal form makes use of a new common knowledge modality Caφ which means that it is common knowledge that everybody except agent a knows φ. We propose a novel algorithm for checking satisfiability for this normal form. Also, we propose revision and update algorithms for this normal form. The essential idea is to change agents' common knowledge before changing agents' knowledge, and carry the changed common knowledge to change knowledge to ensure the consistency between knowledge and common knowledge. Based on our reasoning, revision, and update algorithms, we implemented a multi-agent epistemic planner called MEPC. Our planner successfully generated solutions for several domains that demonstrate the typical usage of common knowledge.

2 Preliminaries

In this section, we introduce the background work of our paper, i.e., the multi-agent modal logic and the epistemic planning modeling framework proposed by Huang et al.

2.1 Multi-agent Modal Logic

We fix a finite set of atoms P and a finite set of agents A.

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

Intuitively, Kaφ means agent a knows φ, and Cφ means all agents commonly know φ. We let Laφ and Dφ abbreviate for ¬Ka¬φ and ¬C¬φ, respectively. Intuitively, Laφ means agent a thinks φ is possible, and Dφ means all agents commonly think φ is possible.

We use φ and ψ to represent formulas, Φ and Ψ to represent sets of formulas, ⊤ and ⊥ to denote true and false, respectively. ∨ Φ stands for the disjunction of members in Φ, while LaΦ (resp. DΦ) stands for the conjunction of Laφ (resp. Dφ) where φ ∈ Φ. The modal depth of a formula φ ∈ LKC is the depth of nesting of modalities 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.

When wRaw′ , we say w′ is an a-child of w. We say Ra is serial if for any w ∈ W, there is a w′ ∈ W s.t. wRaw′ ; we say Ra is transitive if wRau and uRav imply wRav; we say Ra is Euclidean if wRau and wRav imply uRav. 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 : W → 2P is a valuation map. A pointed Kripke model is a pair s = (M,w), where M is a Kripke model and w is a world of M.

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

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

Consider the context of KCn or KD45Cn . We say φ is satisfiable if there is a Kripke model (M,w) s.t. M,w |= φ. We say φ entails ψ, written φ |= ψ, if for any Kripke model (M, w), M, w |= φ entails M, w |= ψ. We say φ and ψ are equivalent, written φ ⇔ ψ, if φ |= ψ and ψ |= φ.

Theorem 2.5. [Halpern and Moses, 1992] The satisfiability problems for KCn and KD45Cn are EXPTIME-complete.

Halpern and Moses presented an algorithm for checking satisfiability in KCn . Given a formula φ ∈ LKC, their algorithm first generates a set S consisting of all subformulas of φ and their negations. Then it computes a set W consisting of all subsets A of S that are propositionally consistent and maximal, i.e., either ψ ∈ A or ¬ψ ∈ A for each ψ ∈ S. Finally it iteratively builds a model for φ with worlds in W.

We now define a normal form for KCn .

Definition 2.6. The set of modal terms is inductively defined:

• A propositional term, i.e., a conjunction of propositional literals, is a modal term;
• A formula of the form φ0 ∧ ∧a∈A(Kaφa ∧ LaΨa) ∧ Cµ ∧DΛ is a modal term, where φ0 is a propositional term, Ψa, Λ are sets of modal terms, and φa, µ are conjunctions of disjunctions of modal terms.

A formula φ is in DNF if it's a disjunction of modal terms. A formula φ is in CDNF if it's a conjunction of DNFs.

So the knowledge and common knowledge parts of a modal term are in CDNF.

Proposition 2.7. In KCn , any formula in LKC can be transformed to an equivalent DNF whose length is at most singly exponential in the length of the original formula.

Proof. For an arbitrary modal formula φ ∈ LKC, we first put it into negation normal form. Then we treat modal atoms, ie, formulas of the form Kψ, Lψ, Cψ and Dψ, as propositional atoms and transform the whole formula into propositional DNF. Then for the ψ in each modal atom, we repeat this process. By induction on the modal depth of φ, we can show that the length of the resulting DNF is at most singly exponential in the length of φ.

In the rest of the paper, the logic we use is KD45Cn , except that in Section 3.1, we discuss satisfiability for KCn .

2.2 Epistemic PlanningModeling Framework

We follow the modeling framework for multi-agent epistemic planning (MEP) in [Huang et al., 2017], and extend it with the support of general common knowledge.

We illustrate the framework with the classic muddy children example [Fagin et al., 1995]. There are n children playing together and m of them get mud on their foreheads. Each can see the mud on others but not on his own forehead. The father announces "At least one of you has mud on your forehead". The father then keeps asking "Does any of you know whether you have mud on your own forehead?" It turns out the first m-1 times he asks the question, they will all say "No", but then the mth time the children with muddy foreheads will all answer "Yes".

Definition 2.8. A MEP problem 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 ∈ LKC is the initial KB, and G ∈ LKC is the goal.

Example 1. Assume that there are three children (A = {a, b, c}) and all of them are muddy. The atoms are: mi, indicating the ith child is muddy. The deterministic actions are: announce, the father announces that at least one of them is muddy; askno, the father asks whether anyone knows that he is muddy, but no child answers "Yes". The initial KB is ma ∧ mb ∧ mc ∧ ∧i∈A(Ki ∧j̸=i mj). The goal is ∧i∈A(mi → Kimi).

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

Definition 2.10. A sensing action is a triple 〈pre, pos, neg〉, where pre, pos, neg ∈ LKC indicate the precondition, the positive result, and the negative result, respectively.

For example,

announce = 〈⊤, {eff}〉, where eff = 〈⊤, C ∨i mi〉. askno = 〈pre, {eff1, eff2}〉, where:

• pre = ∧i (¬Kimi ∧¬Ki¬mi),
• eff1 = 〈C ∨i mi,C ∨i̸=j (mi ∧mj)〉,
• eff2 = 〈C ∨i̸=j (mi ∧mj),C ∧i mi〉.

Here pre says that no child knows if he is muddy, eff1 says: under the condition that the children commonly know that at least one child is muddy, they commonly know at least two of them are muddy, and eff2 says: under the condition that the children commonly know that at least two of them are muddy, they commonly know that all three children are muddy.

An action a is executable wrt a KB φ ∈ LKC if φ |= pre(a). Suppose a is executable wrt φ. The progression of φ wrt a is defined by resorting to belief change operators. 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. We use a revision operator ◦ and an update operator ⋄ for LKC. We use update for progression wrt deterministic actions and revision for sensing actions.

Definition 2.11. Let φ ∈ LKC and a a deterministic action where eff(a) = {〈φ1, ψ1〉, . . . , 〈φn, ψn〉}. Suppose φi1 , . . . , φim are all the φi's s.t. φ |= φi. Then the progression of φ wrt a is defined as ((φ ⋄ ψi1 ) . . . ) ⋄ ψim .

Definition 2.12. Let φ ∈ LKC and a a sensing action. Then the progression of φ wrt a with positive (resp. negative) result is φ+ = φ ◦ pos(a) (resp. φ- = φ ◦ neg(a)).

The progression of φ wrt a sequence of actions (with sensing results for sensing actions) is inductively defined as follows: prog(φ, ϵ) = φ; prog(φ, (a; σ)) = prog(prog(φ, a), σ) if φ |= pre(a), and undefined otherwise.

A solution of a MEP problem is an action tree branching on sensing results, such that the progression of the initial KB wrt each branch in the tree entails the goal.

3 Checking Satisfiability

In this section, we first present an algorithm for checking satisfiability in KCn , and then extend it to KD45Cn .

3.1 KCn Satisfiability

The main idea of our algorithm for checking satisfiability in KCn is as follows. The input formula is in DNF, and we attempt to build a model for it recursively. When checking a model term δ = φ0 ∧ ∧a∈A(Kaφa ∧ LaΨa) ∧ Cµ ∧ DΛ, if φ0 is unsatisfiable, we immediately return ⊥, otherwise we proceed as follows:

• For each agent a and each possibility ψa ∈ Ψa, we conjoin it with knowledge φa and common knowledge µ∧Cµ, and check if the resulting formula is satisfiable.
• If not, we immediately return ⊥, otherwise we check λ ∧ φa ∧ µ ∧ Cµ and Dλ ∧ φa ∧ µ ∧ Cµ for each agent a and each common possibility λ ∈ Λ.

Each of the above formulas is in CDNF, we call it a child of δ. When checking a CDNF φ, we put it into a DNF ∨ ∆, and recursively check each δ′ ∈ ∆. We call δ′ a derivant of φ.

However, the complication is that due to the presence of common knowledge, some newly generated modal terms might be the same as previous ones. To handle this issue, we maintain a graph whose nodes are modal terms. When a new modal term is generated, we mark it by ⊤, and when we know it is unsatisfiable, mark it by ⊥. Also, when a new modal term δ′ is derived from a child of a modal term δ, we add an edge from δ to δ′ , mark the edge by 1 if δ′ is derived from ψa ∧ µ ∧ Cµ, and 2 otherwise. Now, when checking a modal term δ which already exists, we return its current mark.

A formula δ may not be satisfiable if it's marked ⊤ by the above methods. We further update each modal term's mark by checking whether its common possibilities are satisfied. For each conjunct Dλ in each modal term δ, we check whether there is a modal term δ′ reachable from δ s.t. λ is a conjunct of δ′ and δ′ is marked by ⊤. If not, we mark δ by ⊥ and further propagate ⊥ to its ancestors through 1-edges. We repeat this procedure until no mark is updated.

Definition 3.1. Let δ be a modal term. For a ∈ A, let γa denote a's knowledge, i.e., γa = φa ∧µ∧Cµ. We define the set of δ's children, GenK (δ), as the union of the following:

• S1 = {γa ∧ ψa | a ∈ A, ψa ∈ Ψa};
• Sλ1 = {γa ∧ λ | a ∈ A}, and Sλ2 = {γa ∧ Dλ | a ∈ A}, where λ ∈ Λ.

Proposition 3.2. Let δ be a satisfiable modal term. Then the following hold for GenK (δ):

• for all φ ∈ S1, φ is satisfiable;
• for all λ ∈ Λ, there is φ ∈ Sλ1 ∪Sλ2 s.t. φ is satisfiable.

Algorithm 1: CheckK (φ)

input: φ ∈ LKC is in DNF ∨ ∆ output: ⊤ / ⊥ set G = (W, R) to the empty graph; if SatK (φ, ⊥, a, 1) = ⊥ then return ⊥; call Update; foreach δ in ∆ do if Mark(δ) = ⊤ then return ⊤; return ⊥;

Function SatK (φ, φ′ , i, n)

input: φ is in CDNF, φ′ is a modal term, i ∈ A, n = 1, 2 if φ is not a modal term then transform φ into DNF ∨ ∆; foreach δ in ∆ do if SatK (δ, φ′ , i, n) = ⊤ then return ⊤; return ⊥; else if φ′ ̸= ⊥ then Ri ← Ri ∪ {(φ′ , φ)n}; if φ ∈ W then return Mark(φ); W ← W ∪ {φ}, Mark(φ) ← ⊤; GenK (φ) = S1 ∪ ⋃λ∈Λ(Sλ1 ∪ Sλ2 ); if one of the following conditions holds: 1. φ0 is propositionally unsatisfiable; 2. ∃δa ∈ S1: SatK (δa, φ, a, 1) = ⊥. thenMark(φ) ←⊥, return ⊥; foreach δa in ⋃λ∈Λ Sλ1 ∪Sλ2 do call SatK (δa, φ, a, 2);

return ⊤;

Procedure Update

foreach δ in W and λ s.t. Dλ is a conjunct of δ do let Child(δ, λ) be a set of modal terms δ′ where: 1. δ′ is reachable from δ; 2. λ is a conjunct of δ′ ; 3. Mark(δ′ ) = ⊤. U pdated ← ⊤; while Updated = ⊤ do Updated ← ⊥; UpdatedNodes ← ∅; foreach δ in W and λ s.t. Dλ is a conjunct of δ do if Mark(δ) = ⊤ and Child(δ, λ) = ∅ then Mark(δ) ← ⊥; Updated ← ⊤; UpdatedNodes ← UpdatedNodes ∪ {δ}; foreach δ in UpdatedNodes do call Propagate(δ); foreach δ in W and λ do delete δ′ in Child(δ, λ) s.t. Mark(δ′ ) = ⊥;

We demonstrate the procedure of CheckK (φ) by Figure 1. Let φ = Cp ∧ D¬p and A = {a}.

1. We calculate GenK (φ) = {δ1, δ2}, where δ1 = ¬p∧p∧ Cp and δ2 = D¬p ∧ p ∧ Cp, and set W = {φ, δ1, δ2} and Ra = {(φ, δ1)2, (φ, δ2)2}.
2. We check δ1 next. Since its propositional part is unsatisfiable, we set Mark(δ1) = ⊥.
3. We turn to δ2, GenK (δ2) = {δ1, δ2}, Ra ← Ra∪{(δ2, δ1)2, (δ2, δ2)2}, Mark(δ2) = ⊤. Thus Mark(φ) = ⊤.
4. Since D¬p is a conjunct of φ and δ2 but there isn't a reachable modal term δ′ s.t. ¬p is a conjunct of δ′ and Mark(δ′ ) = ⊤, we set Mark(φ) = Mark(δ2) = ⊥. Eventually CheckK (φ) returns ⊥.

Theorem 3.3. The complexity of CheckK (φ) is O(4(d+1)cl+l ), where l is the length of φ, d is the modal depth of φ, and c is the depth of nesting of C modalities in φ.

Procedure P ropagate(δ)

input: δ is a modal term

foreach δ′ inW s.t. (δ′ , δ)1 ∈ R do

if Mark(δ′ ) = ⊤ then

Mark(δ′ ) ← ⊥; call Propagate(δ′ );

Proof sketch. First consider φ without C. For any modal term δ generated during the algorithm, δ corresponds to a substring of φ. Hence the graph has at most 2l nodes. Now consider that φ contains C modalities. Let Cν be the conjunction of all subformulas Cµ in φ. The maximal length of Cν is cl. The children generated from Cν are in the form ν1 ∧ Cν, where ν1 doesn't contain common knowledge since Cν is maximal. For 1 ≤ i < d, we name the children generated from νi as νi+1. All νi corresponds to a substring of ν, thus the length of νi is less than cl. Since the children of Cν without common knowledge will be reduced to propositional formulas after at most (d-1) recursions, the maximal length of the form ∧1≤i≤d νi ∧ Cν in a modal term generated during the algorithm is cl + dcl. Hence the maximum number of nodes is 2(d+1)cl+l . Let n be the number of nodes. Cycle checking and updating marks requires O(n2 ) time. Thus we obtain the complexity result O(4(d+1)cl+l ). □

We proceed to prove soundness and completeness of CheckK . For soundness, when CheckK (φ) returns ⊤, we build a model Mφ for φ by modifying the frame G = (W, R) as follows: remove δ ∈ W s.t. Mark(δ) = ⊥; rename δ ∈ W to wδ; and create a valuation map V s.t. V (wδ) satisfies φ0 in δ. We show that for each wδ in Mφ, Mφ,wδ |= δ. To facilitate the proof, we introduce the notion of implicants.

Definition 3.4. If the conjunction of a CDNF φ and another CDNF φ′ is equivalent to a DNF ∨ ∆, we call each δ ∈ ∆ an implicant of φ, and write δ | .= φ.

Obviously, if δ | .= φ, then δ |= φ. If a modal term δ′ is a subterm of a modal term δ, i.e., the conjuncts of δ′ is a subset of those of δ, then δ is an implicant of δ′ . In Algorithm 1, when a modal term δ′ is added as an a-child of a modal term δ = φ0 ∧ ∧a∈A(Kaφa ∧ LaΨa) ∧ Cµ ∧ DΛ, δ′ is an implicant of φa, µ and Cµ; similarly, δ′ is an implicant of some ψa ∈ Ψa, or an implicant of λ or Dλ for some λ ∈ Λ.

Lemma 3.5. When CheckK (φ) returns ⊤, for all wδ ∈ Mφ, we have Mφ,wδ |= ψ if δ | .= ψ.

Proof. We prove by structural induction on ψ. Consider ψ in the following forms:

• A propositional literal. Then ψ is a conjunct of the propositional term of δ. By the definition of V (wδ), we have Mφ,wδ |= ψ.
• ψ1 ∧ ψ2. Then δ | .= ψ1 and δ | .= ψ2. By induction, Mφ, wδ |= ψ1 andMφ,wδ |= ψ2. SoMφ,wδ |= ψ1 ∧ψ2.
• ψ1 ∨ ψ2. Then δ | .= ψ1 or δ | .= ψ2. By induction, Mφ,wδ |= ψ1 or Mφ,wδ |= ψ2. SoMφ,wδ |= ψ1 ∨ψ2.
• Kaψ′ . By Algorithm 1, for all wδ′ s.t. wδRawδ′ , δ′ | .= ψ′ . By induction, Mφ,wδ′ |= ψ′ . SoMφ,wδ |=Kaψ′ .
• Laψ′ . By Algorithm 1, there is wδ′ s.t. wδRawδ′ and δ′ | .= ψ′ . If not, δ will be marked ⊥ by Propagate. By induction, Mφ,wδ′ |= ψ′ . SoMφ,wδ |= Laψ′ .
• Cψ′ . By Algorithm 1, for all wδ′ reachable fromwδ, δ′ | .= ψ′ . By induction,Mφ,wδ′ |= ψ′ . SoMφ,wδ |= Cψ′ .
• Dψ′ . By Algorithm 1, there is wδ′ reachable from wδ s.t. δ′ | .= ψ′ . If not, δ will be marked ⊥ by Update. By induction, Mφ,wδ′ |= ψ′ . SoMφ,wδ |=Dψ′ . □

For completeness, we prove a modal term δ is unsatisfiable if it's marked ⊥. The difficult case is when δ is marked ⊥ during update. We introduce a lemma to handle this case.

Lemma 3.6. Let δ be a modal term s.t. δ | .= Dλ. When δ is satisfiable, there is a modal term δ′ reachable from δ s.t. δ′ | .= λ and δ′ is satisfiable.

Proof. Since δ is satisfiable, there is a model (M,w) s.t. M,w |= δ. Since δ | .=Dλ, there is a path w,w1, . . . ,wm,w′ in M s.t. M,w′ |= λ. Assume that wRa1 w1, wmRa′w′ and wiRai+1 wi+1 for 1 ≤ i < m. By Algorithm 1, there is a path δ, δ1, . . . , δm, δ′ in W where δi | .= Dλ for each i and δ′ | .= λ. Moreover, we have (δ, δ1) ∈ Ra1 , (δm, δ′ ) ∈ Ra′ and (δi, δi+1) ∈ Rai+1 . By induction, we can show that for each i = 1, . . . ,m, M,wi |= δi. SoM,w′ |= δ′ .

Theorem 3.7. CheckK (φ) = ⊤ iff φ is satisfiable in KCn .

Proof. ⇒: Suppose CheckK (φ) returns ⊤. Then there is a world wδ ∈ Mφ s.t. δ | .= φ. By Lemma 3.5, Mφ,wδ |= φ. Thus φ is satisfiable.

⇐: Suppose CheckK (φ) returns ⊥. Let φ = ∨ ∆. Then each modal term in ∆ is marked ⊥. We prove by induction on k that if δ is the kth modal term that CheckK marks ⊥, δ is unsatisfiable. There are 3 cases:

• The propositional term of δ is unsatisfiable.
• There is δ′ ∈ S1 marked by ⊥. By induction, δ′ is unsatisfiable. By Proposition 3.2, δ is unsatisfiable.
• δ contains a conjunct Dλ and for each δ′ reachable from δ where δ′ | .= λ, δ′ is marked ⊥. By induction, δ′ is unsatisfiable. By Lemma 3.6, δ is unsatisfiable. □

3.2 KD45Cn Satisfiability

The main idea of our algorithm for checking satisfiability in KD45Cn is as follows. We require the input formula φ to be in a certain normal form. We apply to φ the algorithm for checking satisfiability in KCn . When the algorithm returns ⊤ and a model for φ, we add edges to the model to make it serial, transitive, and Euclidean. The normal form we use ensures that after adding edges, the model still satisfies φ. To motivate our normal form, let's consider two examples.

Example 2. Let A = {a, b}, P = {p}, and φ = DKap. Consider M = (W,R, V ) where W = {0, 1, 2}, Ra = {(0, 1), (1, 2)}, Rb = ∅, V (0) = V (1) = ∅, and V (2) = {p}. Then (M, 0) is a model for φ in KCn , but it can't be made a model for φ in KD45Cn by adding edges. Now suppose we have an modality Daφ meaning φ holds in some world reachable by a path whose last edge is not of agent a. Let M ′ be the same as M except Ra = {(1, 2)} and Rb = {(0, 1)}. Then (M ′ , 0) is a model for φ′ = DaKap in KCn , and it can be made a model for φ′ in KD45Cn by adding edges.

Example 3. Let φ = La(p ∧Ka¬p). Then φ is satisfiable in KCn but not in KD45Cn , thus KCn algorithm obtains the wrong answer. Note that φ entails Ka¬p in KD45Cn . If we add Ka¬p to φ, KCn algorithm could answer false correctly.

In the following, we introduce our normal form.

Definition 3.8. The semantics of the subscripted common knowledge modality Ca where a ∈ A is defined as follows:

• M, w |= Caφ iff for all u, v s.t. wR∗Au and uRbv where b ̸= a, we have M, v |= φ, where R∗A is the reflexive transitive closure of the union of Ra for a ∈ A.

We let Daφ abbreviate for ¬Ca¬φ. We use LKCS to refer to LKC where the Ca modality is used instead of C.

Definition 3.9. The set of modal S-terms (resp. normal Sterms) is inductively defined as follows:

• A propositional term is a modal (resp. normal) S-term;
• A formula of the form φ0 ∧ ∧a∈A(Kaφa ∧ LaΨa ∧ Caµa ∧DaΛa) is a modal S-term (resp. normal S-term), where φ0 is a propositional term, Ψa,Λa are sets of modal S-terms (resp. normal S-terms), Ψa is not empty, and φa, µa are conjunctions of disjunctions of modal Sterms (resp. φa, µa are disjunctions of normal S-terms).

A formula φ is in SDNF (resp. normal SDNF) if it's a disjunction of modal S-terms (resp. normal S-terms).

In the above definition, note the requirement that Ψa is not empty. Due to seriality, we can always replace an empty Ψa with the set {⊤} in KD45Cn .

Proposition 3.10. The following hold in KD45Cn :

• Cφ⇔ ∧a∈A(Kaφ ∧CaKaφ);
• Dφ ⇔ ∨a∈A(Laφ ∨DaLaφ).

Proof. We only prove Item 1. The ⇒ direction is obvious. For the ⇐ direction, suppose M,w |= ∧a∈A(Kaφ ∧ CaKaφ). Let v be reachable from w and p a shortest path from w to v. If p is of length 1, since M,w |= ∧a∈A Kaφ, M, v |= φ. If p is of length > 1, then the last two edges on the path must be of different agents; otherwise, by transitivity, there is a shorter path from w to v. Let a be the agent of the last edge. Since M,w |= CaKaφ, M, v |= φ. Thus M, w |= Cφ.

By Proposition 3.10, in KD45Cn , every formula is equivalent to a formula in SDNF and a formula in normal SDNF.

As motivated by Example 3, we present the following rules for unfolding nested knowledge.

Proposition 3.11. The following hold in KD45Cn :

• Ka(Kaφ ∧ φ+ ∨ ψ) ⇔ Ka(φ ∧ Kaφ ∧ φ+ ∨ ψ);
• Ka(Cbφ ∧ φ+ ∨ ψ) ⇔ Ka(φ ∧ Cbφ ∧ φ+ ∨ ψ);
• La(Kaφ ∧ φ+) ⇔Kaφ ∧La(Kaφ ∧ φ+);
• La(Cbφ ∧ φ+) ⇔Ka(φ ∧Cbφ) ∧La(Cbφ ∧ φ+).

Here φ ∈ LKCS, φ+ is a modal S-term and ψ is in SDNF.

Definition 3.12. Let φ be in SDNF. We apply the rules for unfolding knowledge to φ, from inside to outside, and then put the resulting formula into an SDNF φ′ . We say that φ′ is in unfolded SDNF. Unfolded normal SDNF is similarly defined.

Proposition 3.13. Let φ be in unfolded SDNF. Given any formula ψ and agent a, if φ |= Kaψ in KD45Cn , then we also have φ |= Kaψ in KCn .

Now we define the set of children of a modal S-term. Note that due to transitivity, Kaφa entails KaKaφa in KD45Cn .

Definition 3.14. Let δ = φ0 ∧ ∧a∈A(Kaφa ∧ LaΨa ∧ Caµa ∧ DaΛa) be a modal S-term. For a ∈ A, we let γa denote the knowledge of a, i.e., γa = φa ∧ Kaφa ∧ Caµa ∧ ∧b̸=a (µb ∧ Cbµb). We define the set of δ's children, written GenKD45 (δ), as the union of the following sets:

• S1 = {γa ∧ ψa | a ∈ A, ψa ∈ Ψa},
• Sbλ1 = {γa ∧ λ | a ∈ A, a ̸= b}, and Sbλ2 = {γa ∧ Dbλ | a ∈ A}, where b ∈ A, λ ∈ Λb.

Proposition 3.15. Let δ be a satisfiable modal S-term. Then the following hold for GenKD45 (δ):

• for all δ′ ∈ S1, δ′ is satisfiable;
• for all b ∈ A and λ ∈ Λb, there is δ′ ∈ Sbλ1 ∪ Sbλ2 s.t. δ′ is satisfiable.

Algorithm 2: CheckKD45 (φ)

input: φ is in unfolded SDNF output: ⊤ / ⊥

CheckK (φ) where GenK is replaced by GenKD45

When CheckKD45 (φ) returns ⊤, we first build a model Mφ for φ as we do for CheckK (φ), and then set each accessibility relation to its transitive and Euclidean closure. Note that seriality is ensured by requiring Ψa non-empty. The normal form we use and the definition of GenKD45 ensure that the resulting KD45Cn model M ′φ still satisfies φ.

Lemma 3.16. Let a, b ∈ A. When CheckKD45 (φ) returns ⊤, for all wδ,wδ′ ∈M ′φ s.t. wδRawδ′ , we have:

• when δ | .=Kaφ, δ′ | .= φ ∧Kaφ;
• when δ | .= Cbφ, δ′ | .= Cbφ;
• when δ′ | .=Kaφ, δ | .=Kaφ;
• when δ′ | .= Cbφ, either δ | .= Cbφ or δ | .=KaCbφ.

Proof. We prove by induction on the order (wδ, wδ′ ) is added to Ra. The induction cases are straightforward. We prove the base case where (wδ,wδ′) is in Ra before edges are added. Item 1 and Item 3 follow from the definition of GenKD45 . From δ′ | .= Kaφ we can infer that δ is an implicant of Kaφ, KaKaφ or LaKaφ. Since δ is in unfolded SDNF, we have δ | .=Kaφ. From δ′ | .= Cbφ we can infer that δ is an implicant of Cbφ, KaCbφ or LaCbφ. If δ is an implicant of LaCbφ, we have δ | .= KaCbφ by unfolding rules.

Lemma 3.17. When CheckKD45 (φ) returns ⊤, for all wδ ∈ M ′φ , we have M ′φ ,wδ |= ψ if δ | .= ψ.

Proof. We only prove the cases whose proofs are different from those for KCn . Consider ψ in the following forms:

• Kaψ′ . By Lemma 3.16, for all wδ′ s.t. wδRawδ′ , δ′ | .= ψ′ . By induction, Mφ,wδ′ |= ψ′ . SoMφ,wδ |=Kaψ′ .
• Caψ′ . By Lemma 3.16, for all wδ′′ s.t. wδR∗Awδ′′ , δ′′ | .= Caψ′ . Then by the definition of GenKD45 , for all wδ′ s.t. wδ′′Rbwδ′ where b ̸= a, we have δ′ | .= ψ′ . By induction, M ′φ ,wδ′ |= ψ′ . SoM ′φ ,wδ |= Caψ′ . □

Theorem 3.18. CheckKD45 (φ) returns ⊤ iff φ is satisfiable in KD45Cn .

The proof for soundness follows from Lemma 3.17, while the proof for completeness is identical to that in Theorem 3.7.

Theorem 3.19. The complexity of CheckKD45 (φ) is O(4(d+1)(c+d)nl+l ), where n is the number of agents, l, c, and d are as in Theorem 3.3.

Proof sketch. The complexity follows from Theorem 3.3 with two increasing from two factors: the common knowledge operator C is transformed into n copies of the subscripted version; knowledge of each agent is preserved when generating children of a modal S-term. □

4 Belief Revision and Update

In this section, we introduce our algorithms for higher-order belief change involving common knowledge. As Huang et al. [2017], we 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 illustrate our main ideas with three examples.

Example 4. Revise Ka(¬p ∧ Ka¬p) with Cp. When we recursively revise ¬p∧Ka¬p, we cannot simply revise it with p, which will give us the incorrect result Ka(p∧Ka¬p)∧Cp;

we will have to revise it with p and carry Cp, which gives us the correct result Ka(p ∧ Kap) ∧ Cp.

Example 5. Revise Ka(¬p ∧ q) with Ka¬q ∧ Lap. We cannot simply revise old knowledge with new knowledge, which gives us ¬p ∧ ¬q, inconsistent with new possibility p. We will take the disjunction of ¬p ∧ ¬q and the revision of old knowledge with the conjunction of new knowledge and new possibility. This gives us ¬p∧¬q ∨p∧¬q, equivalent to ¬q. The same idea applies to the revision of common knowledge.

Example 6. Revise La(p∧q)∧La(¬p∧q) withKap∧Lar. Since there are old possibilities consistent with new knowledge, we will only keep such old possibilities and revise them with new knowledge. Thus we get La(p ∧ q) ∧ Kap ∧ Lar. However, consider revising La(p ∧ ¬q) ∧ La(¬p ∧ ¬q) with Kaq ∧ Lar. Since all old possibilities are inconsistent with new knowledge, we revise all of them with new knowledge. The result is La(p∧q)∧La(¬p∧q)∧Kaq∧Lar. The same idea applies to the revision of common possibilities.

Motivated by Example 4, we define a "revision with carry" operator φ ◦γ φ′ where γ is the carry. The difference between φ′ and γ is that the revision result must entail φ′ while the result only need to be consistent with γ.

Definition 4.1. Let ◦ be a revision operator. The revision of φ with φ′ and carry γ, written φ ◦γ φ′ is defined as follows:

• φ ◦γ φ′ = φ ◦ φ′ , if φ ∧ γ is satisfiable;
• φ ◦γ φ′ = φ ◦ (φ′ ∧ γ), otherwise.

Similarly, we can define the "update with carry" operator.

Motivated by Example 6, we define the ∗ operator to restrict attention to consistent pairs of formulas if possible.

Definition 4.2. Φ ∗ Φ′ =

• {(φ, φ′ ) | φ ∈ Φ, φ′ ∈ Φ′ , φ ∧ φ′ is satisfiable}, if there are φ ∈ Φ and φ′ ∈ Φ′ s.t. φ ∧ φ′ is satisfiable;
• {(φ, φ′ ) | φ ∈ Φ, φ′ ∈ Φ′ }, otherwise.

Below is the formal definition of our revision operator. Item 4 needs some explanation. In order to obtain a satisfiable result, we revise different parts of the old S-term in the following order, using the ideas behind the three motivating examples:

1. When old common knowledge is consistent with new knowledge and new possibilities, revise it with new common knowledge; otherwise simply assume new common knowledge.
2. Revise knowledge using revised common knowledge.
3. Revise possibilities using revised common knowledge and knowledge.
4. Keep old common possibilities that are consistent with revised common knowledge, knowledge and possibilities.

Definition 4.3. Let φ and φ′ be in unfolded normal SDNF. The revision of φ with φ′ , written φ◦φ′ , is defined recursively:

1. When φ and φ′ are propositional formulas, φ ◦ φ′ = φ ◦s φ′ , where ◦s is Satoh [1988]'s revision operator;
2. When φ = ∨ ∆ and φ′ = ∨ ∆′ , φ ◦ φ′ = ∨{δ ◦ δ′ | (δ, δ′ ) ∈ ∆∗∆′ };
3. When φ and φ′ are normal S-terms and φ ∧ φ′ is satisfiable, φ ◦ φ′ is φ ∧ φ′ converted to a normal S-term;
4. Otherwise, φ and φ′ are normal S-terms, and φ ∧ φ′ is not satisfiable. Let φ = φ0 ∧ ∧a∈A(Kaφa ∧ LaΨa ∧ Caµa ∧ DaΛa), and φ′ = φ′0 ∧ ∧a∈A(Kaφ′a ∧ LaΨ′a ∧ Caµ′a ∧DaΛ′a ). Then φ◦φ′ = φ′′ = φ′′ 0 ∧∧a∈A(Kaφ′′ a ∧ LaΨ′′ a ∧ Caµ′′ a ∧ DaΛ′′ a ) where:
5. (a) φ′′ 0 = φ0 ◦ φ′0 ;
6. (b) If Caµa ∧ ∧b̸=a (Kbφ′b ∧LbΨ′b ) is satisfiable, µ′′ a = (µa ◦γ1 µ′a ) ∨ ∨λ′a∈Λ′a (µa ◦γ2 (µ′a ∧ λ′a )) where γ1 = Caµ′a and γ2 = Caµ′a ∧ Daλ′a ; otherwise µ′′ a = µ′a ;
7. (c) φ′′ a = (φa ◦γ1 (φ′a ∧ ∧b̸=a µ′′ b ))∨ ∨ψ′a∈Ψ′a (φa ◦γ2 (ψ′a ∧ φ′a ∧ ∧b̸=a µ′′ b )), where γ1 = Kaφ′a ∧ ∧a∈A Caµ′′ a and γ2 = Kaφ′a ∧ Laψ′a ∧ ∧a∈A Caµ′′ a ;
8. (d) Ψ′′ a = {ψ◦γψ′ | (ψ, ψ′ ) ∈ Ψa∗{φ′′ a ∧∧b̸=a µ′′ b }}∪ Ψ′a , where γ = Kaφ′′ a ∧ ∧a∈A Caµ′′ a ;
9. (e) Λ′′ a = {λ | λ ∈ Λa and Daλ ∧ ∧a∈A(Kaφ′′ a ∧ LaΨ′′ a ∧ Caµ′′ a ) is satisfiable} ∪ Λ′a .

We now state properties of our revision operator.

Definition 4.4. The set of disjunct-wise satisfiable (d-sat) normal SDNFs is inductively defined:

• A disjunction ∨ ∆ of normal S-terms is d-sat if each δ ∈ ∆ is d-sat;
• A normal S-term φ0 ∧ ∧a∈A(Kaφa ∧ LaΨa ∧ Caµa ∧ DaΛa) is d-sat if it is satisfiable and each disjunct in each φa or µa is d-sat.

Proposition 4.5. An unfolded normal S-term without D modalities φ = φ0 ∧ ∧a∈A(Kaφa ∧ LaΨa ∧ Caµa) is satisfiable if the following hold:

1. φ0 is propositionally satisfiable;
2. For all a ∈ A and for all ψa ∈ Ψa, φψa = ψa ∧ φa ∧ Kaφa ∧ ∧b̸=a µb ∧ ∧a∈A Caµa is satisfiable.

Proof. We construct a model (M,w) for φ. By Item 1, we create a world w where V (w) satisfies φ0. By Item 2, for each a ∈ A and ψa ∈ Ψa, there is a KD45Cn model (Mψa ,wψa ) satisfying φψa . We add each (Mψa ,wψa ) to M and let wRawψa . Then (M,w) is a KD45Cn model for φ after calculating the transitive and Euclidean closures.

Proposition 4.6. Let φ and φ′ be two d-sat unfolded normal SDNFs. Then φ◦φ′ is a d-sat normal SDNF, and φ◦φ′ |= φ′ . Moreover, when φ ∧ φ′ is satisfiable, φ ◦ φ′ ⇔ φ ∧ φ′ .

Proof. The conjunction property follows from Definition 4.3 Item 3 directly. Now we assume that φ ∧ φ′ is unsatisfiable.

We first prove φ ◦ φ′ |= φ′ by induction on the modal depth of φ. Let md(φ) denote the modal depth of φ. When md(φ) = 0, we consider φ′ in two cases:

• md(φ′ ) = 0. Then φ ◦s φ′ |= φ′ by Satoh's revision.

• md(φ′ ) > 0. Let φ = ∨ ∆ and φ′ = ∨ ∆′ . By Definition 4.3 Item2, φ◦φ′ = ∨{δ◦δ′ | (δ, δ′ ) ∈ ∆∗∆′ }. For each (δ, δ′ ) ∈ ∆∗∆′ , since higher-order subformulas in δ′ are directly conjoined into δ ◦ δ′ , we have δ ◦ δ′ |= δ′ . Let φ◦φ′ = ∨ ∆′′ . For each δ′′ ∈ ∆′′ , there is a δ′ ∈ ∆′ s.t. δ′′ |= δ′ . Therefore, φ ◦ φ′ |= φ′ .

When md(φ) = n + 1, we consider φ and φ′ in two cases:

• φ and φ′ are normal S-terms. Let φ′′ = φ ◦ φ′ . By Items (a), (d) and (e), we have φ′′ 0 |= φ′0 , ∧a∈A LaΨ′′ a |= ∧a∈A LaΨ′a and ∧a∈A DaΛ′′ a |= ∧a∈A DaΛ′a . By Item (b) and induction, for each agent a we have µ′′ a |= µ′a , thus ∧a∈A Caµ′′ a |= ∧a∈A Caµ′a . Similarly, by Item (c) we have ∧a∈A Kaφ′′ a |= ∧a∈A Kaφ′a . Take the conjunction of the above results, we have φ′′ |= φ′ .
• Otherwise, we follow the proof in the base case.

Let γ be a modal S-term s.t. φ′ ∧γ is d-sat and φ′′ = φ◦γφ′ . Now we prove that φ′′ and φ′′ ∧ γ are d-sat by induction on the modal depth of φ. When md(φ) = 0, φ ∧ γ is d-sat and φ ◦γ φ′ = φ ◦ φ′ . We consider φ′ in two cases:

• md(φ′ ) = 0. Then φ ◦s φ′ is d-sat by Satoh's revision.
• md(φ′ ) > 0. Let φ = ∨ ∆ and φ′ = ∨ ∆′ . We have φ◦φ′ = ∨{δ ◦ δ′ | (δ, δ′ ) ∈ ∆∗∆′ }. For each (δ, δ′ ) ∈ ∆∗∆′ , let δ = φ0 and δ′ = φ′0 ∧ ∧a∈A(Kaφ′a ∧LaΨ′a ∧ Caµ′a ∧DaΛ′a ). Thus δ◦δ′ = (φ0◦sφ′0 )∧∧a∈A(Kaφ′a ∧ LaΨ′a ∧Caµ′a ∧DaΛ′a ). Again by Satoh's revision, δ◦δ′ is d-sat. Therefore, φ′′ and φ′′ ∧ γ are d-sat.

When md(φ) = n + 1, we consider φ and φ′ in two cases:

• φ and φ′ are normal S-terms. By Item (a) and Satoh's revision, φ′′ 0 is d-sat. By Item (b) and induction, µ′′ a is dsat. By definitions of "revision with carry" and unfolded formulas, we can show that Caµ′′ a is d-sat. Similarly, we have that φ′′ a and Kaφ′′ a are d-sat. Since φ′′ a |= ∧b̸=a µ′′ b , φ′′ a ∧ ∧b̸=a µ′′ b ∧ ∧a∈A Caµ′′ a is d-sat. By Item (d) and induction, ψ′′ a ∧ φ′′ a ∧ Kaφ′′ a ∧ ∧b̸=a µ′′ b ∧ ∧a∈A Caµ′′ a is d-sat for each ψ′′ a ∈ Ψ′′ a . By Proposition 4.5 and Item (e), φ′′ is d-sat. By Definition 4.1, we can show that φ′′ ∧ γ is d-sat.
• Otherwise, we follow the proof in the base case. □

Finally, we present the formal definition of our update operator. For Item 4, the difference with that of the revision operator lies with Item (d) where we update each possibility. Recall that for Item 4 (d) of the revision operator, when there are possibilities consistent with new common knowledge and knowledge, we only keep them and revise them.

Definition 4.7. Let φ and φ′ be in unfolded normal SDNF. The update of φ with φ′ , written φ⋄φ′ , is defined recursively:

1. When φ and φ′ are propositional formulas, φ ⋄ φ′ = φ ⋄w φ′ , where ⋄w is Winslett [1988]'s update operator;
2. When φ = ∨ ∆, φ ⋄ φ′ = ∨δ∈∆ δ ⋄ φ′ ;
3. When φ is an S-term, and φ′ = ∨ ∆′ , φ ⋄ φ′ = ∨{φ ⋄ δ′ | (φ, δ′ ) ∈ {φ} ∗∆′ };
4. Otherwise, φ and φ′ are normal S-terms, φ ⋄ φ′ = φ′′ where φ, φ′ , φ′′ have the form as in Definition 4.3, and:
5. (a) φ′′ 0 = φ0 ⋄ φ′0 ;
6. (b) If Caµa ∧ ∧b̸=a (Kbφ′b ∧LbΨ′b ) is satisfiable, µ′′ a = (µa ⋄γ1 µ′a ) ∨ ∨λ′a∈Λ′a (µa ⋄γ2 (µ′a ∧ λ′a )) where γ1 = Caµ′a and γ2 = Caµ′a ∧ DaΛ′a ; otherwise µ′′ a = µ′a ;
7. (c) φ′′ a = (φa ⋄γ1 (φ′a ∧ ∧b̸=a µ′′ b ))∨ ∨ψ′a∈Ψ′a (φa ⋄γ2 (ψ′a ∧ φ′a ∧ ∧b̸=a µ′′ b )), where γ1 = Kaφ′a ∧ ∧a∈A Caµ′′ a and γ2 = Kaφ′a ∧ Laψ′a ∧ ∧a∈A Caµ′′ a ;
8. (d) Ψ′′ a = {ψ ⋄γ (φ′′ a ∧ ∧b̸=a µ′′ b ) | ψ ∈ Ψa} ∪ Ψ′a , where γ = Kaφ′′ a ∧ ∧a∈A Caµ′′ a ;
9. (e) Λ′′ a = {λ | λ ∈ Λa and Daλ ∧ ∧a∈A(Kaφ′′ a ∧ LaΨ′′ a ∧ Caµ′′ a ) is satisfiable} ∪ Λ′a .

Proposition 4.8. Let φ and φ′ be two d-sat unfolded normal SDNFs. Then φ⋄φ′ is a d-sat normal SDNF, and φ⋄φ′ |= φ′ . Moreover, (φ1 ∨ φ2) ⋄ φ′ ⇔ φ1 ⋄ φ′ ∨ φ2 ⋄ φ′ .

The distribution property can be obtained from Definition 4.7 Item 2 directly. We omit the proofs for the other properties of update since they are similar to those of revision.

5 Implementation and Experimental Results

Based on our reasoning, revision and update algorithms, we implemented a planner called MEPC for multi-agent epistemic planning with common knowledge. Our planning algorithm supports contingent planning by extending breadthfirst search to AND/OR graphs. We evaluate MEPC with five domains which use common knowledge in different ways.

Collaboration-and-Communication: CC(n). There are 4 rooms, 2 agents and n boxes. Agents can enter rooms and sense boxes in it. Also, agents can share information. The goal is to let agents know the positions of boxes. The common knowledge is that each box is in exactly one room.

Muddy-Children: MC(n,m). There are n children and m of them are muddy.

Public-Announcing: PA(n). There are n agents in room 1. Agent 1 can sense whether the book is in room 2 and take it away. Each agent can share his belief about the book to others, while agent n can make a public announcement. The goal is to achieve common knowledge that agent 1 belives the book is missing.

Selective-Communication: SC(n). There are n rooms and n agents in different rooms. A secret is false, but initially it's common knowledge that agent 1 believes the secret is true. Agent 1 can find out that the secret is false. Each agent can move to a neighboring room and tell the secret to others in the room. The goal is to let all agents except agent 1 believe that the secret is false, while agent 1 believes that it is true.

Prisoners-and-Lightbulb: PL(n). This domain is adapted from a puzzle in [van Ditmarsch and Kooi, 2015]. There are n prisoners in the prison. Every day one of them is interrogated in a room furnished with a light bulb. The goal is to let one of them know that all the prisoners have been interrogated.

Our experiments were run on a Windows machine with 3.50GHz CPU and 8GB RAM. The results are shown in Table 1. The 2nd-4th columns indicate the number of agents, the number of atoms, and the number of sensing and deterministic actions. In the last column, A-B(C/D) indicates A seconds of total time, B seconds spent on satisfiability solving, depth C of solution tree (C=0 means the problem is unsolvable), and D nodes searched. The results show that our planner is capable of solving these problems of planning with common knowledge. However, our planner doesn't scale well, due to the exponential time complexity of the satisfiability solving algorithm and the naive search method we use.

6 Conclusion

In this paper, we have extended an existing framework for multi-agent epistemic planning with the capability to deal with general common knowledge. We propose a novel normal form for multi-agent KD45 with common knowledge which makes use of the subscripted common knowledge operator and unfolds knowledge in a certain way. We propose satisfiability solving, revision and update algorithms for this normal form. We implemented a planner MEPC, and it is capable of solving several domains involving typical usage of common knowledge. Despite the current limitations of our work, we have made a significant first step towards multiagent epistemic planning with common knowledge. In the future, we are interested in extending our work to handle common knowledge of a subset of agents. Proposing more efficient algorithms for reasoning about common knowledge is another important future work.

Acknowledgments

We acknowledge support from the Natural Science Foundation of China under Grant Nos. 61572535 and 61463044.