Supervisor synthesis for opacity enforcement in partially observed discrete event systems.

This article focuses on the opacity enforcement problem for discrete event systems modeled by labeled Petri nets (LPNs), where opacity ensures that secret system behaviors, represented by a subset of reachable markings, cannot be inferred by an external intruder with partial observation. To address the computational challenges of verifying opacity, the authors introduce an opacity basis reachability graph (OBRG) that abstracts system behavior without enumerating all reachable states, and develop an observer structure to identify forbidden states that indicate opacity violations. For non-opaque systems, a maximally permissive supervisor is synthesized by trimming forbidden and potential forbidden states from the observer, thereby restricting controllable events to guarantee that the controlled system is opaque. The approach is demonstrated on a manufacturing system example, showing that the OBRG significantly reduces computational complexity compared to full reachability analysis.