Solving Strong-Fault Diagnostic Models by Model Relaxation

1 Modeling for Diagnostic Inference

Model-based diagnosis (MBD), as formulated in terms of logic [Reiter, 1987], focuses on determining whether an assignment of failure status to a set of mode-variables is consistent with a system description and an observation (e.g., of sensor values). Hence, the diagnostic process consists of taking an observation OBS, and then inferring the failure-mode assignment (diagnosis) consistent with OBS.

Within MBD, two broad classes of model types have been specified: weak-fault models WFM [de Kleer et al., 1992] and strong-fault models SFM [Struss and Dressler, 1989]. Traditionally, WFM has been considered to be computationally simple, and SFM computationally hard. Weakfault models describe a system only in terms of its normal (non-faulty) behaviour, whereas strong-fault models include a definition of some aspects of abnormal behaviour. Strongfault models can avoid violating physical rules (cf. [Struss and Dressler, 1989]), but at the cost of increased complexity: moving from a binary-valued model with n components (which is adequate for weak-fault models) to one with m+ 1

possible faulty values increases the maximum number of failure candidates from 2n to (m+ 1)n .

In terms of worst-case complexity, finding the first minimal diagnosis for a Horn model in WFM can be done in polynomial time, but finding the next minimal diagnosis is NP-complete [Friedrich et al., 1990]. In contrast, inference in strong-fault models entails computing kernel diagnoses [de Kleer et al., 1992], which is a ΣP2 -hard task and is known to be computationally intensive in practice; for example, kernel diagnoses are given by the prime implicants of the minimal conflicts [de Kleer et al., 1992]. Further, the average case complexity of reasoning in WFM versus SFM increases from poly-time in n (WFM) to exponential in n (SFM) [de Kleer et al., 1992].

Given this intractability associated with inference using SFM, we show that, by closer examination of SFM, there is a spectrum of model types, and corresponding inference complexities. We identify two main categories of SFM, which we call literal-based SFM, lSFM, and function-based SFM, fSFM, and show that lSFMhas the same properties (including inference complexity) asWFM, whereas fSFMhas the properties traditionally assigned to SFM.

This paper is the first detailed analysis of SFM, to our knowledge, which exploits model structure for computational advantage. It demonstrates the spectrum of fault modeling choices available to the system designer, and the computational implications such choices impose on the resulting diagnostic inference.

We propose a SFM algorithm that: (1) decomposes a strong-fault model into strong and weak sub-models; (2) computes diagnoses first in the "relaxed" weak sub-model; and then (3) discards any diagnosis which is not also a diagnosis in the strong sub-model. We identify classes of SFM in which the SFM diagnosis verification (step 3 above) can be done efficiently. Using ISCAS85 benchmark circuits, we have empirically demonstrated that: (1) our algorithm reduces the diagnosis computation time in CDA∗ by up to a factor of 8; and (2) the average LTMS conflict size decreases (at the price of an extra consistency check, which has lowpolynomial or better time-complexity for several classes of propositional strong-fault models).

2 RelatedWork

One of the key elements of our approach is decomposing a strong-fault model into strong and weak sub-models, and then computing diagnoses first in the "relaxed" weak sub-model, and efficiently verifying if this diagnosis is also a diagnosis in the strong sub-model.

Mozetiˇc and Holzbaur [1994] have proposed a related approach: their diagnostic engine, IDA, computes diagnoses first with a structural model, which specifies the topological connections of components in the model. This model enables propagation of input values to components to output values, given that the component is OK, and is strictly less expressive than either weak- or strong-fault models. Given any diagnoses computed in a structural model, they are then verified by the weak fault-model, and finally the resulting minimal diagnoses are verified by the strong-fault model.

In contrast to Mozetiˇc and Holzbaur, who relax models into an abstract structural relation, we relax models by partitioning the model into weak and strong sub-models, and then verifying the diagnoses of the weak sub-model by the strong sub-model (exploiting the efficient satisfiability of particular classes of strong sub-model, such as lSFM). Furthermore, our work differs in that they make assumptions on the underlying MBD engines, incrementally updating the underlying conflict set, a step which is not necessary in our approach. In contrast to IDA, our relaxation scheme and algorithm are completely orthogonal to the diagnostic engine.

Our work also bears some relation to work on abstraction of propositional knowledge bases, e.g., [Selman and Kautz, 1996; del Val, 2000]. However, rather than relax a model to a Horn approximation, we relax a strong-fault diagnostic model to a more tractable sub-model, the weak-fault model.

