Weijie Dong

Diagnosability is a system theoretical property characterizing whether fault occurrences in a system can always be detected within a finite time. In this paper, we investigate the verification of diagnosability for cyber-physical systems with continuous state sets. We develop an abstraction-free and automata-based framework to verify (the lack of) diagnosability, leveraging a notion of hybrid barrier certificates. To this end, we first construct a ($\delta,K$)-deterministic finite automaton that captures the occurrence of faults targeted for diagnosis. Then, the verification of diagnosability property is converted into a safety verification problem over a product system between the automaton and the augmented version of the dynamical system. We demonstrate that this verification problem can be addressed by computing hybrid barrier certificates for the product system. To this end, we introduce two systematic methods, leveraging sum-of-squares programming and counter-example guided inductive synthesis to search for such certificates. Additionally, if the system is found to be diagnosable, we propose methodologies to construct a diagnoser to identify fault occurrences online. Finally, we showcase the effectiveness of our methods through a case study.

In this paper, we investigate the diagnosability verification problem of partially-observed discrete-event systems (DES) subject to unreliable sensors. In this setting, upon the occurrence of each event, the sensor reading may be non-deterministic due to measurement noises or possible sensor failures. Existing works on this topic mainly consider specific types of unreliable sensors such as the cases of intermittent sensors failures, permanent sensor failures or their combinations. In this work, we propose a novel uniform framework for diagnosability of DES subject to, not only sensor failures, but also a very general class of unreliable sensors. Our approach is to use linear temporal logic (LTL) with semantics on infinite traces to describe the possible behaviors of the sensors. A new notion of $\varphi$ -diagnosability is proposed as the necessary and sufficient condition for the existence of a diagnoser when the behaviors of sensors satisfy the LTL formula $\varphi$ . Effective approach is provided to verify this notion. We show that, our new notion of $\varphi$ -diagnosability subsumes all existing notions of robust diagnosability of DES subject to sensor failures. Furthermore, the proposed framework is user-friendly and flexible since it supports an arbitrary user-defined unreliable sensor type based on the specific scenario of the application. As examples, we provide two new notions of diagnosability, which have never been investigated in the literature, using our uniform framework.