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

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 (infinity-SO) and K-step opacity (K-SO) of a DES under abnormal conditions as mentioned. In this paper, the authors extend the notions of infinity-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 infinity-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.