Supervisory Control of Discrete-Event Systems for Infinite-Step Opacity

In this paper, we investigate the problem of synthesizing maximally-permissive opacity-enforcing supervisors for partially-observed discrete-event systems. We focus on a specific type of opacity called infinite-step opacity requiring that the intruder, which is modeled as a passive observer, can never determine for sure that the system is/was at a secret state for any specific instant. When the original system is verified to be non-opaque, one is interested in synthesizing a supervisor that controls the system in a least-restrictive manner such that the closed-loop system is opaque. We provide an effective approach for solving the infinite-step opacity control problem by re-formulating this problem as a two-player game over a generalized information structure that involves information delays. We show that the proposed synthesis algorithm is sound and complete, and the resulting supervisor is maximally-permissive. Most of the existing works on opacity-enforcing supervisory control only consider current-state opacity in which no delayed information is involved. Our work provides a complete solution to the infinite-step opacity control problem without any assumption on the relationship between controllable events and observable events.