Verification of Hybrid Automata Diagnosability with Measurement Uncertainty

The problem of system diagnosability verification is concerned with whether a fault in the system operation can be diagnosed by using the system model and observations of the system output. In this paper, we investigate the (δd, δm)-diagnosability of hybrid automata, which characterizes the maximum delay for diagnosing faults since their first occurrence, given the measurement uncertainty in observing the system output. We present a methodology that analyzes the (δd, δm)-diagnosability of hybrid automata. Due to the complex dynamics, the hybrid system diagnosability is often difficult to analyze directly. We thus propose an approach of constructing an abstraction using the trajectories of the original system. Their (δd, δm)-diagnosability properties are proved to be quantitatively related to each other. The abstraction has only finitely many trajectories that extend to the end of the time horizon of interest, so its diagnosability can be easily calculated, and then used to derive the diagnosability of the original system.We illustrate this procedure with an example.