Verification of Diagnosability for Cyber-Physical Systems: A Hybrid Barrier Certificate Approach

• 成果类型: Article
• 署名作者: Zhong, Bingzhuo; Dong, Weijie; Yin, Xiang; Zamani, Majid
• 署名单位: Hong Kong University of Science & Technology; Shanghai Jiao Tong University; University of Colorado System; University of Colorado Boulder
• 刊物名称: IEEE TRANSACTIONS ON AUTOMATIC CONTROL
• ISSN/ISSBN: 0018-9286
• DOI: 10.1109/TAC.2026.3669025
• 发表日期: 2026
• 关键词: AUTOMATA DIAGNOSABILITY; FAULT-DIAGNOSIS; opacity

摘要

Diagnosability is a system theoretical property characterizing whether fault occurrences in a system can always be detected within a finite time. In this article, we investigate the verification of diagnosability for cyberphysical 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. In addition, 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.