This paper also characterises strong-fault models. In contrast to previous work discussing strong fault models, e.g., [Console and Torasso, 1991; Mozetiˇc and Holzbaur, 1994; Struss and Dressler, 1989], we propose tractable sub-classes of strong-fault models that occur in practice, such as stuck-at circuit models.

Maier and Sachenbacher [2008] propose a general abstraction approach within the framework of constraint optimization. This approach is orthogonal to ours, in that it adaptively abstracts constraints to control the memory requirements of message-passing algorithms within a tree-decomposition framework, whereas we abstract the model prior to any inference, independent of any particular inference algorithm. It is possible to combine these two approaches, which is a topic of future work.

Strong-fault model relaxation is related to hierarchical abstraction [Chittaro and Ranon, 2004]. Due to the bad worstcase computational complexity of diagnosis, hierarchical diagnosis is often necessary, and strong-fault model relaxation can be applied at each level of a hierarchical abstraction to further improve inference efficiency.

3 Diagnostic Model Taxonomy

We represent an artifact as a propositional Wff over a set V of variables.

Definition 1 (Diagnostic System). A diagnostic system DS is defined as the triple DS = 〈SD, COMPS, OBS〉, where SD is a propositional theory over a set of variables V , COMPS ⊆

V , OBS ⊆ V , COMPS is the set of assumables, and OBS is the set of observables.

Throughout this paper we will assume that SD ̸|=⊥.

3.1 Diagnosis andMinimal Diagnosis

The traditional query in MBD computes terms of assumable variables which are explanations for the system description and an observation.

Definition 2 (Health Assignment). Given a diagnostic system DS = 〈SD,COMPS,OBS〉, an assignment HA to all variables in COMPS is defined as a health assignment.

A health assignment HA is a conjunction of propositional literals. Lit -(HA) is the set of negative literals in HA.

Definition 3 (Diagnosis). Given a diagnostic system DS = 〈SD,COMPS,OBS〉, an observation α over some variables in OBS, and a health assignment ω, ω is a diagnosis iff SD∧ α ∧ ω ̸|=⊥.

Traditionally, other authors [de Kleer and Williams, 1987] arrive at minimal diagnoses by computing a minimal hitting set of the minimal conflicts (broadly, minimal health assignments incompatible with the system description and the observation), while this paper makes no use of conflicts, hence the equivalent direct definition above.

In the MBD literature, a range of types of "preferred" diagnosis has been proposed. This turns the MBD problem into an optimization problem. We assume that we have a preference relation ⪯ over diagnoses, which enables us to specify a minimal diagnosis with respect to ⪯.

Definition 4 (Minimal Diagnosis). A diagnosis ω⪯ is defined as minimal if no diagnosis ˜ω⪯ exists such that Lit -(˜ω⪯) ⊂ Lit -(ω⪯).

This definition allows us to capture the two best-known definitions of minimality, namely subset-minimality (using order ⊆) and cardinality-minimality (using order ≤ which minimizes the number of negative literals).

The set of all diagnoses/minimal-cardinality (MC) diagnoses of a system description SD and an observation α is denoted as Ω(SD, α)/Ω≤(SD, α), respectively. We are often interested in computing the size of |Ω≤(SD, α)|. We refer to the latter problem as counting all MC diagnoses of SD and α.

3.2 Classification of Diagnostic Fault Models

We now introduce our classification of fault models. Given a health variable hi and an arbitrary Wff Fi, normal behaviour for component i is denoted using the clause hi ⇒ Fi, and abnormal behaviour by ¬hi ⇒ Fi. Hence a weak-fault model, as depicted in row 2 of Table 1, is given by ∧ni=1 (hi ⇒Fi); a strong-fault model consists of clauses denoting both normal and abnormal behaviour, i.e., ∧ni=1 (hi ⇒ Fi,1) ∧ (¬hi ⇒ Fi,2).

We generalize the well-known class of stuck-at models using the strong-fault class lSFM, in which each clause denoting abnormal behaviour is given by (¬hi ⇒ li) for some literal li; for example, this captures component i (with output li being stuck-at-0) as given by [(hi = stuck-at-0) ⇒ (li = 0)].

The class hSFM of Horn strong-fault models has the consequent Wff Fi restricted to Horn clauses. The class fSFM

of functional strong-fault models allows the consequent Wff Fi to take on any form. Finally, the class nlSFMof negativeliteral strong-fault models has the consequent Wff Fi restricted to defining the negation of the normal behaviour of component i given hi.

