Logic programs for consistency-based diagnosis.
Gregory W. Bond · 1994
In this dissertation we develop a solution to the problem of automating systems diagnosis, where we define diagnosis to be the task of identifying potentially faulty system components given assertions regarding intended or erroneous system behavior. The solution is applicable to systems that are characterized by the fact that (i) there exists a priori knowledge concerning the modes or probability of component failure, and (ii) either there does not exist complete knowledge of the system's specification or observability of the system itself is restricted. Domains for which there exist significant numbers of systems satisfying these properties are software development domains, hardware development domains and domains concerned with the development of system specifications. The solution to the problem takes the form of a theoretical framework and a number of polynomial-time procedures for computing the diagnoses defined by the framework. The framework we develop is an instance of an existing diagnostic approach known as consistency-based diagnosis. Diagnoses are defined with respect to a set of first-order assertions and a system description based on a logic program. Using logic programs as the basis for system descriptions presents a number of advantages including ease of model construction, the ability to diagnose hierarchically structured systems and software systems, and the automatic definition of negative system behavior. Two necessary and sufficient conditions for component abnormality are defined and shown to reflect intuitive notions of faults occurring in hierarchies. We also formally show that the approach to logic program diagnosis known as declarative error diagnosis is a specialized instance of the consistency-based diagnosis framework developed here. One of the two diagnosis computation procedures developed for the framework efficiently computes diagnoses for a restricted class of assertions. We prove this procedure sound, identify conditions for completeness and prove its implementation correct. The other, more complex, procedure computes diagnoses for a more general class of assertions. We prove this procedure to be sound, discuss completeness issues and prove its implementation correct. Both procedures are implemented in Prolog and are used to compute diagnoses for a combinatorial logic circuit, a sequential logic circuit and a buggy logic program.