Research on the Opacity of Discrete Event Systems based on Nondeterministic Observations

In real-world systems, event observability is nondeterministic due to factors such as sensor malfunctions, sensing constraints, and network packet losses. This makes the opacity problem of discrete event systems (DES) extremely complicated. The nondeterministic observability of events means that the same event string in a DES may yield multiple observations, and the same event may have different observations under distinct states. Aiming at the opacity verification of DES under nondeterministic observations, this paper proposes a verification method to determine whether the system is opaque. First, a nondeterministic observation mapping mechanism is introduced to formalize the opacity of DES with nondeterministic observations. Then, a current state estimation observer is constructed to verify the system opacity under nondeterministic observations. Finally, the necessary and sufficient conditions for the system opacity under nondeterministic observations are derived, and the effectiveness of the theoretical results is illustrated through a typical example. Compared to existing methods, ours achieves lower time complexity and remains applicable to traditional natural projection models.