Multi-Agent Epistemic Explanatory Diagnosis via Reasoning about Actions

1 Introduction

The task of explanatory diagnosis conjectures what actions occurred to explain observations of dynamic systems. This is a common task in real life and an essential ability of intelligent agents. For example, on a murder scene, a detective speculates on what happened based on his observations of the scene; in a factory, an engineer tries to determine the internal operation of a machine according to the external observations. Explanatory diagnosis becomes more complicated in multi-agent scenarios, since agents' actions may be partially observable to other agents, and observations might involve agents' knowledge about the world or other agents' knowledge or even common knowledge of a group of agents. In this paper, we use the words "knowledge" and "epistemic" in the broad sense.

For example, consider a simple scenario involving three persons Ann, Bob and Carl working in the same office. There is a desk in the office and each person owns a drawer of the desk. Ann has a valuable watch in her drawer, and the three persons commonly know that. The door of the office can only be opened by Ann, Bob and Carl. Ann left the office and closed the door as usual. When she comes back, she finds that, contrary to her belief, her watch is not in her drawer. Now Ann wants to know what happened.

McIlrailth [1998] presented a formal characterization of explanatory diagnosis in the language of the situation calculus, one of the most popular languages for reasoning about actions. Sohrabi et al. [2010] established a formal correspondence between explanatory diagnosis and planning, and showed how modern planning techniques can be exploited to generate explanatory diagnoses. Further, they [2011] explored generating preferred explanations via planning.

In the big picture, explanatory diagnosis is a generalization of model-based diagnosis from static systems to dynamic systems. Reiter [1987] laid an elegant theoretical foundation for model-based diagnosis, which is the task of locating faulty components of a system based on a description of the correct behavior of the system and an observation of its aberrant behavior. In control theory, a very influential work about modelbased diagnosis of dynamic systems is the one by Sympath et al. [1995] where they modeled discrete event systems as finite state automata and characterized diagnosis as a reachability analysis problem. Pencol´ e and Cordier [2005] proposed a formal framework for the decentralized diagnosis of large-scale discrete event systems. In the past decade, Grastien, Rintanen and colleagues [Rintanen and Grastien, 2007; Grastien et al., 2007] showed how the diagnosing problems of discrete event systems can be translated into the propositional satisfiability problem and solved by modern SAT solvers.

The most influential logic framework for reasoning about actions in the multi-agent case is dynamic epistemic logic (DEL) [van Ditmarsch et al., 2007]. An important concept in DEL is that of an event model, which is a Kripke model of events, representing the agents' uncertainty about the current event. By the product update operation, an event model may be used to update a Kripke model. Recently, Bolander and Anderson [2011] explored multi-agent epistemic planning based on DEL. They showed that single-agent epistemic planning is decidable, but multi-agent epistemic planning is undecidable even without common knowledge. Meanwhile, L¨owe et al. [2011] showed that for a special type of event models, multi-agent epistemic planning is decidable.

In this paper, we formalize the multi-agent epistemic explanatory diagnosis task in DEL. Since this task is undecidable in general, we identify two important decidable fragments of it by restricting our attention to propositional actions, i.e., actions whose preconditions do not involve knowledge, or purely epistemic actions, i.e., actions which do not effect world change. Our first result is that when observations do not involve common knowledge and all actions are propositional, explanatory diagnosing is decidable. Secondly, we identify a wide variety of special types of propositional purely epistemic actions, and show that when all actions are of these types, explanatory diagnosing is decidable. Our decidability results are achieved via techniques of reducing the potentially infinite search spaces to finite ones of epistemic states or action sequences.

2 Preliminaries

In this section, we present the syntax and semantics of multiagent epistemic logic, and introduce the concepts of event models and product update from dynamic epistemic logic.

2.1 Multi-agent epistemic logic

We fix a finite set A of agents and a finite set of atoms P. We use |S| for the cardinality of a set S.

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

where p ∈ P, a ∈ A, B ⊆ A, and φ, ψ ∈ LKC. We use LK for the language without the CB operator.

Definition 2.2. A frame is a structure (W, R), where

• W is a finite non-empty 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 such that wRaw′ . We say Ra is Euclidean if whenever wRaw1 and wRaw2, we have w1Raw2. A frame whose accessibility relations are equivalence relations is called an S5 frame, and a frame whose accessibility relations are transitive and Euclidean (resp. serial, transitive and Euclidean) is called a K45 (resp. KD45) frame.

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.

Definition 2.4. An epistemic state, or an e-state in short, 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.5. Let s = (M, w) be an epistemic state 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 |= CBφ iff for all v s.t. wRBv, M, v |= φ, where RB is the transitive closure of the union of Ra for a ∈ B.

