A Static Model-Based Engine for Model-Based Reasoning

1 Introduction

Since Reiter's seminal paper [Reiter, 1987], several generic systems for model-based diagnosis have been developed us­ ing logical inference, assumption based truth maintenance and conflicts as their underlying principles (see [de K.leer and Williams, 1987] and many others). Efficiency problems due to administration overhead inherent to this approach have only recently been solved [Raiman et al., 1993].

DRUM-II follows a different line of research which in­ vestigates reasoning through direct manipulation of logical models. Chou and Winslett [Chou and Winslett, 1994] have developed model-based algorithms for the minimal change semantics. Frohlich and Nejdl took up the ideas of Chou and Winslett and developed algorithms for minimal model computation and query answering under circumscrip­ tion [Frohlich and Nejdl, 1996].

In this paper we present a simpler and more efficient vari­ ant of this minimal model computation algorithm and apply it to diagnosis. First we introduce the basic algorithm which performs local search to find minimal models of the system description (and thus minimal diagnoses). Although this al­ gorithm is already efficient enough for a wide range of appli­ cations (like alarm management in telecom networks) large complex problems require additional focusing techniques. In most systems focusing is supported by recording actual de­ pendencies among the literals in the system description dur­ ing runtime. We introduce a new approach in which possible dependencies among the literals are detected statically during the compilation of the system description and used for focus­ ing the algorithm. To demonstrate the efficiency of the en­ gine we give a new characterization of a popular benchmark suite and discuss why the examples are hard to solve. We run our engine on these examples and compare its performance to previous results.

2 The Model-Based Framework

2.1 Relating Diagnoses and System Models

The device under consideration is described by a logical sys­ tem description SD, denoted as a set of clauses. To avoid confusion we use the term model only for logical Herbrand models represented by sets of atoms in this paper (and not for the system description). The observed behaviour is char­ acterized by a set of observations OBS. As usual, the set of system components is called COMP. With each component c E COMP we associate at least two behavioral modes: a cor­ rect mode denoted by Ok( c) and an abnormal mode denoted by Ab(c) = ·Ok(c). Our framework is suitable for express­ ing a wide range of diagnostic concepts. First we reconstruct Reiter's concept of minimal diagnosis.

