Abstract: Due to drop of quantitative and nonlinear causal information,the solution of signed directed graph(SDG) fault diagnosis needs to be further verified and validated.Verification for the solution of SDG fault diagnosis is placed in the framework of symbolic model checking.A formal verification approach for the solution of SDG fault diagnosis via symbolic model checking(SSDGFD_SMC) is proposed.A formal characterization of SDG model,as a finite state transition system,is defined firstly,and SMV(symbolic model verifier) module is modeled.Secondly,the dynamic verification information for the observed variables is set up by means of fault propagation time,and the dynamic inference verification strategy based on progressive monitoring is analyzed.Then SMV model is extended for the dynamic inference verification process,and SSDGFD_SMC algorithm is designed.Finally,the practical applicability of SSDGFD_SMC is demonstrated by a simple water tank SDG model.