Active opacity of discrete-event systems

As an essential attribute of information flow, opacity is used to characterise whether or not the intruders can infer the system secrets, which has caused considerable concern. For a complex system with multiple secret states, it is difficult to ensure the system opacity, which makes it necessary to actively control the system to enforce their opacity. In this regard, based on the framework of partially observable and controllable discrete event system, the active current-state opacity is studied. The system being actively opaque means that we can find a control for each secret state such that the behaviour of system reaching the secret state is opaque. Under such control, the intruder is unable to confirm the current state as secret state through limited observation. We construct an active-opacity verifier and derive a necessary and sufficient condition to check the active opacity of the system.