Example 1. Consider the watch example. We use pa, pb and pc to denote that the watch is in Ann's, Bob's and Carl's drawer, respectively, and pd to denote that the watch is on the surface of the desk. Then the initial e-state is s0 where there is only one world w0, V (w0) = {pa}, and all accessibility relations are reflexive. Then we have s0 |= C{a,b,c}pa, i.e., all agents commonly know that the watch is in Ann's drawer.

2.2 Event models and product update

Event models and product update are two important concepts of dynamic epistemic logic. Intuitively, an event model is a Kripke model of events, representing the agents' uncertainty about the current event.

Definition 2.6. An event model is a tuple

• (E,→) is a frame, and an e ∈ E is called an event;
• For each e ∈ E, pre(e) ∈ LKC is its precondition;
• For each e ∈ E, post(e) is its postcondition, and it is in the form of a conjunction of atoms or their negations.

Suppose P = {p, q, r} and post(e) = p ∧ ¬q. It means that the execution of e makes p true, q false, and r unchanged.

We let e⊤ denote a special event such that pre(e⊤) = post(e⊤) = true. Intuitively, e⊤ means nothing happens.

Note that the above definition of post(e) follows that in [Bolander and Andersen, 2011]. This form of postconditions is restrictive in that it can only represent context-free actions. Usually, post(e) is defined as a mapping from P to LKC, and this general form of postconditions can represent context-dependent or context-sensitive actions such as flipping a switch. As shown by Van Ditmarsch and Kooi [2008], for any event model E with general postconditions, we can construct an equivalent event model E ′ as defined in Definition 2.6. However, the number of events in E ′ is 2n times the number of events in E, where n = |P|.

Definition 2.7. An action is a tuple α=(E, e, actr, cost), where

• E is an event model;
• e ∈ E is the actual event;
• For each e ∈ E, actr(e) ∈ A is the performer of e;
• For each e ∈ E, cost(e), a real number, is the cost of e.

We often omit the actr and cost parts of an action.

Example 2. Consider the watch example. To describe the scenario that Bob moves the watch from Ann's drawer to the surface of the desk while Ann is away, we use action α1 = (E1, e1, actr, cost) where E1 = (E, →, pre, post), and

• E = {e⊤, e1}, pre(e1) = pa, post(e1) = ¬pa ∧ pd,
• →a= {(e1, e⊤), (e⊤, e⊤)}, →b and →c are identities,
• actr(e⊤)=actr(e1)=b, cost(e⊤)=0, cost(e1)=1.

Intuitively, e1 is the event of moving the watch and e1 is the actual event, e1 is observable to Bob and Carl but not to Ann. We illustrate E1 and α1 with Figure 1 where we use a solid dot to represent the actual event.

Below we define the product update operation.

Definition 2.8. Given an epistemic state s = (M, w) and an action α = (E, e), α is applicable in s if M, w |= pre(e).

Definition 2.9. Given an e-state s = (M, w) and an action α = (E , e), where M =(W, R, V ) and E =(E, →, pre, post), when α is applicable in s, the product of s and α, denoted by s⊗α, is a new e-state s′ = (M ′ , w′ ), where M ′ = M ⊗E = (W ′ , R′ , V ′ ), w′ = (w, e), and

• W ′ = {(w, e) ∈ W × E | M, w |= pre(e)};
• (w, e)R′a (w′ , e′ ) iff wRaw′ and e →a e′ ;
• For each (w, e) ∈ W ′ , V ′ ((w, e)) = {p ∈ P | p ∈ V (w) and post(e) ̸|= ¬p, or post(e) |= p}.

Intuitively, (w, e) is the world resulting from doing e in w.

Example 3. Consider the e-state s0 from Example 1 and the action α1 from Example 2. Since s0 |= pa, α1 is applicable in s0. The update of s0 by α1, s0⊗α1, is a new e-state s1 where there are two worlds: (w0, e⊤) and (w0, e1), V ((w0, e⊤)) = {pa}, V ((w0, e1)) = {pd}, and the accessibility relations are inherited from those of α1. This is illustrated with Figure 2.

Definition 2.10. Let s be an e-state, and σ = α1 . . . αn an action sequence. We define si, i ≤ n as follows: s0 = s; for i < n, if si is defined and αi+1 is applicable in si, then si+1 = si ⊗ αi+1, otherwise si+1 is undefined. If sn is defined, we say that σ is applicable in s and define s ⊗ σ = sn.

Finally, we introduce different types of event models from the DEL literature, and we say an action is of type X if its event model is of type X.

Definition 2.11. An event model is public if it has a single event and all accessibility relations are reflexive.

So there is a single event point, observable to all agents.

Definition 2.12. An event model is (purely) epistemic if all postconditions are true. Hence we omit the post part.

