Research On DES Fault Diagnosis System Based On Propositional Satisfiability

Recently, the scale and function of modern industrial artificial system is getting stronger and stronger, meanwhile, the action of the system is also becoming more and more complex. In the event of system malfunction, which cannot be effectively ruled out in time, it is likely to cause catastrophic consequences. Therefore, it is very important to effectively troubleshoot the system crash in time. At present, Researches on fault diagnosis method have achieved some results at home and abroad. Discrete-event systems (DES) due to man-made systems can be easily characterized, so fault diagnosis method based on DES is currently more popular fields of study. Propositional satisfiability problem (SAT) is the core issue in the field of artificial intelligence, but also the basis for solving many practical problems. An Algorithm for SAT currently already very efficient, the efficiency of the use of SAT solving for fault diagnosis would be a very good subject.This paper summarized the research progress of fault diagnosis techniques, and applied SAT solving algorithm on the fault diagnosis, which was based on the high efficiency of SAT solving algorithm. In detail, the system model was encoded to the format that SAT solver could recognize, and then solved by the SAT solver. The solving result obtained was the diagnosis result. Because the result was a set of assignment, a decoder (explanation) procedure was needed to translate the assignment into a readable diagnosis results.In this paper, we designed and achieved a fault diagnosis system which can support this method. In order to check the effects of our approach and the corresponding system, we used the state-machine automatic generation algorithm to automatically generate the required state machine model experiments. And we analyzed the diagnostic features of this diagnostic method. Our experiments demonstrate that the proposed method is much more efficient than traditional diagnosis algorithms. It also shows that the diagnosis system has some practical values.