Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Opacity Enforcing Supervisory Control with a Priori Unknown Supervisors

Bohan Cui, Ziyue Ma, Alessandro Giua, Xiang Yin

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.

Opacity Enforcing Supervisory Control with a Priori Unknown Supervisors

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.

Paper Structure

This paper contains 18 sections, 6 theorems, 59 equations, 6 figures, 1 algorithm.

Table of Contents

  1. Introduction
  2. Motivations
  3. Status and Challenges in Opacity Supervisory Control
  4. Our Results and Contributions
  5. Organization
  6. Preliminaries
  7. System Model
  8. Supervisory Control Theory
  9. Opacity under Passive Intruders
  10. Opacity with A Priori Unknown Supervisors
  11. Information Structures with A Priori Unknown Supervisors
  12. Information Evolution from The Intruder's Perspective
  13. Information Structure of the Supervisor
  14. Synthesis of IS-Based Supervisors
  15. Supervisor Synthesis Algorithm
  16. ...and 3 more sections

Key Result

Proposition 1

Let $G$ be the system and $S: P_o({\mathcal{L}})\to\Gamma$ be a supervisor. For any string $s\in \mathcal{L}(S/G)$, we have $\blacktriangleleft$$\blacktriangleleft$

Figures (6)

  • Figure 1: Conceptual illustration of the a priori unknown opacity supervisory control setting investigated.
  • Figure 2: System $G$, where $\Sigma_o=\{u_1,u_2\}$, $\Sigma_a=\{a,b\}$, $\Sigma_c=\{u_1,u_2,u_3\}$.
  • Figure 3: Partial representation of online current-state estimator $\mathfrak{A}$.
  • Figure 4: IS-based Control Structure of $S$ in Example \ref{['example1']}.
  • Figure 5: Partial representation of structure $\mathfrak{B}$. Incomplete states are highlighted in red. An extracted control structure is highlighted in blue.
  • ...and 1 more figures

Theorems & Definitions (31)

  • Definition 1: Current-State Opacity
  • Example 1: Online Information-Flow
  • Definition 2: Controlled State Estimate
  • Example 2: Controlled State Estimate
  • Definition 3: Opacity with A Priori Unknown Supervisors
  • Example 3: Opacity-Enforcing Supervisor
  • Remark 1: Comparison with the A Priori Known Setting
  • Definition 4: Intruder State Estimator
  • Proposition 1
  • proof
  • ...and 21 more