Symbolic Calculation Of Model Based Diagnosis In Discrete Event System

In the large-scale industrial systems and aerospace systems, some small failure can causeunimaginable consequences and irreparable disaster. In order to avoid such disasterand makefailure nipped in the bud, a new branch of artificial intelligence, fault diagnosis has beenproduced. The initial typical method of faultdiagnosis basedon the expert system. The methodrequires strong professionalknowledge, so it is system-dependent and not well portability.In the eighties of last century, in order to overcome the serious defect of the traditionaldiagnostic methods, Model Based Diagnosis(MBD) rised. After30years of development, ithas become a very important branch of arti-ficial intelligence field.So by the concern of themajority of experts and scholars at home and abroad, it has a wide range of applications in themedical,chemical, electronic, mechanical, software debugging and economic.The initial MBD was based on the static system, with the development of diagnostictechniques, it gradually excess to the dynamic system. Model Based Diagnosis of DiscreteEvent System(DES) is transition between static systems and dynamic systems. The states ofDiscrete event systems are closed to the static systems, while the expression of many mixedor continuous-valued dynamic systems through hierarchical and status abstract approximateDES.Most of the DES are modeled by Finite State Machine(FSM). According totheobservation,we search the system graph. In order to reduce the time complexityofsearching, we construct diagnoser before system diagnosis. But, when the diag-nostic systemmodel is in the large scale, in the stage of the diagnoser calculation, there will be spaceexplosion phenomenon. This is because the number of states of the diagnoser is exponentialof the number of the system model.This article convert the DES modeled by FSM to the Boolean expression. One method isin the form of Conjunctive Normal Form(CNF), the other is of Bina-ry Decision Diagram(BDD). CNF is the import form of satisfiability problem(SAT). SAT has importantapplications in artificial intelligence, graph theory, planning and so on. Many issues is directlythe form of SAT or can be transformed to SAT, and the formulation and data structure of SATis relatively simple. In contacting the diagnosis of DES with SAT, this article may well be agood way. Algorithms used in this diagnosis is inspired from the DP algorithm of SAT, andagainst the characteristic of DES we use the attributing method to diagnose.BDD is a specification expression of the Boolean functions, and it has a good applicationin model diagnosis and model checking. The most important featureof this method is that, bythe coding of some of the parameters variables used in the model can be greatly reduced. We model DES with BDD, then abstract system further,and finally according to the observableevent sequence we apply related algorithm for diagnosis. On the principle of systemabstraction and diag-nostic method, it is similar to the previous method, but differs on thespecific operations.This two methods in the abstraction of systems are easier than the traditional methods,and in the constructing of the diagnoser there are not new states, andtherefore we can avoidthe space explosion phenomenon of diagnoser. But in the stage of abstraction, the CNFmethod has to traver all transfer of the system model, while the BDD method reduces the timeneeded by the traversal because of its feature and it also uses a lot fewer variables forexpression thanother methods.