Increasing complexity and magnitude of technical systems demand an accurate fault localization in order to reduce maintenance costs and system down times. Resting on solid theoretical foundations, model-based diagnosis provides techniques for root cause identification by reasoning on a description of the system to be diagnosed. Practical implementations in industries, however, are sparse due to the initial modeling effort and the computational complexity. In this paper, we utilize a mapping function automating the modeling process by converting fault information available in practice into propositional Horn logic sentences to be used in abductive model-based diagnosis. Furthermore, the continuing performance improvements of SAT solvers motivated us to investigate a SAT-based approach to abductive diagnosis. While an empirical evaluation did not indicate a computational benefit over an ATMS-based algorithm, the potential to diagnose more expressive models than Horn theories encourages future research in this area.
Fault identification of technical systems is becoming increasingly difficult due to their rising complexity and scale. Economic and safety considerations have put accurate diagnosis not only into research focus but has led to a growing interest in practice as well.
Model-based diagnosis has been presented as a
method to derive root causes for observable
anomalies utilizing a description of the system to be
diagnosed [
Besides the consistency-based approach, a second
method emerged within the field of model-based
diagnosis, which exploits the concept of entailment to infer
explanations for given observables. While related to
the more traditional technique based on consistency,
abductive model-based diagnosis requires a system
formalization representing faults and their manifestations
[
Even though based on a well-defined theory, a
widespread acceptance of model-based diagnosis among
industries has not been accounted for yet. Two main
contributing factors can be identified: the initial model
development and the computational complexity of
diagnosis [
Apart from discovering inconsistencies, an ATMS is capable of inferring abductive diagnoses. However, it may face computational challenges and is restricted to operate on propositional Horn clauses. In the case of the models we are extracting from the FMEAs, this is not a limitation so far. Nevertheless, as we anticipate to exploit more expressive representations, a different approach is required.
The performance of Boolean satisfiability (SAT) solvers has improved immensely over the last years and several applications of SAT solvers in practice have proven successful. Furthermore, we are able to encode a greater variety of models in SAT. Thus, we propose a SAT-based approach to abductive diagnosis and empirically compare its performance to a procedure dependent on an ATMS.
The remainder of this paper is structured as follows. After formally providing the theoretical background on abductive diagnosis as well as relevant definitions in the context of SAT, we formulate the modeling process based on FMEAs and give information on the properties of the obtained system descriptions. In Section 5 we describe our SAT-based approach to abductive diagnosis and present an algorithm computing explanations for a given abduction problem. An empirical evaluation comparing our method to an ATMS-based diagnosis engine follows in Section 6. Subsequently, we provide some concluding remarks and give an outlook on future research possibilities. 2
Mechanizing logic-based abduction has been an active
research field for several decades with different
approaches for generating explanations emerging, such as
proof tree completion [
While the number of practical applications in the
context of abductive model-based diagnosis is rather
small, in [
Most recently [
In [
As stated by [
This section provides a brief introduction to abductive model-based diagnosis. In particular, we describe the propositional Horn clause abduction problem (PHCAP) which provides the basis for our research. Note that throughout the paper we consider the closed-world assumption. In addition to the background on abductive model-based diagnosis, we formally define MUSes and MCSes. 3.1
In contrast to the traditional consistency-based
approach, abductive model-based diagnosis depends on a
stronger relation between faults and observable
symptoms, namely entailment. Hence, whereas
consistencybased diagnosis reasons on the description of the
correct system operation, abductive reasoning requires the
model to capture the behavior in presence of a fault.
By exploiting the notion of entailment and the causal
links between defects and their corresponding effects,
we can reason about explanations for observed
anomalies. In general, abductive diagnosis is an NP-hard
problem. However, there are certain subsets of logic,
such as propositional definite Horn theory, which are
tractable [
Definition 1 (Knowledge base (KB)). A knowledge base (KB) is a tuple (A,Hyp,Th) where A denotes the set of propositional variables, Hyp ⊆ A the set of hypotheses, and Th the set of Horn clause sentences over A.
The set of hypotheses contains the propositions, which can be assumed to either be true or false and refer to possible causes. In order to form an abduction problem, a set of observations has to be considered for which explanations are to be computed.
Definition 2. (Propositional Horn Clause Abduction Problem (PHCAP)) Given a knowledge base (A,Hyp,Th) and a set of observations Obs ⊆ A then the tuple (A,Hyp,Th,Obs) forms a Propositional Horn Clause Abduction Problem (PHCAP).
Definition 3 (Diagnosis; Solution of a PHCAP). Given a PHCAP (A,Hyp,Th,Obs). A set Δ ⊆ Hyp is a solution if and only if Δ ∪ Th |= Obs and Δ ∪ Th 6|= ⊥. A solution Δ is parsimonious or minimal if and only if no set Δ0 ⊂ Δ is a solution.
A solution to a PHCAP is equivalent to an
abductive diagnosis, as it comprises the set of hypotheses
explaining the observations. Even though Definition 3
does not impose the constraint of minimality on a
solution, in practice only parsimonious explanations are of
interest. Hence, we refer to minimal diagnoses simply
as diagnoses. Notice that finding solutions for a given
PHCAP is NP-complete [
As aforementioned an ATMS derives abductive explanations for propositional Horn theories, thus it can be utilized to find solutions to a PHCAP. Based on a graph structure where hypotheses, observations, and contradiction are represented as nodes, the Horn clause sentences defined in T h determine the directed edges in the graph. Each node is assigned a label containing the set of hypotheses said node can be inferred from. By updating the labels, the ATMS maintains consistency.
Algorithm abductiveExplanations exploits an
ATMS and returns consistent abductive explanations
for a set of observations [
abductiveExplanations procedure (A, Hyp, T h, Obs)
Add T h to AT M S Add Vo∈Obs o → obs to AT M S return the label of obs end procedure . obs ∈/ A 3.2
We assume standard definitions for propositional logic
[
In case φ is unsatisfiable there are subsets of φ, which are of special interest in the diagnosis context, namely the MUSes and MCSes. A Minimal Unsatisfiable Subset (MUS) comprises a subset of clauses which cannot be satisfied simultaneously. Notice that every proper subset of MUS is satisfiable. A Minimal Correction Subset (MCS) is the set of clauses which corrects the unsatisfiable formula, i.e. by removing any MCS the formula becomes satisfiable.
Given an unsatisfiable formula φ, an MUS and MCS
are defined as follows [
Definition 5. (Minimal Correction Subset (MCS)) A subset M ⊆ φ is an MCS if φ \ M is satisfiable and ∀Ci ∈ M, φ \ (M \ {Ci}) is unsatisfiable.
Since an MCS is a set of clauses correcting the
unsatisfiable formula when removed, a single clause of an
MUS is an MCS for this MUS. Note that the hitting
set duality of MUSes and MCSes has been established
[
Example. Consider the unsatisfiable formula φ in CNF.
C1
C2
C3
C4 φ = (z¬a ∨}¬|b ∨ c{) ∧ (z¬c}∨| d{) ∧ z(}c|){ ∧ (z¬}|d{) It is apparent that the combination of clauses C2, C3 and C4 results in φ being unsatisfiable, hence
MUSes(φ) = {{C2, C3, C4}}.
By hitting set computation we arrive at the following set of MCSes:
MCSes(φ) = {{C2}, {C3}, {C4}}.
Removing any MCS of φ results in the formula being satisfiable.
It is worth noticing that utilizing subsets of
unsatisfiable formulas has been proposed in regard to
consistency-based diagnosis. In this context, a
diagnosis is defined as the set of components which assumed
faulty retains the consistency of the system. Thus, a
consistency-based diagnosis corresponds to an MCS.
For instance, [
As mentioned before model-based diagnosis depends on a formal description of the system to be examined. The generation of appropriate models, however, is still an issue preventing a wide industrial adoption, since the modeling process is time-consuming and typically demanding for system engineers.
Therefore, we present a modeling methodology
relying on FMEAs available in practice. An FMEA
comprises a systematic component-oriented analysis of
possible faults and the way they manifest themselves in
the artifact’s behavior and functionality [
Running Example. In order to illustrate our
modeling process, we use the converter of an industrial
wind turbine as our running example [
Component
Fault Mode
Effect Fan Fan IGBT
Corrosion
TMF HCF
T cabinet, P turbine T cabinet, P turbine T inverter cabinet, T nacelle, P turbine Consider the FMEA of the converter in Table 1. We can map the columns to their corresponding representations from Definition 6. The entries in the column Component constitute the elements of COM P , the entries in Fault Mode of M ODES and P ROP S subsumes the entries of Effect.
COM P = { F an, IGBT }
M ODES = { Corrosion, T M F, HCF } P ROP S =
T cabinet, P turbine,
T inverter cabinet, T nacelle Through Definition 6 we obtain F M EAConverter = (F an, Corrosion, {T cabinet, P turbine}),
(F an, T M F, {T cabinet, P turbine}), (IGBT, HCF, {T inverter cabinet, T nacelle, P turbine})
Since the FMEA already represents the relation
between defects and their manifestations the conversion to
a suitable abductive KB is straightforward. It is worth
noting that FMEAs usually consider single faults; thus,
the resulting diagnostic system holds the single fault
assumption. Let HC be the set of horn clauses. We define
a mapping function M : 2F MEA 7→ HC generating a
corresponding propositional Horn clause for each entry
of the FMEA [
Definition 7 (Mapping function M). Given an FMEA, the function M is defined as follows: M(F M EA) =def
[ t∈F MEA
M(t) where M(C, M, E) =def {mode(C, M ) → e |e ∈ E } . We utilize the proposition mode(C, M ) to denote that component C experiences fault mode M . Thus, the set of component-fault mode couples forms the set of hypotheses.
Hyp =def
[ (C,M,E)∈F MEA {mode(C, M )}.
In regard to the running example the following elements compose the set Hyp:
Hyp = ( mode(F an, Corrosion), ) mode(F an, T M F ), mode(IGBT, HCF )
The set of propositional variables A is defined as the union of all effects stored in the FMEA as well as all hypotheses, that is the set of component-fault mode pairs, i.e.:
A =def
[ (C,M,E)∈F MEA
E ∪ {mode(C, M )} A = T cabinet, P turbine, T inverter cabinet, T nacelle,
mode(F an, Corrosion), mmooddee((IFGaBnT,T, HMCFF),) Applying M results in the following set of propositional Horn clauses representing T h and thus completing KBConverter: T h = mode(F an, Corrosion) → T cabinet, momdeo(dFe(aFna,Cn,oTrrMosFio)n→)→T Pcabtuinrebti,ne, mode(F an, T M F ) → P turbine, mode(IGBT, HCF ) → T inverter cabinet, mmooddee((IIGGBBTT,, HHCCFF )) →→ TP ntuarcbeilnlee, On account of the mapping function M and the underlying structure of the FMEAs, the compiled models feature a certain topology. First, the set of hypotheses and symptoms are disjoint sets. Second, since there is a causal link from faults to effects but not vice versa, the descriptions exhibit a forward and acyclic structure. Specifically, each implication connects one hypothesis to one effect, thus are bijunctive clauses. In order to account for impossible observations, we append additional implications to KB stating that an effect and its negation cannot occur simultaneously, i.e. e ∧ ¬e |= ⊥.
The question remains whether the generated models are suitable for the diagnostic task. Abductive explanations are consistent by definition and complete given an exhaustive search. Thus, the appropriateness of the system description is determined by whether a single fault diagnosis can be obtained given all necessary information is available.
Definition 8. (One Single Fault Diagnosis Property (OSFDP)) Given a KB (A, Hyp, T h). KB fulfills the OSFDP if the following hold: ∀m ∈ Hyp : ∃Obs ⊆ A : {m} is a diagnosis of (A, Hyp, T h, Obs) and ¬∃m0 ∈ Hyp : m0 6= m such that {m’} is a diagnosis for the same PHCAP.
The property ensures that under the assumption
enough knowledge is available all single fault diagnoses
can be distinguished and subsequently unnecessary
replacement activities are avoided. To verify whether the
OSFDP holds or not, we compute the set of
propositions δ(h) implied by each hypothesis h and the theory.
It is not fulfilled if we can record for two or more
hypotheses the same δ(h). [
Algorithm distinguishHypotheses replaces all indistinguishable causes and ensures that after termination the given KB satisfies the OSFDP. Evidently, the algorithm’s complexity is determined by the three nested loops, hence O(|Hyp|2|A − Hyp|). Since there is a finite number of hypotheses and effects possibly included in δ(h) the algorithm must terminate. Algorithm 2 distinguishHypotheses procedure distinguishHypotheses (A, Hyp, T h) Ψ[|Hyp|] ← Hyp for all h1 ∈ Ψ do for all h2 ∈ Ψ do if h1 6= h2 then if δ(h1) = δ(h2) and δ(h1) 6= ∅ then
Create new hypothesis h0 . h0 ∈/ Hyp Add h0 to Ψ Add h0 to A for all e ∈ δ(h1) do
Add (h0 → e) to T h Remove (h1 → e) from T h
Remove (h2 → e) from T h end for Remove h1 ∧ h2 from Ψ
Remove h1 ∧ h2 from A end if end if end for end for return KB(A, Ψ, T h) end procedure
Our running example of the converter does not fulfill the OSFDP, since mode(F an, Corrosion) and mode(F an, T M F ) are not distinguishable. By removing both hypotheses and introducing h0 = mode((F an, Corrosion), (F an, T M F )) the property is fulfilled.
Notice that abductive diagnosis is premised on the assumption that the model is complete; thus, we presume that all significant fault modes for each contributing part of the system have been contemplated in the FMEA. Furthermore, we expect on the one hand that the symptoms described within the FMEA are detectable in order to constitute observations. On the other hand, the automated mapping demands a consistent effect denotation throughout the analysis. 5
Although an ATMS derives abductive diagnoses, it is limited to propositional Horn theories and subject to performance issues. Both problems have been accommodated through ATMS extensions and focus strategies. Nevertheless, the advances in the development of SAT solvers and their application to a vast number of different AI problems and industrial domains have motivated us to consider a SAT-based approach for abductive diagnosis.
Recall Definition 3 of a diagnosis: Δ is an
abductive explanation if Δ ∪ T h |= Obs and Δ ∪ T h 6|= ⊥.
Through logical equivalence we recast the first
condition to Δ ∪ T h ∪ {¬Obs} |= ⊥, where {¬Obs} denotes
the set containing the complement of each observation
in Obs, i.e. ∀o ∈ Obs : ¬o ∈ {¬Obs} [
Since MUSes contain several unsatisfiable subsets irrelevant for the diagnostic task, we define the set M U SesHyp, which only contains subset minimal MUS comprising clauses referring to hypotheses: Definition 9. (M U SesHyp) Let M U Ses be the set of MUSes of Hyp∪T h∪{¬Obs}, then ∀M ∈ M U SesHyp : ∃U ∈ M U Ses : M = U ∩ Hyp and ¬∃M 0 ∈ M U SesHyp : M 0 ⊂ M.
Corollary 1. Given a P HCAP (A, Hyp, T h, Obs), let M U SesHyp be the set of interesting MUSes. A set Δ ⊆ Hyp is a minimal abductive diagnosis if ∃M ∈ M U SesHyp : Δ = M and Δ ∪ T h 6|= ⊥.
Proof. We can restate the problem of computing inconsistencies to finding the set of prime implicates of T h∧Hyp∧{¬Obs}. By definition, the prime implicates are equivalent to the MUSes of said formula.
Deriving a minimal abductive explanation corresponds to computing a minimal subset of the hypotheses, which cannot be simultaneously satisfied with the theory and the negation of observations.
We devised the algorithm satAB, which computes the
set of abductive diagnoses for a given PHCAP based on
MUS enumeration. First, in order to take advantage of
the MUSes, which correspond to the solutions of the
PHCAP, we create an unsatisfiable CNF encoding of
the problem. Since the T h consists of Horn clauses
a conversion into CNF is straightforward. Note that
we are, however, not limited to Horn clause models, as
we can create a CNF representation based on Tseitin
transformation [
The diagnostic task consists in computing the sets of
hypotheses which are responsible for the
unsatisfiability of φ, i.e. M U SesHyp(φ). Since finding satisfiable
subsets is an NP-hard problem whereas UNSAT resides
in Co-NP, we employ an MCSes enumeration algorithm
on the unsatisfiable formula and then derive the
diagnoses via hitting set computation [
Consider again our running example of the converter. We already obtained the KB via the mapping function M. Let us assume that the condition monitoring system of the wind turbine encountered that the turbine’s power output is lower than expected (P turbine) and that the cabinet temperature exceeds a certain threshold (T cabinet), i.e. Obs = {P turbine, T cabinet}. In Figure 1 we depict the CNF representation φ of the abduction problem. Clauses C1 to C7 refer to T , C8 to C10 to the set Hyp and clause C11 contains the negation of the set of observations.
Computing the M CSes of φ we obtain: M CSes = ( {C11} , {C1, C3} , {C1, C9} , {C3, C8} , {C9, C8} , ) {C4, C7, C2} , {C4, C10, C2} , {C4, C7, C8} , {C4, C10, C8} , {C2, C9, C7} , {C2, C9, C10} .
Extracting the MCSes, which only contain clauses from Hyp and are consistent with regard to the theory, results in
M CSesHyp = {{C9, C8}}.
By computing the hitting set of M CSesHyp, we obtain the set of MUSes solely referring to explanations, which is in fact the set of diagnoses: Δ − Set = {{C9} , {C8}}. diagnoses and Δ2 are =
Δ1 = {mode(F an, Corrosion)} {mode(F an, T M F )}. 6
To determine whether computing abductive diagnoses
via SAT yields any computational advantages in the
case of our models, we conducted an empirical
evaluation, comparing abductiveExplanations to satAB
on several instances of FMEAs. In case of the former
we employed a Java implementation of an unfocused
ATMS. The algorithm satAB exploits on the one hand
an MCS enumeration procedure and on the other hand
an implementation of a hitting set algorithm. We
utilized the MCSLS tool by [
Several publicly available as well as project internal FMEAs provide the basis for our evaluation. They cover various technical systems and subsystems with different underlying structures. In particular they describe faults in electrical circuits, a connector system by Ford (FCS), the Focal Plane Unit (FPU) of the Heterodyne Instrument for the Far Infrared (HIFI) built for the Herschel Space Observatory, printed circuit boards (PCB), the Anticoincidence Detector (ACD) mounted on the Large Area Telescope of the Fermi Gamma-ray Space Telescope, the Maritim ITStandard (MiTS), and rectifier, inverter, transformer, backup components, as well as main bearing of an industrial wind turbine. By applying the mapping function M, we generated the corresponding abductive knowledge bases KB for each FMEA. Table 2 provides an overview of the FMEAs’ structure and the evaluation results. It is worth noting that the FMEAs vary in the number of hypotheses, i.e. component-fault mode couples, the number of effects, and the number of rules, i.e. the links between faults and symptoms. Due to T h of an abductive KB comprising Horn clauses, a conversion into a CNF representation, suitable for the MCSLS tool, is straightforward. We do not address the model compilation times, since the system description would be compiled offline and the mapping execution consumed less than one second for the examples we utilized so far.
Table 2 shows that none, except of the model resulting from the transformer’s FMEA, of the original models satisfy the OSFDP. Therefore, we compiled a second set of models fulfilling the property by exchanging each set of indistinguishable hypotheses with a new single hypothesis representing said set. For example, Algorithm distinguishHyp ensures that the resulting KB satisfies the OSFDP. In Table 2 the original models are identified accordingly, and the adapted models are provided with the label OSFDP. Note that the number of hypotheses and rules diminishes for the adapted models.
In the experiments, we computed the abductive
explanations for |Obs| from one to the maximum number
of effects possible. The observations were generated
randomly; however, the same set was used for satAB
and abductiveExplanations on the original as well as
adapted model. The results reported in Table 2 have
been obtained from ten trials and both algorithms faced
a 200 seconds runtime limit. Whereas some of the small
runtimes are arguable due to the measurement in the
milliseconds range, Table 2 reveals that satAB (Mean
= 703.73 ms, SD = 8432.07 ms, Median = 0.59 ms,
Skewness = 18.61) does not outperform
abductiveExplanations (Mean = 3.08 ms, SD = 16.38 ms, Median
= 1 ms, Skewness = 12.68) in general. From the
statistical data we can infer that the underlying distribution
of both algorithms is highly right skewed, thus the bulk
of values is located towards the lower runtimes. We can
even observe that for certain instances, the SAT-based
approach performs rather poorly. Amongst these are
the model of an inverter and a rectifier of an industrial
wind turbine. satAB exceeded the given timeout four
times for the former. Notice that in all these cases the
MCSes generation already reached the time threshold.
According to [
Figure 2 illustrates the cumulative log runtimes for satAB and abductiveExplanations on the FMEA models generated. Although abductiveExplanations performs on average better, the first model requires a longer computation time for both algorithms. Moreover, the illustration reveals the high computational effort necessary for satAB to compute the diagnoses for the model of the inverter. As expected we observe particularly high runtimes when the set of observations contains effects corresponding to different hypotheses. This has a greater impact on satAB than on the ATMS implementation. For the section from the models FCS to PCB in Figure 2, however, we can see that the cumulative runtime for abductiveExplanations rises at a steeper angle. Generally, the data gathered in the experiment do not suggest a performance benefit of the SAT-based approach over an ATMS implementation. 7
In the course of the paper, we presented a mapping from failure assessments available to propositional Horn clause models. The modeling methodology relies on FMEAs as they comprise information on faults and their symptoms. Hence, they provide a suitable source for model compilation. Although in our case an ATMS can be used to compute abductive diagnoses, it is limited to propositional Horn theories. We proposed a SAT-based approach to abductive model-based diagnosis which allows us to reason on more expressive representations. Our method is based on computing conflict sets, i.e. MUSes, resulting from a rewritten, unsatisfiable system description. Subsets of these unsatisfiable cores constitute the minimal abductive explanations. Since the computation of MUSes is computationally demanding our proposed algorithm exploits its hitting set dual, MCSes, in order to derive minimal diagnoses.
We empirically compared an implementation of a diagnosis engine employing an ATMS to our SAT-based algorithm. The results indicate that while for some of the models, the algorithm performs well, in general we could not observe a performance advantage. Particular examples led to even longer computation times than the ATMS-based implementation. Despite the fact that the data provided no evidence of a computational benefit in employing a SAT-based approach, we believe that the possibility to utilize more expressive models provides an interesting incentive for future research in this area.
Since the evaluation results, did not indicate a
superiority of the SAT-based approach on grounds of
MCSes enumeration, we currently investigate direct conflict
generation methods. Additionally, due to the model
structure and the experiment data we are planning on
employing compilation methods [
The work presented in this paper has been supported by the FFG project Applied Model Based Reasoning (AMOR) under grant 842407. We would further like to express our gratitude to our industrial partner, Uptime Engineering GmbH.
Proceedings of the 26th International Workshop on Principles of Diagnosis 176