So an epistemic event model doesn't change the world.

Definition 2.13. An event model is propositional if all preconditions are propositional formulas.

So all preconditions only depend on the world state.

Definition 2.14. An event model is globally deterministic if all preconditions are pairwise inconsistent, i.e., whenever e and e′ are different, pre(e) and pre(e′ ) are inconsistent.

Intuitively, in any world, at most one event can happen.

Definition 2.15. A sensing event model is a globally deterministic epistemic event model where the preconditions are collectively exhaustive, i.e., the disjunction of all preconditions is a valid formula.

Definition 2.16. A secret communication event model is an epistemic event model ({e, e⊤},→, pre), where there exists a subset B of A such that for all a ∈ B, →a is identity, and for all a ̸∈ B, →a= {e, e⊤} × {e⊤}.

So agents in B are aware that φ = pre(e) is communicated, but others think that nothing happens. This definition corresponds to the group update program UB?φ in Gerbrandy's PhD thesis [1999].

3 Multi-agent epistemic explanatory diagnosis

In this section, we present the formal definition of multi-agent epistemic explanatory diagnosis, and propose several criteria for preferred diagnoses.

Definition 3.1. A diagnosis problem is a tuple P = (∆, s0, φo), where ∆ is a finite set of actions, s0 is the initial epistemic state, and φo ∈ LKC is the observation.

Definition 3.2. An explanatory diagnosis for a diagnosis problem P = (∆, s0, φo) is a finite sequence σ of actions from ∆ such that σ is applicable in s0, and s0 ⊗ σ |= φo.

Thus σ is an explanatory diagnosis if in s0, it is possible to execute the actions in σ one by one, and in the resulting epistemic state, the observation holds.

Example 4. The diagnosis problem for the watch example is P = (∆, s0, φo), where φo = ¬pa ∧ Kapa, s0 is from Example 1, and we let ∆ be the set of the following actions:

• α1 (α2): Bob (Carl) moves the watch fromAnn's drawer to the surface of the desk (while Ann is away);
• α3 (α4): Bob (Carl) moves the watch from the surface of the desk to Ann's drawer (while Ann is away);
• α5 (α6): Bob (Carl) moves the watch from the surface of the desk to Bob's (Carl's) drawer (while Ann is away);

Then the following are some solutions for P:

σ1 = α1α5, σ2 = α1α3α1α5, σ3 = α1α3α2α6. Figure 3 illustrates the evolution of e-states as the sequence α1α5 is performed. Clearly, s2 |= ¬pa ∧Kapa.

As we can see from the above example, for a diagnosis problem, there might very well be many explanatory diagnoses, and there is a need to distinguish between diagnoses of different quality. In all cases, we would prefer diagnoses which avoid conjecturing actions which do not account for the observation. In addition, there may be domain-specific information which we would like to consider in determining preferred diagnoses.

Definition 3.3. Let ≺ be a preference relation between diagnoses. Given a diagnosis problem P, σ is a preferred diagnosis for P if σ is a diagnosis for P and there does not exist another diagnosis σ′ for P such that σ′ ≺ σ.

Next, we propose three domain-independent preference criteria for diagnoses. In many situations, the most important criterion is the length of the diagnosis. There are two other useful criteria: one prefers diagnoses involving fewer agents, and the other prefers diagnoses of lower-cost.

To formalize these criteria, we introduce some notation. Let σ be a finite sequence of actions α1 . . . αn, where αi = (Ei, ei, actri, costi), i = 1, . . . , n. We use ‖σ‖ to denote the length of the sequence σ. We define actrs(σ) as the set {actri(ei) | i = 1, . . . , n}, and cost(σ) as Σni=1 costi(ei).

Definition 3.4. Given a diagnosis problem P and two diagnoses σ1 and σ2 for it,

1. σ1 is preferred to σ2 wrt length if ‖σ1‖ < ‖σ2‖;
2. σ1 is preferred to σ2 wrt simplicity if |actrs(σ1)| < |actrs(σ2)|;
3. σ1 is preferred to σ2 wrt cost if cost(σ1) < cost(σ2).

Considering Example 4, we have: σ1 is preferred to σ2 and σ3 wrt length; σ1 and σ2 are preferred to σ3 wrt simplicity.

From our definition, it is easy to see that computing an explanatory diagnosis is analogous to generating a plan to achieve a goal. However, there is a difference between explanatory diagnosis and planning. In planning, a goal might not be achievable. But in diagnosis, an observation is a property of the current e-state, which results from the initial e-state by the execution of a sequence of actions. So if a diagnosis problem is correctly specified, a solution always exists. But a diagnosis problem might be incorrectly specified and if so, a solution may not exist. In this paper, we study the decidability issue of the following problem:

