Manifestability Verification of Discrete Event Systems
Résumé
Fault diagnosis is a crucial and challenging task in the automatic control of complex systems, whose efficiency depends on the diagnosability property of a system, allowing one to determine with certainty whether a given fault has effectively occurred based on the available observations. However, this is a quite strong property that generally requires a high number of sensors. Consequently, it is not rare that developing a diagnosable systemis too expensive. In this paper, we analyze a new system property called manifestability, that represents the weakest requirement on observations for having a chance to identify on line fault occurrences and can be verified at design stage. Intuitively, this property makes sure that a faulty system has at least one future behavior after fault occurrence observably distinguishable from all normal behaviors. Then, we propose an algorithm with PSPACE complexity to automatically verify it for finite automata. Furthermore, we prove that the problem of manifestability verification itselfis PSPACE-complete. The experimental results show the feasibility of our algorithm from a practical point of view. Then, we extend our approachto real-time systems modeled by timed automata.To do this, we redefine manifestability by taking into account time constraints and we prove that this problem for timed automata is undecidable.
Fichier principal
Manifestability_Verification__of_Discrete_Event_Systems_DX19.pdf (236.23 Ko)
Télécharger le fichier
Origine | Fichiers produits par l'(les) auteur(s) |
---|