Diagnosability verification for hybrid automata and durational graphs

A notion of diagnosability for hybrid systems is defined, which generalizes the notion of observability. We verify diagnosability properties on a timed automaton abstraction of the original hybrid system. We propose a procedure to check diagnosability, and show that the computational complexity is in PTIME for the system class of our abstraction, namely for a subclass of timed automata: the durational graphs. We apply our procedure to an electromagnetic valve system for camless engines. For an extended version of this paper refer to M.D. Di Benedetto, et al. (2007).