Definition 3.5. The explanatory diagnosing problem is to decide if a given diagnosis problem has a solution.

In fact, our definition of explanatory diagnoses is the same as that of epistemic planning solutions by Bolander and Anderson [2011] except that they use local epistemic states. A local epistemic state for agent a is a pair (M,Wa), where M = (W, R, V ) is a Kripke model, and Wa ⊆ W is closed under Ra, i.e., if w ∈ Wa and wRaw′ , then w′ ∈ Wa. They showed that multi-agent epistemic planning is undecidable even without common knowledge. So in general, explanatory diagnosing is undecidable. In the next two sections, we identify important decidable fragments of the problem.

4 A decidability result in the absence of common knowledge

In this section, we present our result that in the absence of common knowledge, when we only allow propositional actions, explanatory diagnosing is decidable. Our result is inspired by two decidability results from [Bolander and Andersen, 2011] concerning multi-agent epistemic planning. So we introduce their results first.

The basic idea of their results is this. Given a multi-agent epistemic planning problem, we perform a search in the space of e-states. In general, this is an infinite search space. Under conditions ensuring that the number of non-isomorphic e-states is finite, planning is decidable. Better yet, under conditions guaranteeing that the number of non-equivalent estates is finite, planning is also decidable. In the following, we rephrase their results in the context of explanatory diagnosis, and briefly present the proofs.

Proposition 4.1. Given a natural number n, the number of non-isomorphic e-states with exactly n worlds is ≤ n · 2n2 .

Theorem 4.2. Explanatory diagnosing is decidable when only globally deterministic actions are allowed.

Proof. Given such a diagnosis problem, we perform a search in the space of e-states. For a globally deterministic event model, in any world, at most one event can happen. Hence when we update an e-state by an action, the number of worlds won't increase. Suppose that the initial e-state has n worlds. Then any possible e-state has no more than n worlds. By Proposition 4.1, the e-state space is finite.

Examples of globally deterministic actions are public actions and sensing actions.

We now introduce the well-known concept of bisimulation, which is needed in the rest of this paper. For a reference on modal logic, see for example [Blackburn et al., 2002].

Definition 4.3. Let s = (M,w) and s′ = (M ′ ,w′ ) be two e-states, where M = (W, R, V ) and M ′ = (W ′ , R′ , V ′ ). A bisimulation between s and s′ is a relation ρ ⊆ W ×W ′ s.t. wρw′ , and whenever uρu′ , V (u) = V ′ (u′ ), and

• The forth condition: for all agents a ∈ A, if uRav, then there is v′ (called the forth witness) s.t. u′R′a v′ and vρv′ ;
• The back condition: for all agents a∈A, if u′R′a v′ , then there is v (called the back witness) s.t. uRav and vρv′ .

We say that s and s′ are bisimilar, written s↔s′ , if there is a bisimulation relation between s and s′ .

A nice property of bisimilar epistemic states is that they agree on all epistemic formulas:

Proposition 4.4. Let s and s′ be two epistemic states s.t. s↔s′ . Then for any φ ∈ LKC, s |= φ iff s′ |= φ.

Let M = (W, R, V ) be a Kripke model. We can define an equivalence relation on W as follows: w↔v iff M, w↔M, v. Then we can construct the quotient structure of M wrt ↔, which turns out to be bisimilar toM.

Definition 4.5. Given a Kripke model M = (W,R, V ), the bisimulation contraction of M is the quotient structure M↔ = (W ′ , R′ , V ′ ), where

• W ′ = {[w]↔ | w ∈ W}, here [w]↔ = {v ∈ W | (M, w)↔(M, v)};
• For all agents a ∈ A, [w]↔R′a [v]↔ iff there are w′ ∈ [w]↔ and v′ ∈ [v]↔ such that w′Rav′ ;
• For all w ∈ W, V ′ ([w]↔) = V (w).

Proposition 4.6. (M↔, [w]↔)↔(M,w).

We are now ready to present the second result.

Proposition 4.7. In the single-agent case, the number of nonbisimilar S5, KD45 or K45 e-states is ≤2n·22n , here n=|P|.

Proof. In the single-agent case, it is easy to show: (1) Each S5 e-state is bisimilar to an e-state s = ((W, R, V ), w), where R = W ×W, and V is an injection. (2) Each KD45 or K45 e-state is bisimilar to an e-state s = (({w} ∪W,R, V ),w), where W ̸= ∅ in the case of KD45, R = ({w} ∪ W) ×W, and the restriction of V to W is an injection.

Theorem4.8. Single-agent explanatory diagnosing is decidable when the frames are all S5, all KD45, or all K45.

