A notion of diagnosability for hybrid systems is defined, which generalizes the 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 propose 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.

Verification of Hybrid Automata Diagnosability by Abstraction

DI BENEDETTO, MARIA DOMENICA;D'INNOCENZO, ALESSANDRO;DI GENNARO, Stefano
2011-01-01

Abstract

A notion of diagnosability for hybrid systems is defined, which generalizes the 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 propose 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.
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11697/89459
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 13
  • ???jsp.display-item.citation.isi??? 5
social impact