Infinite-and K-Step Opacity Verification of Discrete-Event Systems Under Nondeterministic Observations  

作　　者：CHU Qian ZHANG Jiahui HAN Xiaoguang LI Zhiwu CHEN Zengqiang 

机构地区：[1]College of Electronic Information and Automation,Tianjin University of Science and Technology,Tianjin 300222,China [2]Institute of Systems Engineering,Macao University of Science and Technology,Taipa 999078,China [3]College of Artificial Intelligence,Nankai University,Tianjin 300350,China

出　　处：《Journal of Systems Science & Complexity》2023年第5期1830-1850,共21页系统科学与复杂性学报（英文版）

基　　金：supported by the National Natural Science Foundation of China under Grant Nos.61903274,61873342,61973175;the Tianjin Natural Science Foundation of China under Grant No.18JCQNJC74000。

摘　　要：In some practical applications modeled by discrete-event systems(DES),the observations of events may be no longer deterministic due to sensor faults/failures,packet loss,and/or measurement uncertainties.In this context,it is interesting to reconsider the infinite-step opacity(∞-SO)and K-step opacity(K-SO)of a DES under abnormal conditions as mentioned.In this paper,the authors extend the notions of∞-SO and K-SO defined in the standard setting to the framework of nondeterministic observations(i.e.,the event-observation mechanism is state-dependent and nondeterministic).Obviously,the extended notions of∞-SO and K-SO are more general than the previous standard ones.To effectively verify them,a matrix-based current state estimator in the context of this advanced framework is constructed using the Boolean semi-tensor product(BSTP)technique.Accordingly,the necessary and sufficient conditions for verifying these two extended versions of opacity are provided as well as their complexity analysis.Finally,several examples are given to illustrate the obtained theoretical results.

关 键 词：Boolean semi-tensor product discrete-event system infinite-step opacity K-step opacity nondeterministic observation 

分 类 号：TP212[自动化与计算机技术—检测技术与自动化装置]