Opacity Enforcing Supervisory Control with a Priori Unknown Supervisors

TL;DR

This paper develops a supervisory control framework to enforce opacity in discrete-event systems when the supervisor's internal details are initially unknown but can be partially inferred by an intruder through observed control decisions.

Contribution

It introduces a novel intermediate setting for opacity enforcement where the supervisor is initially unknown but partially observable, with algorithms for synthesis without restrictions.

Findings

Algorithms for synthesizing opacity-enforcing supervisors are sound and complete.

The approach reduces the synthesis problem to a safety game based on an information-state structure.

Under finer intruder observations, the setting aligns with the standard known supervisor model.

Abstract

We investigate the enforcement of opacity in discrete-event systems via supervisory control. A system is said to be opaque if a passive intruder can never unambiguously infer whether the system is in a secret state through its observations. In this context, the intruder's knowledge about the supervisor plays a critical role in both problem formulation and solvability. Existing studies typically assume that the policy of the supervisor is either fully unknown to the intruder or fully known a priori, the latter leading to severe technical challenges and unresolved problems under incomparable observations. This paper investigates opacity supervisory control under a new intermediate information setting, which we refer to as the a priori unknown supervisor setting. In this setting, the supervisor's internal realization is not publicly available, but the intruder can partially infer its behavior by eavesdropping on the control decisions issued online during system execution. We formalize the intruder's information-flow under both observation-triggered and decision-triggered decision-issuance mechanisms and define the corresponding notions of opacity. We provide sound and complete algorithms for synthesizing opacity-enforcing supervisors without imposing any restrictions on the observable or controllable event sets. By constructing an information-state structure that embeds the supervisor's estimate of the intruder's belief, the synthesis problem is reduced to a safety game. Finally, we show that, under strictly finer intruder observations, the proposed setting coincides with the standard a priori known supervisor model.