4 SFMAlgorithm

In this section we show that we can define an algorithm for specific classes of strong fault models which have complexity of the same class as weak fault models.

4.1 SFMDecomposability

We use the notion of model decomposability in this algorithm, which we introduce first.

Proposition 1. SD ∈ SFM is decomposable, i.e., SD = SDw∧SDs, where SDw, SDs are the weak and strong subsets of clauses, respectively, such that the subsets have no clauses in common, i.e., SDw ∩ SDs = ∅.

Proof. If we have a consistent SD, there can be no clause of the form hi ∧ ¬hi ⇒ Fi, where Fi is an arbitraryWff; i.e., every clause can have only one of hi or ¬hi in it. Hence we must be able to partition the clauses into: SDw which consists of clauses of the form hi ⇒ Fi, for i = 1, ...,m, and SDs which consists of clauses of the form ¬hi ⇒ Fi, for i = 1, ...,m. As a consequence, we can decompose SD = SDw ∪ SDs, such that SDw ∩ SDs = ∅.

In order to make use of this decomposability property, we need to prove that the strong fault portion of the model SDs will constrain the diagnoses that are generated by the weak part of the model SDw, since we compute the intersection of the diagnosis sets of the weak (Ω(SDw,OBS)) and strong (Ω(SDs,OBS)) sub-models, i.e., Ω(SD,OBS) = Ω(SDs, OBS) ∩ Ω(SDw, OBS).

Lemma 1. For a strong fault model SD ∈ SFM which is decomposable such that SD = SDs ∧ SDw, we must have Ω(SD, α) = Ω(SDw, α) \ Ω(SDs, α).

Proof. Since we are using a monotonic propositional logic, adding extra clauses to any formula F will reduce the number of logical models (diagnoses) of F. It is easy to show that Ω(SDw, α) ⊇ Ω(SDs, α). The diagnoses of SDs alone are given by Ω(SDs, α), and diagnoses excluded by SDs alone are given by Ω(SDs, α). Hence by adding SDs to SDw we obtain Ω(SD, α) = Ω(SDw, α) \ Ω(SDs, α).

4.2 SFMAlgorithm

Algorithm 1 shows how SFM decomposability can be used to extend existing MBD engines which can benefit from reasoning inWFM.

Algorithm 1 SFM Decomposition Algorithm

1: function DIAGNOSE(DS, α) returns a set of diagnoses inputs: DS = 〈SD, COMPS, OBS〉, diag. system α, term, observation local variables: ω, term, diagnosis z, term, internal variables SDw, SDs, system descriptions Ω, result, set of diagnoses 2: SDw ← NOMINALBEHAVIOR(SD) 3: SDs ← FAULTYBEHAVIOR(SD) 4: while MOREDIAGNOSES?(SDw, α) do 5: ω ← NEXTDIAGNOSIS(SDw, α) 6: U ← COMPUTEINTERNALS(SDw, α, ω) 7: if SDs ∧ α ∧ ω ∧ U ̸|=⊥ then 8: Ω ← Ω ∪ {ω} 9: end if 10: end while 11: return Ω 12: end function

Note that Alg. 1 is independent of the diagnostic inference engine Ξ. In lines 2-3, we decompose the model; in line 5 we compute a diagnosis ω using the weak portion SDw of the model using Ξ. Then, line 7 determines if ω is consistent with the strong portion of model, SDs. Our SFM

algorithm relies on being able to assign values in function COMPUTEINTERNALS to all internal variables, the correctness of which we show in Lemma 3.

The complexity of Diagnose(DS, α) depends on the complexity of three steps:

1. Computing a diagnosis in a weak fault model using a diagnostic oracle Ξ;
2. Computing values of internal variables U = V \(OBS∪ COMPS);
3. Computing a diagnosis in the strong portion of the fault model, SDs.

Our algorithm is independent of the diagnostic oracle Ξ, so we state the worst-case complexity here, and do not focus on the average-case complexity of any particular inference algorithm.

The complexity of computing a diagnosis in a weak fault model SD ∈ WFM (e.g., in the weak portion SDw of the fault model) is as follows:

Lemma 2. Given SD ∈ WFM, an observation α, the complexity of computing the first diagnosis ω(SD, α) is Σp1 - complete, and of computing subsequent diagnoses is Σp2 - complete.

