Verification of Hybrid Automata Diagnosability by Abstraction

A notion of diagnosability for hybrid systems is defined, which generalizes the common notion of observability. We propose an abstraction procedure to translate a hybrid automaton into a timed automaton, in order to verify observability and diagnosability properties. We introduce a procedure to check diagnosability, and show that for the system class of our abstraction (namely for a subclass of timed automata: the durational graphs) the verification problem belongs to the complexity class P. We apply our procedure to an electromagnetic valve system for camless engines.