How To Be Sure A Faulty System Does Not Always Appear Healthy?

Fault diagnosis is a crucial and challenging task in the automatic control of complex systems, whose efficiency depends on the diagnosability property of a system. Diagnosability describes the system property allowing one to determine with certainty whether a given fault has effectively occurred based on the available observations. However, this is a quite strong property that generally requires a high number of sensors. Consequently, it is not rare that developing a diagnosable system is too expensive. In this paper, we analyze a new discrete event system property called manifestability, that represents the weakest requirement on observations for having a chance to identify on line fault occurrences and can be verified at design stage. Intuitively, this property makes sure that a faulty system cannot always appear healthy, i.e., has at least one future behavior after fault occurrence observably distinguishable from all normal behaviors. Then, we prove that manifestability is a weaker property than diagnosability before proposing an algorithm with PSPACE complexity to automatically verify both properties. Furthermore, we prove that the problem of manifestability verification itself is PSPACE-complete. The experimental results show the feasibility of our algorithm from a practical point of view. Finally, we compare our approach with related work.