Proof. For the class of propositional Horn abduction problems, Bylander et al. [1991] show that computing the first diagnosis ω(SD, α) is polynomial in |COMPS| + |OBS|), and of computing subsequent diagnoses is Σp1 -complete. Since we now deal with general propositional problems, the respective complexities will be up one level of the polynomial hierarchy, i.e., computing the first diagnosis ω(SD, α) is Σp1 -complete, and of computing subsequent diagnoses is Σp2 -complete. Further, these results concur with appropriate formulations in [Nordh and Zanuttini, 2008].

The complexity of computing the internal variables is as follows:

Lemma 3. Given SD ∈ WFM, an observation α assigning values to all variables in OBS, and a diagnosis ω, we can assign values to all internal variables U = V \ (OBS ∪ COMPS) in time O(|COMPS| · |V |).

Proof (Sketch). We first show the correctness of this procedure, and then show its complexity.

Correctness: Let OBS = IN ∪ OUT. For SD ∈ WFM and α, diagnosis ω assigns all hi for the clauses hi ⇒ Fi. For each component i that has all inputs in IN, we can compute its outputs given hi. Here we have to distinguish (1) hi and (2) ¬hi. In (1) the output of each gate can be computed directly from the inputs and the assumption that the gate is functioning correctly. In (2) the output of the gate is opposite to the one of a correctly functioning gate, otherwise the diagnostic inference cannot deduce ¬hi. If the circuit is connected, which we assume is the case, we can recursively compute the outputs of all downstream components, using induction on COMPS and the connectivity assumption.

Complexity: In the worst case every component has O(|V |) outputs, each of which can be determined in O(1) time, hence a total of O(|COMPS| · |V |) computations.

For nlSFM, we prove the following Lemma to be used later. Lemma 4. The strong part SDs of SD ∈ nlSFM is isomor-

phic to SD ∈ WFM.

Proof. We show this isomorphism by rewriting SDs so that it has the form of SDw. SDs has the form ¬hi ⇒ ¬Fi, and SDw has the form hi ⇒ Fi. If we rename the literals in SDs by replacing each literal v ∈ V such that ¬vi is replaced with ˜ vi, we obtain SDs with the form ˜ hi ⇒ ˜ Fi. The description for the strong part is now isomorphic to the description for the weak part, up to variable renaming.

The complexity of computing a diagnosis in the strong portion SDs of the fault model depends on the class of the model. We focus on the following strong fault model classes: lSFM, nlSFM, hSFM, fSFM.

Lemma 5. Given the strong portion SDs of SD ∈ SFM, an observation α assigning values to all variables in OBS, diagnosis ω(SDw, α) for the weak portion SDs of SD ∈ SFM, and values for internal variables U = V \(OBS∪COMPS), the worst-case complexity of the consistency check SDs ∧α∧ ω ∧ U ̸|=⊥ is given by:

• O(|V |) for SD ∈ lSFM;
• O(|V |) for SD ∈ hSFM;
• Σp1 -complete for the first diagnosis for SD ∈ nlSFM;
• Σp2 -complete for SD ∈ fSFM.

Proof. For SD ∈ lSFM, the strong part of the system description SDs is a 2SAT Boolean function, since it has the form ∧ni=1 (¬hi ⇒ li) ≡ ∧ni=1 (hi ∨ ¬li). As a consequence, SDS can be solved in time linear in the number of literals (using unit propagation).

For SD ∈ hSFM, SDs has the form ¬hi ⇒ Hi. Given we have assignments to all the hi, we need to check the consistency of a set of Horn formulae each of which is set to t or f. Since consistency checking of a set of Horn formulae is a linear-time operation, we can evaluate the consistency of SDs in linear time.

For SD ∈ nlSFM, the strong part of the system description SDs has the form ∧ni=1 [¬hi ⇒ (¬oi ⇔ Ci)], where Ci is any CNF Wff that does not include oi or hi, for i = 1, ..., n. Using Lemma 4, we can show that this task has the same complexity as computing a weak-fault diagnosis.

For SD ∈ fSFM (the case of general clauses), the complexity reverts to the worst-case result of Σp2 - completeness.

5 Experimental Results

Our approach applies to any domain in which models can be defined as in Table 1. We empirically demonstrate our approach using the well-known ISCAS85 circuits [Brglez and Fujiwara, 1985]. In addition to the original ISCAS85 models, we have performed cone reductions as described by Siddiqi and Huang [2007] and de Kleer [2008].