Proof. It is easy to show that bisimilarity of e-states is preserved under product update. So by Propositions 4.4 and 4.6, when we perform search of the e-state space, we can replace each e-state by its bisimulation contraction. By Proposition 4.7, we get a finite search space.

Now we proceed to present our result. Theorem 4.8 holds because there are a finite number of non-bisimilar e-states, which does not hold in the multi-agent case. However, if the observations do not contain common knowledge, a weak notion of bisimilarity would suffice. Below we present the definition of k-bisimulation and the property that two kbisimilar e-states agree on all formulas of LK with modal depth bounded by k from [Blackburn et al., 2002]. We will show that the k-bisimulation contraction of a Kripke model is k-bisimilar to itself, there are a finite number of non-kbisimilar e-states, and k-bisimilarity is preserved under update by propositional actions. With these results, we can show that explanatory diagnosing is decidable when observations do not contain common knowledge and only propositional actions are allowed.

Definition 4.9. Let s = (M,w) and s′ = (M ′ ,w′ ) be two e-states, where M = (W, R, V ) and M ′ = (W ′ , R′ , V ′ ). We say that s and s′ are k-bisimilar, written s↔k s′ , if V (w) = V ′ (w′ ), and either k = 0 or the following conditions hold:

• The forth condition: for all agents a ∈ A, if wRav, then there is v′ s.t. w′R′a v′ and (M, v)↔k-1 (M ′ , v′ );
• The back condition: for all agents a ∈ A, if w′R′a v′ , then there is v s.t. wRav and (M, v)↔k-1 (M ′ , v′ ).

Clearly, for any k ≥ 0, if s↔k+1 s′ , then s↔k s′ .

The modal depth of a formula φ, denoted by md(φ), is the depth of nesting of modal operators in φ.

Proposition 4.10. Let s and s′ be two e-states s.t. s↔k s′ . Then for any φ ∈ LK s.t. md(φ) ≤ k, s |= φ iff s′ |= φ.

Following the idea of bisimulation contraction, we define:

Definition 4.11. The k-bisimulation contraction of a Kripke model M is the quotient structure of M wrt the ↔k relation.

The proposition below shows that the k-bisimulation contraction of a Kripke model M is k-bisimilar to M itself.

Proposition 4.12. Let (M,w) be an e-state. Then for any j, k such that j ≥ k ≥ 0, (M↔j , [w]↔j )↔k (M, w).

Proof. Let M = (W,R, V ). To simplify the notation, we denote M↔j by Mj, and [w]↔j by [w]j. We prove by induction on k. The base case is obvious. Assume that the statement holds for k. Then by transitivity of ↔k , we have for any j1, j2 ≥ k, (Mj1 , [w]j1 )↔k (Mj2 , [w]j2 ). We prove that the statement holds for k + 1. Let j ≥ k + 1. Let Mj = (W ′ ,R′ , V ′ ). First, V ′ ([w]j) = V (w). (1) Suppose wRav. Then [w]jR′a [v]j. By induction hypothesis, (Mj, [v]j)↔k (M, v). (2) Suppose [w]jR′a [v]j. Then there are w∗ ∈ [w]j and v∗ ∈ [v]j s.t. w∗Rav∗ . Since (M,w)↔j (M,w∗ ), there is v′ s.t. wRav′ and (M, v′ )↔j-1 (M, v∗ ). Since (M, v)↔j (M, v∗ ), (M, v)↔j-1 (M, v∗ ). So (M, v)↔j-1 (M, v′ ), hence [v]j-1 = [v′ ]j-1. By induction hypothesis, (Mj-1, [v′ ]j-1)↔k (M, v′ ), and (Mj, [v]j)↔k (Mj-1, [v]j-1). Since [v]j-1 = [v′ ]j-1, we have (Mj, [v]j)↔k (M, v′ ). Thus, (Mj, [w]j)↔k+1 (M,w).

Visser [1996] showed that in the single-agent case, the number of ↔k equivalence classes of any Kripke model is bounded by a number which only depends on k. In the following, we extend his result to the multi-agent case:

Proposition 4.13. Let M be a Kripke model. We use Fk(M) to denote the number of ↔k equivalence classes of worlds of M. Suppose |A| = m and |P| = n. Let f(0) = 2n , and f(i + 1) = 2mf(i)+n for i ≥ 0. Then Fk(M) ≤ f(k).

