Dynamic theorem proving algorithm for consistency-based diagnosis

作者：Zhang Li Ming; Zeng Hai Lin; Fang Yang; Ouyang Dan Tong^*

来源：Expert Systems with Applications, 2011, 38(6): 7511-7516.

DOI：10.1016/j.eswa.2010.12.117

• Satisfiability
• Model-based diagnosis
• Dynamic algorithm
• Conjunctive normal form

In this paper, a dynamic theorem proving (DTP) algorithm is proposed for dynamically judging whether a component set is consistency-based diagnosis in model-based diagnosis. Firstly, the model of the system to be diagnosed and all the observations are described with conjunctive normal forms (CNF), and the problem of diagnosis is translated into the satisfiability of the related clauses in the CNF files. Next. all the minimal consistency-based diagnostic sets are derived by calling DTP dynamically combining with the CSSE-tree. As the theorem about the number of components in minimal diagnosis is proposed, the majority of the non-minimal diagnosis can never be produced. Moreover, this approach can compute all the consistency-based diagnostic sets directly, without computing all the conflict sets and therefore the hitting sets of the collection of the corresponding conflict sets like the classical methods. Finally, the approach's soundness, completeness and complexity are analyzed and proved, and results show that the program is easy to be implemented, and the diagnosis efficiency is highly improved.

• 出版日期2011-6
• 单位吉林大学