1Opacity-Enforcing Supervisory Strategies via State Estimator Constructions

Abstract—State-based notions of opacity, such as initial-state opacity and infinite-step opacity, emerge as key properties in numerous security applications of discrete event systems. We consider systems that are modeled as partially observed non-deterministic finite automata and tackle the problem of constructing a minimally restrictive opacity-enforcing supervisor (MOES), which limits the system’s behavior within some pre-specified legal behavior while enforcing initial-state opacity or infinite-step opacity requirements. We characterize the solution to MOES, under some mild assumptions, in terms of the supremal ele-ment of certain controllable, normal, and opaque languages. We also show that this supremal element always exists and that it can be implemented using state estimators. The result is a supervisor that achieves conformance to the pre-specified legal behavior while enforcing initial-state opacity by disabling, at any given time, a subset of the controllable system events, in a way that minimally restricts the range of allowable system behavior. Although infinite-step opacity cannot be easily translated to language-based opacity, we show that, by using a finite bank of supervisors, the aforementioned approach can be extended to enforce infinite-step opacity in a minimally restrictive way