Proof. Let M = (W,R, V ). We prove by induction on k. Base case: k = 0. For any w1, w2 ∈ W, if V (w1) = V (w2), then M,w1↔0M,w2. There are at most 2n different possibilities for V (w),w ∈ W. Thus F0(M) ≤ 2n = f(0). Inductive step: Assume that the statement holds for k. We prove that it holds for k + 1. For any w ∈ W, a ∈ A, let Ra(w) denote the set {[w′ ]↔k | wRaw′}. Then we have: for any w1,w2 ∈ W, if V (w1) = V (w2) and Ra(w1) = Ra(w2) for all a ∈ A, then (M,w1)↔k+1 (M,w2). For each a ∈ A, there are at most 2Fk(M) different possibilities for Ra(w). So Fk+1(M) ≤ 2n · (2Fk(M) )m ≤ 2mf(k)+n = f(k + 1).

The next proposition states that k-bisimilarity between estates is preserved under update by propositional actions.

Proposition 4.14. Let s = (M, w) and s′ = (M ′ , w′ ) be two e-states such that s↔k s′ . Let α = (E, e) be a propositional action. Then α is applicable in s iff α is applicable in s′ ; and if α is applicable in s, then s ⊗ α↔k s′ ⊗ α.

Proof. Let M = (W,R, V ), M ′ = (W ′ ,R′ , V ′ ), and E = (E,→, pre, post). Since (M,w)↔k (M ′ ,w′ ), V (w) = V ′ (w′ ). Since pre(e) is propositional, M,w |= pre(e) iff M ′ ,w′ |= pre(e). Hence α is applicable in s iff α is applicable in s′ . Now suppose α is applicable in s. Let M ⊗ E =(W ∗ , R∗ , V ∗ ) and M ′ ⊗E = (W ′∗ , R′∗ , V ′∗ ). We prove s⊗α↔k s′ ⊗α by induction on k. Since (M, w)↔0 (M ′ , w′ ), V (w) = V ′ (w′ ). So V ∗ ((w, e)) = V ′∗ ((w′ , e)). So we have proved the base case: k = 0. Induction step: Assume that the statement holds for k. We prove that it also holds for k + 1. We first prove the forth condition. Suppose (w1, e1) ∈ W ∗ and (w, e)R∗a (w1, e1). Then M,w1 |= pre(e1), wRaw1 and e →a e1. Since (M,w)↔k+1 (M ′ ,w′ ), there exists w′1 such that w′Raw′1 and (M,w1)↔k (M ′ ,w′1 ). By induction hypothesis, M ⊗ E, (w1, e1)↔kM ′ ⊗ E, (w′1 , e1). Meanwhile, (w′ , e)R′∗ a (w′1 , e1). The back condition can be similarly proved. Thus, M ⊗ E, (w, e)↔k+1M ′ ⊗ E, (w′ , e).

It is important to note that without the restriction to propositional actions, Proposition 4.14 does not hold. We illustrate this with the following example:

Example 5. Let A = {a} and P = {p}. Figure 4 illustrates two e-states s1 and s2, action α, and the two e-states s1 ⊗ α and s2 ⊗ α. Here α has a single event e with pre(e) = Kap. s2 ⊗α has a single state (v, e), since e is not executable in v1 or v2. Clearly, s1↔1 s2, but not s1 ⊗α↔1 s2 ⊗α.

We are now ready to present the main result of this section:

Theorem 4.15. Explanatory diagnosing is decidable when observations are in LK and all actions are propositional.

Proof. Let P = (∆, s0, φo) be such a diagnosis problem. Let k = md(φo). By Propositions 4.10 and 4.12, any e-state s and its k-bisimulation contraction are k-bisimilar and hence agree on φo. By Proposition 4.14, k-bisimularity is preserved under update by propositional actions. Thus, when we perform search of the e-state space, we can replace each e-sate by its k-bisimulation contraction. By Propositions 4.13 and 4.1, there are only finitely many non-isomorphic k-bisimulation contractions. So we get a finite search space.

5 A decidability result in the presence of common knowledge

In this section, we present a decidability result of the explanatory diagnosing problem in the presence of common knowledge where we allow only propositional epistemic actions. We will use PE to abbreviate for "propositional epistemic". Our result is inspired by the work of L¨owe et al. [2011], which we introduce first.

L¨owe et al. identified two important properties of event models, defined as follows:

Definition 5.1. Two actions α1 and α2 commute if for all e-states s, we have (s ⊗ α1) ⊗ α2↔(s ⊗ α2) ⊗ α1.

Let α be an action, and n ≥ 1. We use αn to denote the sequence consisting of exactly n α's.

Definition 5.2. An action α is called self-absorbing if for all e-states s, s ⊗ α2↔s ⊗ α.

If all actions are self-absorbing and commute, then multiagent epistemic planning is decidable, since we can reduce the search space of action sequences to the finite space of action sequences where each action appears at most once. They showed that PE actions commute and identified a special type of PE actions which are self-absorbing.

Proposition 5.3. Propositional epistemic actions commute.