Definition 1 A Diagnosis of (SD, COMP, OBS) is a set~~ COMP, such that SDU OBSU {Ab(c)Jc EMU { ·Ab(c)Jc E COMP- ~} is consistent. ~is called a Minimal Diagnosis, iff it is the minimal set (wrt. ~)with this property.

Next we characterize this diagnosis concept by the logical models of SD U OBS. Given a model M of SD U OBS, the ex­ tension oftheAb-predicate (denoted by MJAbJ) tells us which components are considered faulty by M. Thus, every model M of SD U OBS corresponds to a (possibly non-minimal) di­ agnosis MJAbJ. To characterize the minimal diagnoses using models, we define an order <Ab on the models, based on the abnormal components they contain.

Definition 2 Given models M, and M2, we define M, :SAh M2, iff MdAbl ~ M2IAbl and M, "'Ah M2, iff M,IAbl = M2IAbl. Furthermore we define M, <Ah M2, iff M, :SAh M2 and not M, "'Ah M2

The minimal diagnoses of (SD, COMPS, OBS) correspond to the :SAh-minimal models of SD U OBS.

Proposition 3 A set~ of components is a minimal diagnosis of (SD, COMP, OBS), iff there exists a :SAh-minimal model M of SD u OBS, such that~= MIAbl.

The following example shows that there can be several sys­ tem models corresponding to a single diagnosis. Consider a system componentC (an J 1 8X

integrated digital circuit) with two /2 C y

output ports X and Y.

Suppose the system description predicts the values X = 1 and Y = 0, given the current values of / 1 ,h and h. If we observe Y = 1, we have to assume that C is faulty. Since C is behaving abnormally, we cannot pre­ dict the value of X. Thus we have the following two :SAh-minimal models corresponding to the minimal diagno­ sis {C}: M1 = {Value(X,O), Value(Y, 1),Ab(C)} and M2 = {Value(X, 1) , Value(Y, 1),Ab(C)} .

M1 and M2 are equivalent (M, "'Ah M2), because they cor­ respond to the same diagnosis. DRUM-II therefore computes only one model out of every "'Ah-equivalence class. Such a representative set of minimal models is called a Transversal.

Definition 4 Let % be a set of models and %I"' Ah = {[M]IM E %} be a set of equivalence classes. A set%' is called a Transversal of %I"' Ah· iff%' contains exactly one member out of every equivalence class in %I"' Ah·

The following theorem shows that computing a transversal of the minimal models is a correct implementation of model­ based diagnosis.

Theorem 5 Let% := {MIM f= SDU OBS and JjN: (N f= SD U OBS and N <Ah M)} be the set of all :SAh-minimal models. Let%' be a transversal of MI"'Ah· Then D := {MIAbl IM E %'} is the set of all minimal diagnoses of (SD, COMP, OBS) .

While previous results on the relation of diagnosis and cir­ cumscription [Besnard and Cordier, 1994; Raiman, 1990] fo­ cus on formalizing stronger forms of explanation (than pro­ vided by consistency-based diagnosis), this theorem estab­ lishes an interesting connection between consistency-based diagnosis and circumscription, because % is the set of all models obtained by circumscribing SD U OBS in Ab, while varying all other predicates.

2.2 Repairing Inconsistent Models

The following algorithm was motivated by Chou and Winslett, who have implemented a system (IMMORTAL) for model-based belief revision [Chou and Winslett, 1994]. Con­ sider a system description SD and a model M which con­ tains no abnormals, such that M f= SD. Circuits, for exam­ ple, can be modeled by axioms describing the function of their gates. We split the observations into observations of input and output values respectively OBS = OBS;nUOBSour· A model W of the correctly functioning circuit can be ob­ tained by simulating the circuit's correct behavior given the input observations. More generally, monotonic first order logics can be used to construct a model of SD U { Ok( C) IC E Camp} U OBS;n . We denote the model which is obtained by incorporating the observations OBS into the model W by Ins( OBS,M 0 ). It is obtained by inserting the positive literals from OBS into M 0 and deleting the negative literals in OBS from M 0 . 1

Definition 6 For a model M we define lns(OBS,M) := OBSUM\ {xl·x E OBS} \ { ·xl·x E OBS}

The changed model M 1 = Ins(OBS,W) possibly contra­ dicts some of the axioms in the system description. Our algo­ rithm however uses the inconsistent model M 1 to construct a model of SD U OBS. It does so by inverting the truth values of literals in M 1 which contradict the axioms in SD.

Example 7 Consider SD = {a --+ c V d, d --+ ·e}, in clause form { { ·a, c, d}, { ·d, · e}} together with the initial model W = { e} and the observations OBS = {a}.

The model M 1 contradicts the axiom a --+ c V d. We can change it in two ways in order to make the axiom hold again. Either we assume c or d, because these are the other lit­ erals in the corresponding clause, which can make it true again. While assuming c creates a consistent model (M 2 ) of SD U OBS, assuming d violates the axiom d --+ · e. Thus, we have to delete e in order to obtain the second model M 4 .

To formalize the iterative model repair algorithm motivated in the above example, we need the concept of Committed Lit­ erals. The positive and negative literals, which have been inverted in model M; compared to the initial model W are called committed literals Comm(M;).

Definition 8

Comm(M;) := {llliterall and M f= land W ~ 1}

1 Note, that inserting OBS into~ has the same effect as inserting only OBSout. since in our case~ already reflects the input observa­ tions. In general, any model without abnormals can serve as initial model, so the notation lns(M, OBS) is more general.

Repair ...Model (SD, M 0 , OBS) Solutions : = 0; M 1 := Ins(OBS,M 0 ); Models := {M 1 }; WHILE Models =j:. 0 DO M := Select(Models); Models :=Models\ { M}; IF M p SDUOBS THEN Solutions : = Solutions U { M}; ELSE FOR ALL Flippings f DO Models:= ModelsU {Ins(--,f,M)}; END FOR; END IF; END WHILE;

In our example Comm(M 3 ) = { a,d}. To avoid cycles in the model repair algorithm, a committed literal is not considered for inversion again. We consider a literal for inversion, if it occurs in a violated clause and neither the literal itself nor its negative counterpart are committed. Such a literal is called a Flipping.

Definition 9 Let M; be a model and l a literal. l is called a Flipping, iff

1. There exists a clause C in SD such that l E C and M; ~ C and
2. l , --,1 ¢ Comm(M) .

Our iterative repair algorithm, which is summarized in fig­ ure 1 iteratively applies all possible flippings to the inconsis­ tent models. 2

2.3 Obtaining Minimal Models

During the repair process we maintain a set of partially re­ paired models (The set Models in figure 1). We have to se­ lect a model from this set and apply the next repair step to it. Since we want to compute minimal models, it is important to choose a model which is <Ah-minimal.

An earlier solution to the problem of model selection, which we presented in [Frohlich and Nejdl, 1996] and applied successfully to reasoning about change-problems, is a best­ first algorithm. The list of models is organized as a priority queue. This priority queue is sorted by the number of Ab­ literals in the models, and so the first element of the priority queue is always <Ah-minimal. Although this model selec­ tion policy is sufficiently efficient to solve benchmark prob­ lems from the reasoning about action and change domain, it proved not suitable for larger diagnostic applications. The main problem here is the management of multiple models and copying of models which is necessary after each repair step.

2 0ur idea of applying local changes to models is similar to GSAT [Selman et al., 19921. However, in contrast to GSAT, our method performs a deterministic exhaustive search for minimal models. For this task no probabilistic algorithms have been proposed so far.

In DRUM-II we therefore use an iterative deepening algo­ rithm for obtaining the minimal models. For this algorithm the model set is organized as a stack with the usual opera­ tions Push and Pop. A stack has a better locality than a prior­ ity queue, because all operations only affect its first element. When using a stack, we can implement the push and pop oper­ ations without really copying the models. However, since its top element is just some arbitrary model, we must implement other mechanisms to avoid the generation of non-minimal models. The iterative deepening algorithm first defines an initial upper bound Cutoff = I on the number of Ab-literals in a model. If a partially repaired model contains more Ab­ literals than Cutoff it is deleted, but a flag is set to indicate the deletion. The algorithm computes all consistent models with one Ab-literal and then sets Cutoff to the smallest number of Ab-literals of a model which was deleted. The algorithm pro­ ceeds until either no model is deleted or the bound Cutoff has reached an externally defined maximum (e.g. "only search for single and double faults") .

It is easy to see that ali" models generated by this algorithm are indeed minimal models. In the first iteration we only search for single faults. All single faults found are minimal diagnoses. Then we set the search limit to the next small­ est cardinality of a diagnosis which was pruned. During the search we always compare the models to the solutions already found. Thus, no non-minimal diagnoses are generated.

2.4 Formal Properties

The algorithm developed in the previous section is a sim­ pler and more efficient variant of the algorithms presented in [Frohlich and Nejdl, 1996] and fits in the framework for deciding entailment under circumscription presented in that paper. In the current paper we will only give the results rele­ vant to diagnosis.

Definition 10 Let M and N be sets. Diff(M,N) := (M\N) U (N\M)

Under the uniqueness of names assumption (UNA) and the domain closure assumption (DCA) (see [Lukaszewicz, 1990]) we can show that the set of models computed by ID_Repair...Model is a superset of those models of SDU OBS which differ minimally from the initial model~.

Lemma 11 Let SD be a system description without func­ tion symbols, for which we assume UNA and DCA. Let ~ be a model such that~ p SD and ~IAbl = 0. Let OBS be a set of literals. Let :M be the set of models re­ turned by ID..Repair...Model (SD, M 0 , OBS). Then :M 2 {M'IM' p SDU OBS and Diff(~,M') is minimal}.

Since M 0 1Abl = 0 it is easy to show that :M contains a model for each minimal extension of Ab. Thus :M contains a transversal of the minimal models and using theorem 5 we can conclude, that ID_Repair ..Model is a correct imple­ mentation of diagnosis:

Proposition 12 Let SD,OBS,W and :M be given as in lemma 11. For every diagnosis~ there is a model ME :M such that MIAbl = ~-

3 Static Dependencies

We will now present a theory of dependencies between lit­ erals in sets of horn clauses. These dependencies (and cor­ responding indepencies) can be used to focus the search for diagnoses. The results presented below are applicable to all system descriptions, where the correct model can be for­ malized by propositional horn clauses. We do not assume that the whole system description horn since some clauses are typically not horn, e.g. relations among fault models like Ok := ·Ab.

3.1 Exploiting Indepence of Literals

Let us consider a set of Horn Clauses S. Let {a 1 , ... , an} be the set of atoms occurring in S. We say that a; depends directly on a;, if there is a clause containing ai and ·a;.

Definition 13 a; depends directly on a; , denoted by a; --t 1 a j . iff there is a clause C E S with {a;, ·a;} ~ C.

We define the transitive closure of the direct dependency relation.--t 1 and call it--t+ (depends on).

Definition 14 The relation --t + is defined inductively by

We want to study the effect of certain atoms on the other atoms of the theory. In particular, we want to see which changes are caused by assuming different sets A,B of atoms. If we know that an atom a was entailed by SUA (i .e. SUA ~ a), we want to know if a is still entailed if we assume the set of atoms B instead.

Proposition 15 Let A and B be sets of atoms such that SU A ~ .l and SUA ~ .l. Let a be an atom. If SUA ~a and there is nob E Diff(A,B) such that b --t+ a, then SUB~ a.

Proof Sketch: The positive literal a follows from SUA, iff it holds in the minimal model of SUA . This minimal model coincides with the minimal model of s+ U A (s+ consists of those clauses of S, which contain a positive literal). Thus, s+ U A ~ a. Thus, there is a proof for a, only based on the clauses ~n s+. If we delete all unneccessary steps from this proof, only those steps remain, which derive a itself or liter­ als on which a depends. This proof remains possible, if we replace A by B since we assume that A and B do not disagree on atoms, on which a depends. Thus, s+ U B ~ a and, since SUB is consistent, we conclude SUB~ a. #

The knowledge from the above proposition can be used to focus the search for diagnoses.

3.2 Application to Diagnosis

In diagnosis, the horn clauses S are given by the system de­ scription SD. The following proposition is a special case of proposition 15.

Proposition 16 Let SD be a system description, OBS = OBS;nUOBSour an observation, a an atom and~ a candidate (a set of components considered faulty).

if SDU OBS;n ~a and for all c E ~: Ok(c) ft+ a, then SDU { Ok(c)ic E COMP\~} U OBS ~a.

To proof this proposition, we must assume, that the obser­ vations OBSout are really the outputs of the device, i.e. no further atom depends on the output observations. The above proposition allows us to delete any model, which contains changes not influenced by the current candidate.

Corollary 17 Let M be a model and a E M an atom occur­ ring negatively in Comm(Mi). Let ~ be a candidate. If for all c E ~: Ok(c) ft+ a then M ~ SDU OBSU {Ok(c)ic E COMP\~} and thus model M can be deleted.

The method described above enables us to eliminate a large number of candidates, which do not influence all abnormal outputs of the device as well as a large number of models which contain changes not influenced by the current candi­ date. The relation --t + needs only to be computed once for each system description. We compute --t + when the sys­ tem description changes and store it in a (bit-) matrix, which is loaded into memory by the DRUM-II engine. The space complexity as well as the time complexity for computing the matrix is quadratic in the number of clauses of the underlying system description. The offline computation of the matrix is rather efficient. For a large circuit, the c6288 (see section 4) our current implementation uses approximately one minute to compute --t+ . While we have not yet compared the vari­ ous optimizations of ATMS-based systems to our approach, a few comparisons can be made already. First, while an ATMS computes actual dependencies of propositions at run­ time, our approach computes possible dependencies at com­ pile time. Second, as these possible dependencies are cor­ rect for each truth value of the input propositions, they ob­ viously cannot exploit specific values of input propositions. An ATMS-environment is therefore more specific than our dependency set, and can exploit specific input values of the circuit. On the other hand, it seems impossible to precom­ pile ATMS-dependencies since they depend on the actual test vector used. Third, as ATMS' s usually store environments as bit vectors, the storage requirement for one environment is the same as for one of our dependency sets. Fourth, while a proposition usually can be deduced in different ways, and the ATMS therefore has to store more than one environment for these propositions, we have exactly one dependency set for each proposition, which avoids any explosion of these depen­ dency sets. An interesting issue for further exploration would be to use our possible dependencies in an ATMS instead of the specific justifications computed by the ATMS at run-time in order to speed up ATMS-based diagnosis systems.

4 Combinatorial Benchmark Circuits

The ISCAS-85 benchmark suite contains combinatorial cir­ cuits with 160 to 3512 components. In recent years it has been regarded as a challenge for diagnostic engines in sev­ eral papers [de Kleer, 1991; Raiman et al. , 1993; Nejdl and Frohlich, 1997; Williams and Nayak, 1997] due to the size of the problems and their inherent complexity. Before we discuss the performance of DRUM-II on these problems and compare it to previous results, we will give a characteriza­ tion of the kind of complexity present in these problems and discuss why some of these circuits are hard to solve.

4.1 Why are these Problems so hard?

For satisfiability and constraint satisfaction benchmarks con­ sisting of random problems are widely used. Random problems are often characterized by a set of parameters (n ,m, pi , p2 ) [Smith and Dyer, 1996], where n is the num­ ber of variables, m is the number of possibles values per vari­ able, Pi is the constraint density (the probabilty that a con­ straint exists between two variables) and P2 is the constraint tightness (the probability that two variables related by a con­ straint have incompatible values). The constraint tightness is not applicable to the circuits because the constraints (clauses) are not all binary. Other parameters for the ISCAS circuits are given in table 1. The estimated constraint density of the problems decrease when problem size increases 3 . This sug­ gests that the problems are hard in a dimension not yet cap­ tured by random problems or at least by their usual numeri­ cal characterization. Figure 2 shows the graph structure of a small part of the c6288 circuit (all successors of a particular component). We can observe the phenomenon of reconver­ gent fanout, which was already noted by de Kleer [Raiman et al., 1993]: Although a value occurs only in a small number of constraints, there are long chains of constraints, through which nearly all variables in the graph are finally related. For an algorithm this means that it is easy to find a locally consis­ tent solution but after a long computation it will eventually turn out that the solution is not globally consistent. Con­ sequently, the circuits are not easily solvable by brute force search alone and focusing is necessary. Moreover, there is a large number of long propagation paths making straightfor­ ward dependency recording algorithms run out of memory.

4.2 Experimental Results

In this section we include experimental results for DRUM­ II on the benchmark circuits. We have run 5 test vectors for each circuit. The running time is given in table 2. The times given are elapsed times in seconds on a lightly loaded SUN Ultra-11170. They do not include model setup time, which is, however, very short (using a domain-specific forward chainer for generating the initial model).

3 Due to the special structure of the system description the actual constraint density is even lower than these estimates

The test vectors used are available from the authors. Note, that the timing results show a large variation depending on the test vector used. This effect is striking with respect to the c6288. A reason for this is the different number of com­ ponents which can explain the abnormal observation. Table 3 shows the number of propositions (possibly) influencing the abnormal observation for the different test vectors of the c6288. In the difficult cases t1 and t4 nearly the whole circuit influences the abnormal observation. We expect a large vari­ ation in running time for ATMS-based systems, too, though no such results have been published so far.

In table 4 we compare the median running time of DRUM­ II to previous results from the literature. DRUM-II is always the fastest system except for the c6288 where IMPLODE is faster. Since however the test vector used is not given in [Raiman et al., 1993] it is not clear, whether IMPLODE's critical reasoning techniques provide still better focusing on the special structure of the c6288 for all test vectors.

5 Conclusion and Further Work

In this paper we describe the reasoning algorithm DRUM-II for diagnosis and other non-monotonic reasoning problems, which is based on the direct manipulation of logical models. It uses static precompiled information on the structure of the underlying theory and does no further recording at runtime. Running DRUM-II on a set of circuit diagnosis benchmarks with more than 3000 components shows that its efficiency is in most cases much better than the performance of previous systems. The paper also contains a short characterization of these benchmarks and their inherent complexity

Currently, we are extending DRUM to handle stronger de­ finitions of diagnosis (abductive diagnosis and kernel diagno­ sis). For these optimizations the filtering operator defined in [Frohlich and Nejdl, I996] is used, which decides, if the truth value of a given literal is entailed.

6 Acknowledgement

We thank Peter Baumgartner as well as an anonymous referee for their contributions to section 3