Table 2 gives an overview of all models (V and C denote the total number of variables and number of clauses, respectively). For each circuit we have generated 100 non-masking double-faults and counted the number of minimal-cardinality diagnoses for each observation. The results are summarized in Table 3 for the nlSFM and WFM representations.

Next we have repeated the counting of MC diagnoses in stuck-at-0 and stuck-at-1 models (SD ∈ lSFM). The results are shown in Table 4 (data for stuck-at-1 are very similar). With lSFM, there are observations α such that SD∧ α |=⊥. The number of these "inconsistent" observations are given in the θ columns of Table 4. Note that, in practice, θ increases with the cardinality of the MC diagnoses.

The data in Table 3 and Table 4, show similar diagnostic density for lSFM and nlSFM models. For the non-reduced circuits, the ratio of the mean number of MC diagnoses in lSFM to nlSFM varies between 0.13 (for stuck-at-0, c6552) and 0.41 (for stuck-at-1, c6552). The mean ratio of 0.26 shows that more than a quarter of theWFMdiagnoses are also diagnoses in SFM. This evidence, together with the large number of MC diagnoses in WFM, presume the existence of one or several continuous large lSFM subspaces.

Next we studied the effect of the fault modes on the average conflict size computed by a Logic-Based Truth Maintenance System (LTMS) [Forbus and de Kleer, 1993]. The conflict size is very important for algorithms like GDE [de Kleer and Williams, 1987] and CDA∗ [Williams and Ragno, 2007]. The LTMS conflict sizes for full models are shown in Table 5. We have measured similar reduction in the conflict size for reduced models. For each circuit and observation we computed the average conflict size from the "all nominal" candidate (SD ∧ α leads to a double fault, hence assuming each component is healthy leads to a conflict) and from all singlefault candidates. The WFM columns show these values averaged over all observations. The remaining three columns show the ratio of the average conflict sizes in WFM to the respective SFM subclasses.

Interestingly, the savings in the average conflict size (between 30% and 36%) are biggest in c6288, which is considered the most difficult ISCAS85 circuit in MBD.

Finally, we studied the effect of Alg. 1 on CDA∗ , whose average-case complexity is governed by the following two NPhard problems, which must be solved to compute minimal diagnoses, given a set of (non-minimal) conflicts: (1) compute the set of minimal conflicts by using, for example, directed resolution, and (2) compute the Minimal Hitting Sets (MHS) of all minimal conflicts [Reiter, 1987]. In this experiment we measured the time for computing the first 10 diagnoses in lSFMwith (1) CDA∗ and (2) Alg. 1 (i.e., CDA∗withWFM models and then discarding part of theWFMdiagnoses after fast consistency check). Table 6 demonstrates speed-ups of up to 750%. Note that our CDA∗ implementation is pretty limited in solving only "easier" diagnostic problems, and the advantage of model relaxation would be more visible with problems leading to diagnoses of higher cardinalities (more conflicts).

Table 6 shows that Alg. 1 leads to a considerable diagnostic speedup (up to a factor of 8) and that the speedup increases with the model size. The speedup is better observed with the non-reduced models. We expect even better speedup for diagnosis instances leading to a higher number of conflicts (and respectively higher MC diagnosis cardinality).

6 Conclusions

We have provided a classification of strong-fault diagnostics models, and have shown some computational properties of key sub-classes of such models. In particular, by decomposing a strong-fault model into disjoint strong and weak submodels, we have shown a relaxation algorithm which improves the efficiency of conflict-based inference algorithms by computing first the diagnoses for the weak sub-model, Ω(SDw, α), and then removing any diagnoses in Ω(SDw, α) inconsistent with the strong sub-model, which can be performed in low-polynomial or better time for several classes of propositional strong-fault models.

Our method is complementary to algorithms (such as conflict-based algorithms), which, on average, work faster withWFMmodels. Using ISCAS85 circuits, we have empirically demonstrated that: (1) a large portion of theWFM models are also diagnoses in the corresponding SFMmodels; (2) the average LTMS conflict size decreases; and (3) the diagnosis computation time in CDA∗ decreases by up to a factor of 8. Our method gives best results with the "difficult" c6288 circuit, and we conjecture that its speedups will increase with the complexity of diagnostic inference.

In the future we plan to extend our methods beyond propositional logic. One straightforward extension of our strongfault model classification is to many-valued logic, where components may have more than one nominal state; similar relaxation (or strengthening) techniques are also applicable to temporal logic.