Definition 5.4. An epistemic event model E = (E,→, pre) is almost-mutex if e⊤ ∈ E, e⊤ →a e⊤ for all a ∈ A, and the formulas pre(e) with e ̸= e⊤ are pairwise inconsistent.

Definition 5.5. A propositional epistemic event model is called almost-mutex transitive if it is almost-mutex and all accessibility relations are transitive.

Proposition 5.6. Almost-mutex transitive propositional epistemic actions are self-absorbing.

In the following, we will identify a wide variety of special types of PE actions, and show that any action α of these types is self-absorbing in the general sense, i.e., there exists a number n which depends only on α, such that for any e-state s, we have s⊗αn+1↔s⊗αn . Thus we will be able to show that explanatory diagnosing is decidable when only these types of PE actions are allowed.

We first state a simple property of PE actions:

Proposition 5.7. Let s = (M, w0) be an e-state where M = (W, R, V ), and α = (E, e0) a propositional epistemic action where E = (E,→, pre). Suppose that αn is applicable in s. Then for any w ∈ W, any τ = (e1, . . . , en) ∈ En , (w, τ) is a world of s ⊗ αn iff w |= pre(τ), where pre(τ) denotes pre(e1) ∧ . . . ∧ pre(en).

It is easy to prove the following:

Proposition 5.8. Public propositional epistemic actions are self-absorbing.

Definition 5.9. An epistemic event model E = (E,→, pre) is possibly oblivious if e⊤ ∈ E, and for all e ∈ E and all a ∈ A, e →a e⊤.

Intuitively, a possibly oblivious event model is one where when any event happens, any agent thinks it is possible that nothing happens. It might be strange that the performer of the event also thinks it is possible that nothing happens. But this is the case for fallible events.

Proposition 5.10. Possibly oblivious propositional epistemic actions are self-absorbing.

Proof. Let α = (E, e0) be a possibly oblivious PE action where E = (E,→, pre). Let s = (M,w0) be an e-state where M = (W, R, V ). We show that s ⊗ α2↔s ⊗ α. Let M ⊗ E = M ′ = (W ′ ,R′ , V ′ ) and M ′ ⊗ E = M ′′ = (W ′′ ,R′′ , V ′′ ). We define ρ ⊆ W ′′ × W ′ as follows: ρ = {((w, e1, e2), (w, e)) | e = e1 or e = e2}. We show that ρ is a bisimulation between s ⊗ α2 and s ⊗ α. First, (w0, e0, e0)ρ(w0, e0). Now suppose ((w, e1, e2), (w, e)) ∈

ρ. Since E is epistemic, we have V ′ ((w, e)) = V (w) = V ′′ ((w, e1, e2)). Suppose (w, e1, e2)R′′ a (w′ , e′1 , e′2 ). Since (w′ , e′1 , e′2 ) ∈ W ′′ , we have w′ |= pre(e′1 ) ∧ pre(e′2 ). If e = e1, let e′ = e′1 , else let e′ = e′2 . Then (w′ , e′ ) is the forth witness. Suppose (w, e)R′a (w′ , e′ ). Since E is possibly oblivious, e⊤ ∈ E, and for all e ∈ E, e →a e⊤. If e = e1, let e′1 = e′ and e′2 = e⊤, else let e′1 = e⊤ and e′2 = e′ . Then (w′ , e′1 , e′2 ) is the back witness.

Definition 5.11. A binary relation R is functional dependent if whenever xRy and xRz, we have y = z. An event model is called functional dependent if all accessibility relations are. Intuitively, a functional dependent event model is one where when any event happens, any agent is certain but may be mistaken about the current event. An example of such event models is secret communication.

Definition 5.12. An event model is binary if it has exactly two events.

An example of binary event models is binary sensing.

Definition 5.13. A binary relation R is divergent if every element is related to at least two distinct elements. An event model is triple dichotomous if it has exactly three events and every accessibility relation is either functional dependent or divergent.

Intuitively, a triple dichotomous event model is one where there are only two types of agents: the first is certain about the current event when any event happens, and the second is uncertain about the current event when any event happens.

Proposition 5.14. Let α = (E, e0) be a propositional epistemic action which is functional dependent, or binary, or triple dichotomous. Let n be the number of events in E. Then for all e-states s, s ⊗ αn+1↔s ⊗ αn .

