Verification of Hybrid Automata Diagnosability by Abstraction
Maria Domenica Di Benedetto, S. Di Gennaro, Alessandro D’Innocenzo · IEEE Transactions on Automatic Control · 2011
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.