Model Checking on Fault Diagnosis Graph

This paper investigates the use of model checking techniques for fault diagnosis on timed systems. The timed systems are modeled with time Petri nets (TPN). Our approach is based on the fault diagnosis graph (FDG), which is obtained from the state class graph of TPN, by removing nodes and edges that are not used in fault diagnosis. In order to apply the reduction rules, we assume that the FDG is bounded and completely constructed. We first propose some reduction rules on the FDG to obtain a more compact representation and then we use model checking techniques on the reduced FDG to compute the diagnosis states. We compare the complexity of model checking on FDG with the one on the reduced FDG.