Opacity Enforcing Supervisory Control Using Nondeterministic Supervisors
Yifan Xie, Xiang Yin, Shaoyuan Li
Abstract
In this article, we investigate the enforcement of opacity via supervisory control in the context of discrete-event systems. A system is said to be opaque if the intruder, which is modeled as a passive observer, can never infer confidently that the system is at a secret state. The design objective is to synthesize a supervisor such that the closed-loop system is opaque even when the control policy is publicly known. In this article, we propose a new approach for enforcing opacity using nondeterministic supervisors. A nondeterministic supervisor is a decision mechanism that provides <italic xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">a set of control decisions</i> at each instant, and randomly picks a specific control decision from the decision set to actually control the plant. Compared with the standard deterministic control mechanism, such a nondeterministic control mechanism can enhance the plausible deniability of the controlled system as the online control decision is a random realization and cannot be implicitly inferred from the control policy. We provide a sound and complete algorithm for synthesizing a nondeterministic opacity-enforcing supervisor. Furthermore, we show that nondeterministic supervisors are strictly more powerful than deterministic supervisors in the sense that there may exist a nondeterministic opacity-enforcing supervisor even when deterministic supervisors cannot enforce opacity.