Proof. Let E = (E,→, pre). Let s = (M,w0) be an e-state where M = (W,R, V ). Let M ⊗ E n = (W ′ ,R′ , V ′ ) and M ⊗ E n+1 = (W ′′ ,R′′ , V ′′ ). We define ρ ⊆ W ′′ × W ′ as follows: ρ = {((w, τ1), (w, τ2)) | set(τ1) = set(τ2)}, where set(τ) is the set of elements occurring in τ. We show that ρ is a bisimulation between s ⊗ αn+1 and s ⊗ αn . First, (w0, en+1 0 )ρ(w0, en0 ). Now suppose ((w, τ1), (w, τ2)) ∈ ρ. Since E is epistemic, V ′′ ((w, τ1)) = V (w) = V ′ ((w, τ2)). Let τ1 = (e1, . . . , en, en+1). Since |E| = n and set(τ1) = set(τ2), there exist i, j s.t. 1 ≤ i ≤ j ≤ n + 1, ei = ej, and τ2 is obtained from τ1 by removing ei and possibly permuting the other elements. Since E is propositional epistemic, the order of events does not matter. Without loss of generality, assume that en = en+1 and τ2 = (e1, . . . , en). Suppose (w, τ2)R′a (w′ , τ ′2 ) where τ ′2 = (e′1 , . . . , e′n ). Let τ ′1 = (e′1 , . . . , e′n , e′n ). Since (w′ , τ ′2 ) ∈ W ′ , w′ |= pre(τ ′2 ), hence w′ |= pre(τ ′1 ), so (w′ , τ ′1 ) ∈ W ′′ . Then (w′ , τ ′1 ) is the back witness. Finally, suppose (w, τ1)R′′ a (w′ , τ ′1 ) where τ ′1 = (e′1 , . . . , e′n , e′n+1 ). We show there is τ ′2 so that (w′ , τ ′2 ) is the forth witness. We consider three cases: (1) E is functional dependent. Since en = en+1, en →a e′n , and en+1 →a e′n+1 , we have e′n = e′n+1 . We let τ ′2 = (e′1 , . . . , e′n ).

(2) E is binary. So n = 2. If e′2 = e′3 , the proof is the same as in (1). Otherwise, e′2 ̸= e′3 . Since n = 2, e′1 = e′2 or e′1 = e′3 . If e′1 = e′2 , let τ ′2 = (e′1 , e′3 ), else let τ ′2 = (e′1 , e′2 ).

(3) E is triple dichotomous, so n = 3. If e′3 = e′4 , the proof is the same as in (1). Otherwise, e′3 ̸= e′4 , so →a is divergent. Since n = 3, e2 →a e′3 or e2 →a e′4 . If e2 →a e′3 , we let τ ′2 = (e′1 , e′3 , e′4 ), otherwise let τ ′2 = (e′1 , e′4 , e′3 ).

We now present the main result of this section.

Theorem 5.15. Explanatory diagnosing is decidable when only the following types of propositional epistemic actions are allowed: public, almost-mutex transitive, possibly oblivious, functional dependent, binary, and triple dichotomous.

Proof. Give a diagnosis problem, we perform a search in the space of action sequences. Note that bisimilar e-states agree on all formulas of LKC. By Proposition 5.3, PE actions commute. So we can restrict the search space to sequences of powers of different actions, i.e., sequences of the form: αk1 1 . . . αkn n , where for any i ̸= j, αi ̸= αj. By Propositions 5.6, 5.8, 5.10, and 5.14, we can further restrict the search space so that each power ki is bounded by 1 if the action αi is almost-mutex transitive or possibly oblivious, or by n where n is the number of events in the action. Since there are only finitely many actions, we get a finite search space.

So we have shown that for a wide range of propositional epistemic actions, explanatory diagnosing is decidable in the presence of common knowledge.

6 Conclusions

Explanatory diagnosis is a common task in real life and an essential ability of intelligent agents. In this paper, we have formally defined multi-agent epistemic explanatory diagnosis in the framework of dynamic epistemic logic. Since explanatory diagnosing is undecidable in general, we identify important decidable fragments of it. Our first result is that when observations do not contain common knowledge and all actions are propositional, explanatory diagnosing is decidable. Our second result is that in the presence of common knowledge, for a wide range of propositional epistemic actions, explanatory diagnosing is decidable. We would like to remark that these results carry over to multi-agent epistemic planning. There are also two results inherited from the literature: the first is that explanatory diagnosing is decidable when all actions are globally deterministic; the other is that single-agent explanatory diagnosing is decidable when the frames are all S5, all KD45, or all K45. For the future, we would like to identify decidable fragments of explanatory diagnosing that go beyond propositional actions, investigate the computational complexity of explanatory diagnosing for the decidable fragments we have identified, implement multi-agent explanatory diagnosis solver, and apply it to multi-agent high-level program execution.

Acknowledgments

We thank the anonymous reviewers for helpful comments. This work was supported by the Natural Science Foundation of China under Grant No. 61073053. The first author was also supported by the Natural Science Foundation of Guizhou Province, China under Grant No. [2012]2310.