An algebraic approach to model-based diagnosis

Traditional approaches to computing minimal conflicts and diagnoses use search technique. It is well known that search technique may cause combination explosion. Algebraic approach may be a way to solve the problem. In this paper we present an algebraic approach to model-based diagnosis. A system with an observation can be represented by a special Petri net PN, checking whether there is a conflict between the correct system behavior and the observation corresponds to checking whether there exists a marking M is an element of R(M-0) such that M(p(1)) and M(p(2)) are not zero, where p(1) and p(2) are labeled with the output of the system and its negation respectively. Furthermore, we show that M = M-0 + CX is such a marking, where M-0 is the initial marking, C is the incidence matrix of PN, and X is the maximal vector in {V broken vertical bar V is a {0,1}-vector and for each transition t, if V(t) = 1, then there is a firing sequence t(1), t(2), - - -, t(m), t}. Then, we present an algorithm to compute the maximal vector X in VSE(PN) in polynomial time. Once the maximal vector in VSE(PN) is generated, we can check whether there is conflicts between the correct system behavior and the observation. We also present algorithms for computing minimal conflicts and diagnoses by using the above algorithm. Compared with related works, our algorithm terminates in polynomial time if the inputs of the each component in the system are not more than a given constant.