pith. machine review for the scientific record. sign in

arxiv: 2604.04070 · v1 · submitted 2026-04-05 · 📡 eess.SY · cs.SY

Recognition: 2 theorem links

· Lean Theorem

Opacity Enforcing Supervisory Control with a Priori Unknown Supervisors

Bohan Cui , Ziyue Ma , Alessandro Giua , Xiang Yin
Authors on Pith no claims yet

Pith reviewed 2026-05-13 17:06 UTC · model grok-4.3

classification 📡 eess.SY cs.SY
keywords opacity enforcementsupervisory controldiscrete-event systemsinformation-state structuresafety gamea priori unknown supervisorintruder belief
0
0 comments X

The pith

Opacity-enforcing supervisors can be synthesized without restrictions on observable or controllable events by reducing the problem to a safety game via an information-state structure.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

This paper shows how to enforce opacity in discrete-event systems through supervisory control when the supervisor's internal policy is not known in advance to a passive intruder. The intruder can still partially infer supervisor behavior by eavesdropping on control decisions issued online, under either observation-triggered or decision-triggered mechanisms. Sound and complete algorithms are provided that impose no restrictions on which events are observable or controllable. The key step constructs an information-state structure that embeds the supervisor's estimate of the intruder's belief, allowing the entire synthesis task to be solved as a safety game. The setting coincides with the standard known-supervisor model when the intruder has strictly finer observations.

Core claim

Opacity-enforcing supervisors can be synthesized for discrete-event systems in the a priori unknown supervisor setting by constructing an information-state structure that embeds the supervisor's estimate of the intruder's belief, thereby reducing the synthesis problem to a safety game, with sound and complete algorithms that require no restrictions on the observable or controllable event sets.

What carries the argument

An information-state structure that embeds the supervisor's estimate of the intruder's belief, which carries the argument by enabling the reduction of the opacity synthesis problem to a safety game.

Load-bearing premise

The intruder's partial inference of supervisor behavior from online control decisions under observation-triggered and decision-triggered mechanisms can be accurately captured in a finite information-state structure that enables exact reduction to a safety game.

What would settle it

Construct a small discrete-event system example with secret states, apply the synthesis algorithm, then verify whether any run allowed by the resulting supervisor lets the intruder unambiguously determine a secret state under the defined observation and decision mechanisms.

Figures

Figures reproduced from arXiv: 2604.04070 by Alessandro Giua, Bohan Cui, Xiang Yin, Ziyue Ma.

Figure 1
Figure 1. Figure 1: Conceptual illustration of the a priori unknown opacity supervisory control setting investigated. on by an intruder. From the theoretical perspective, this setting identifies a new class of opacity-enforcing supervisory control problems, where the intruder can leverage more information than in the fully unknown setting, yet incomparable to the a priori known setting. In particular, this new setting admits … view at source ↗
Figure 2
Figure 2. Figure 2: System G, where Σo = {u1, u2}, Σa = {a, b}, Σc = {u1, u2, u3}. observation-triggered or a decision-triggered decision-issuance mechanism. Formally, based on the above setting, given a supervisor S : Po(L(G)) → Γ, the information-flow of the controlled system from the intruder’s perspective is captured as the function: PS : L(S/G) → (Σϵ a × Γ ϵ ) ∗ such that (i) PS(ϵ) = (ϵ, S(ϵ)); and (ii) for any string sσ… view at source ↗
Figure 3
Figure 3. Figure 3: Partial representation of online current-state estimator [PITH_FULL_IMAGE:figures/full_fig_p007_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: IS-based Control Structure of S in Example 1. where γn is the unique control decision at I S D(α) in S. The following result establishes the meaningfulness of the proposed information structure. Specifically, it shows that, for any supervisor decoded from an IS-based structure, the observation-state reached explicitly captures both the super￾visor’s own knowledge of the plant states and its knowledge about… view at source ↗
Figure 5
Figure 5. Figure 5: Partial representation of structure B. Incomplete states are highlighted in red. An extracted control structure is highlighted in blue. so forth. This search terminates until it encounters either a state that has been previously visited, which are states {(7, {6, 7},Σ)}, {(6, {6, 7},Σ)} and {(6, {6},Σ)} in the shown part, or the unsafe observation-state, which is {(7, {7},Σ)} in the shown part. Thus, trans… view at source ↗
Figure 6
Figure 6. Figure 6: IS-based Control Structure S˜ of S in Example 1. i.e., the modified A˜ correctly computes the state estimator of the intruder under the decision-triggered mechanism. Based on the modified state estimator, the IS-based control structure, as well as the associated synthesis algorithm, is the same as the observation-triggered case. The only difference is that when defining operators NX(σ,γ)(ı) and URγ(ı), one… view at source ↗
read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper introduces an intermediate 'a priori unknown supervisor' setting for opacity enforcement in discrete-event systems, where the supervisor's internal realization is unavailable to the intruder but its online control decisions can be observed and used for partial inference. It formalizes corresponding opacity notions under observation-triggered and decision-triggered decision-issuance mechanisms, presents sound and complete synthesis algorithms that impose no restrictions on observable or controllable event sets, reduces the problem to a safety game via an information-state structure embedding the supervisor's estimate of the intruder's belief, and proves that the new setting coincides with the standard a priori known supervisor model under strictly finer intruder observations.

Significance. If the soundness and completeness claims hold, the work provides a practical middle ground between the fully known and fully unknown supervisor models that dominate the literature, enabling opacity enforcement in settings where supervisor policies are not disclosed but decisions are eavesdroppable. The restriction-free algorithms and safety-game reduction are notable strengths, as is the explicit coincidence theorem linking the new model to existing results.

major comments (2)
  1. [Section 4] Definition of the information-state structure (Section 4): the state is defined to embed only the supervisor's estimate of the intruder's belief set; it is not shown to maintain an explicit component for the set of possible supervisor realizations consistent with observed decisions. Under the a priori unknown setting this omission risks incomplete tracking of intruder belief updates when decisions are issued under either mechanism, which would render the safety-game reduction either unsound (missed opacity violations) or incomplete (valid supervisors rejected).
  2. [Theorem 5] Theorem 5 (coincidence result): the equivalence is established only under strictly finer observations; the proof does not address whether the intermediate information-state construction remains faithful for arbitrary (non-finer) observable sets, leaving the central soundness claim for the general case without direct verification.
minor comments (2)
  1. [Section 3] Notation for the two decision-issuance mechanisms is introduced without a compact tabular comparison of their information-flow differences; a small table would improve readability.
  2. [Section 5] The complexity analysis of the safety-game algorithm is stated only in terms of state-space size; explicit dependence on the number of possible supervisors (even if finite) should be added for clarity.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the thorough review and insightful comments on our work. We address each major comment below with clarifications on our constructions and proofs.

read point-by-point responses

  1. Referee: [Section 4] Definition of the information-state structure (Section 4): the state is defined to embed only the supervisor's estimate of the intruder's belief set; it is not shown to maintain an explicit component for the set of possible supervisor realizations consistent with observed decisions. Under the a priori unknown setting this omission risks incomplete tracking of intruder belief updates when decisions are issued under either mechanism, which would render the safety-game reduction either unsound (missed opacity violations) or incomplete (valid supervisors rejected).

    Authors: The information-state structure is constructed precisely to track the supervisor's estimate of the intruder's belief, with transitions defined to incorporate all possible updates arising from observed decisions under both observation-triggered and decision-triggered mechanisms. Because the supervisor is synthesizing its own (fixed but undisclosed) policy, it computes this estimate directly from the observed sequence without needing an auxiliary component enumerating possible realizations; any realization consistent with the observed decisions is already reflected in the belief-set evolution. The soundness and completeness proofs (Theorems 3 and 4) verify that the safety-game winning strategies correspond exactly to opacity-enforcing supervisors in the a priori unknown setting. We will add a short clarifying paragraph in Section 4 of the revision to make this implicit accounting explicit. revision: partial

  2. Referee: [Theorem 5] Theorem 5 (coincidence result): the equivalence is established only under strictly finer observations; the proof does not address whether the intermediate information-state construction remains faithful for arbitrary (non-finer) observable sets, leaving the central soundness claim for the general case without direct verification.

    Authors: Theorem 5 is an auxiliary result that shows coincidence with the a priori known model precisely when intruder observations are strictly finer; this is the only regime in which the two models are expected to coincide. The central soundness and completeness claims for the a priori unknown setting (Theorems 3 and 4) are established independently by showing that the information-state structure and safety-game reduction correctly capture the intruder's belief updates and yield valid supervisors for arbitrary observable and controllable sets. The proofs rely only on the definitions of the new opacity notions and the transition rules of the information-state structure, without invoking the known-supervisor model or any fineness assumption. revision: no

Circularity Check

0 steps flagged

No significant circularity: new setting and reduction defined from first principles

full rationale

The paper defines the a priori unknown supervisor setting from first principles by formalizing intruder's partial inference under observation-triggered and decision-triggered mechanisms. The information-state structure embedding the supervisor's estimate of the intruder's belief is constructed explicitly to reduce synthesis to a safety game, presented as an algorithmic step rather than a definitional identity. The coincidence result with the known-supervisor model is stated as a separate theorem under strictly finer observations, not by construction or self-citation. No self-definitional steps, fitted inputs renamed as predictions, or load-bearing self-citations appear in the derivation chain; the central claims remain independent of the inputs.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 2 invented entities

The work rests on standard discrete-event system modeling assumptions and introduces new formal definitions for the unknown-supervisor information flow; no data fitting or new physical entities are involved.

axioms (2)
  • standard math Discrete-event systems are modeled as finite automata with controllable and observable event sets
    Standard foundation of supervisory control theory invoked throughout the abstract
  • domain assumption Opacity is defined via intruder belief states over secret versus non-secret states
    Core semantic assumption for the opacity property in the new setting
invented entities (2)
  • a priori unknown supervisor setting no independent evidence
    purpose: Intermediate information model allowing partial inference from online control decisions
    Newly introduced concept that bridges fully known and fully unknown supervisor models
  • decision-triggered decision-issuance mechanism no independent evidence
    purpose: Alternative timing model for when control decisions become visible to the intruder
    New formalization of information flow alongside observation-triggered mechanism

pith-pipeline@v0.9.0 · 5546 in / 1385 out tokens · 34590 ms · 2026-05-13T17:06:19.794045+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

54 extracted references · 54 canonical work pages

  1. [1]

    Enhancement of opacity for distributed state estimation in cyber–physical systems.Automatica, 136:110087, 2022

    Liwei An and Guang-Hong Yang. Enhancement of opacity for distributed state estimation in cyber–physical systems.Automatica, 136:110087, 2022

    work page 2022

  2. [2]

    A sequence-based approach for the verification of current- state opacity in bounded discrete event systems.IEEE Transactions on Automatic Control, 2026

    Francesco Basile, Gianmaria De Tommasi, Sara Dubbioso, and Federico Fiorenza. A sequence-based approach for the verification of current- state opacity in bounded discrete event systems.IEEE Transactions on Automatic Control, 2026

    work page 2026

  3. [3]

    Now Foundations and Trends, 2021

    Jo ˜ao Carlos Basilio, Christoforos N Hadjicostis, and Rong Su.Analysis and control for resilience of discrete event systems: Fault diagnosis, opacity and cyber security. Now Foundations and Trends, 2021

    work page 2021

  4. [4]

    Supervisory control for opacity of discrete event systems

    Majed Ben-Kalefa and Feng Lin. Supervisory control for opacity of discrete event systems. In2011 49th Annual Allerton Conference on Communication, Control, and Computing (Allerton), pages 1113–1119. IEEE, 2011

    work page 2011

  5. [5]

    The complexity of diagnosability and opacity verification for Petri nets

    B ´eatrice B ´erard, Stefan Haar, Sylvain Schmitz, and Stefan Schwoon. The complexity of diagnosability and opacity verification for Petri nets. Fundamenta Informaticae, 161(4):317–349, 2018

    work page 2018

  6. [6]

    Synthesis of opaque systems with static and dynamic masks.Formal Methods in System Design, 40(1):88–115, 2012

    Franck Cassez, J ´er´emy Dubreil, and Herv ´e Marchand. Synthesis of opaque systems with static and dynamic masks.Formal Methods in System Design, 40(1):88–115, 2012

    work page 2012

  7. [7]

    Quantification of secrecy in partially observed stochastic discrete event systems.IEEE Transactions on Automation Science and Engineering, 14(1):185–195, 2016

    Jun Chen, Mariam Ibrahim, and Ratnesh Kumar. Quantification of secrecy in partially observed stochastic discrete event systems.IEEE Transactions on Automation Science and Engineering, 14(1):185–195, 2016

    work page 2016

  8. [8]

    Enforcing opacity of regular predicates on modal transition systems.Discrete Event Dynamic Systems, 25(1):251–270, 2015

    Philippe Darondeau, Herv ´e Marchand, and Laurie Ricker. Enforcing opacity of regular predicates on modal transition systems.Discrete Event Dynamic Systems, 25(1):251–270, 2015

    work page 2015

  9. [9]

    Yifan Dong, Dimitri Lefebvre, and Zhiwu Li.k-step opacity verification and enforcement of time labeled Petri net systems.IEEE Transactions on Automatic Control, 2025

    work page 2025

  10. [10]

    Opacity enforcing control synthesis

    J ´er´emy Dubreil, Philippe Darondeau, and Herv ´e Marchand. Opacity enforcing control synthesis. In9th International Workshop on Discrete Event Systems, pages 28–35. IEEE, 2008

    work page 2008

  11. [11]

    Supervi- sory control for opacity.IEEE Transactions on Automatic Control, 55(5):1089–1100, 2010

    J ´er´emy Dubreil, Philippe Darondeau, and Herv ´e Marchand. Supervi- sory control for opacity.IEEE Transactions on Automatic Control, 55(5):1089–1100, 2010

    work page 2010

  12. [12]

    Enforcement and validation (at runtime) of various notions of opacity.Discrete Event Dynamic Systems, 25(4):531–570, 2015

    Ylies Falcone and Herv ´e Marchand. Enforcement and validation (at runtime) of various notions of opacity.Discrete Event Dynamic Systems, 25(4):531–570, 2015

    work page 2015

  13. [13]

    State estimation of timed automata under partial observation

    Chao Gao, Dimitri Lefebvre, Carla Seatzu, Zhiwu Li, and Alessandro Giua. State estimation of timed automata under partial observation. IEEE Transactions on Automatic Control, 2024

    work page 2024

  14. [14]

    Strong current-state and initial-state opacity of discrete-event systems.Automatica, 148:110756, 2023

    Xiaoguang Han, Kuize Zhang, Jiahui Zhang, Zhiwu Li, and Zengqiang Chen. Strong current-state and initial-state opacity of discrete-event systems.Automatica, 148:110756, 2023

    work page 2023

  15. [15]

    Probabilistic system opacity in discrete event systems.Discrete Event Dynamic Systems, 28(2):289–314, 2018

    Christoforos Keroglou and Christoforos N Hadjicostis. Probabilistic system opacity in discrete event systems.Discrete Event Dynamic Systems, 28(2):289–314, 2018

    work page 2018

  16. [16]

    On the history of diagnosability and opacity in discrete event systems.Annual Reviews in Control, 45:257–266, 2018

    St ´ephane Lafortune, Feng Lin, and Christoforos N Hadjicostis. On the history of diagnosability and opacity in discrete event systems.Annual Reviews in Control, 45:257–266, 2018

    work page 2018

  17. [17]

    Exposure and reve- lation times as a measure of opacity in timed stochastic discrete event systems.IEEE Transactions on Automatic Control, 66(12):5802–5815, 2020

    Dimitri Lefebvre and Christoforos N Hadjicostis. Exposure and reve- lation times as a measure of opacity in timed stochastic discrete event systems.IEEE Transactions on Automatic Control, 66(12):5802–5815, 2020

    work page 2020

  18. [18]

    Privacy and safety analysis of timed stochastic discrete event systems using markovian trajectory-observers.Discrete Event Dynamic Systems, 30(3):413–440, 2020

    Dimitri Lefebvre and Christoforos N Hadjicostis. Privacy and safety analysis of timed stochastic discrete event systems using markovian trajectory-observers.Discrete Event Dynamic Systems, 30(3):413–440, 2020

    work page 2020

  19. [19]

    Opacity enforcement in discrete event systems using extended insertion functions under inserted language constraints.IEEE Transactions on Automatic Control, 68(11):6797–6803, 2023

    Xiaoyan Li, Christoforos N Hadjicostis, and Zhiwu Li. Opacity enforcement in discrete event systems using extended insertion functions under inserted language constraints.IEEE Transactions on Automatic Control, 68(11):6797–6803, 2023

    work page 2023

  20. [20]

    Ensuring confidentiality of cyber-physical systems using event-based cryptogra- phy.Information Sciences, 621:119–135, 2023

    P ´ublio M Lima, Lilian K Carvalho, and Marcos V Moreira. Ensuring confidentiality of cyber-physical systems using event-based cryptogra- phy.Information Sciences, 621:119–135, 2023. 14

    work page 2023

  21. [21]

    Opacity of discrete event systems and its applications

    Feng Lin. Opacity of discrete event systems and its applications. Automatica, 47(3):496–503, 2011

    work page 2011

  22. [22]

    Opacity enforcement via attribute-based edit functions in the presence of an intended receiver.IEEE Transactions on Automatic Control, 68(9):5646– 5652, 2022

    Rongjian Liu, Jianquan Lu, and Christoforos N Hadjicostis. Opacity enforcement via attribute-based edit functions in the presence of an intended receiver.IEEE Transactions on Automatic Control, 68(9):5646– 5652, 2022

    work page 2022

  23. [23]

    Secure- by-construction synthesis of cyber-physical systems.Annual Reviews in Control, 53:30–50, 2022

    Siyuan Liu, Ashutosh Trivedi, Xiang Yin, and Majid Zamani. Secure- by-construction synthesis of cyber-physical systems.Annual Reviews in Control, 53:30–50, 2022

    work page 2022

  24. [24]

    On approximate opacity of stochastic control systems.IEEE Transactions on Automatic Control, 2024

    Siyuan Liu, Xiang Yin, Dimos V Dimarogonas, and Majid Zamani. On approximate opacity of stochastic control systems.IEEE Transactions on Automatic Control, 2024

    work page 2024

  25. [25]

    Verification of approximate opacity via barrier certificates.IEEE Control Systems Letters, 5(4):1369–1374, 2020

    Siyuan Liu and Majid Zamani. Verification of approximate opacity via barrier certificates.IEEE Control Systems Letters, 5(4):1369–1374, 2020

    work page 2020

  26. [26]

    Compositional synthesis of opacity- preserving finite abstractions for interconnected systems.Automatica, 131:109745, 2021

    Siyuan Liu and Majid Zamani. Compositional synthesis of opacity- preserving finite abstractions for interconnected systems.Automatica, 131:109745, 2021

    work page 2021

  27. [27]

    Always guarding you: Strong initial-and-final-state opacity of discrete-event systems

    Shaowen Miao, Aiwen Lai, and Jan Komenda. Always guarding you: Strong initial-and-final-state opacity of discrete-event systems. Automatica, 173:112085, 2025

    work page 2025

  28. [28]

    Using subobservers to synthesize opacity-enforcing supervisors.Discrete Event Dynamic Systems, 32(4):611–640, 2022

    Richard Hugh Moulton, Behnam Behinaein Hamgini, Zahra Abedi Khouzani, R ˆomulo Meira-G ´oes, Fei Wang, and Karen Rudie. Using subobservers to synthesize opacity-enforcing supervisors.Discrete Event Dynamic Systems, 32(4):611–640, 2022

    work page 2022

  29. [29]

    Verifying opacity properties in security systems.IEEE Transactions on Dependable and Secure Computing, 20(2):1450–1460, 2022

    Chunyan Mu and David Clark. Verifying opacity properties in security systems.IEEE Transactions on Dependable and Secure Computing, 20(2):1450–1460, 2022

    work page 2022

  30. [30]

    Notions of centralized and decentralized opacity in linear systems.IEEE Transactions on Automatic Control, 65(4):1442–1455, 2020

    Bhaskar Ramasubramanian, Rance Cleaveland, and Steven I Marcus. Notions of centralized and decentralized opacity in linear systems.IEEE Transactions on Automatic Control, 65(4):1442–1455, 2020

    work page 2020

  31. [31]

    Enforcing current-state opacity and utility of cyber-physical systems using multi- path event routing.IEEE Transactions on Automatic Control, 2026

    Lucas NR Reis, Lilian K Carvalho, and Marcos V Moreira. Enforcing current-state opacity and utility of cyber-physical systems using multi- path event routing.IEEE Transactions on Automatic Control, 2026

    work page 2026

  32. [32]

    Joint opacity and opacity against state-estimate-intersection-based intrusion of discrete- event systems.Automatica, 176:112136, 2025

    K Ritsuka, St ´ephane Lafortune, and Feng Lin. Joint opacity and opacity against state-estimate-intersection-based intrusion of discrete- event systems.Automatica, 176:112136, 2025

    work page 2025

  33. [33]

    Opacity- enforcing supervisory strategies via state estimator constructions.IEEE Transactions on Automatic Control, 57(5):1155–1165, 2011

    Anooshiravan Saboori and Christoforos N Hadjicostis. Opacity- enforcing supervisory strategies via state estimator constructions.IEEE Transactions on Automatic Control, 57(5):1155–1165, 2011

    work page 2011

  34. [34]

    Verification of infinite-step opacity and complexity considerations.IEEE Transactions on Automatic Control, 57(5):1265–1269, 2011

    Anooshiravan Saboori and Christoforos N Hadjicostis. Verification of infinite-step opacity and complexity considerations.IEEE Transactions on Automatic Control, 57(5):1265–1269, 2011

    work page 2011

  35. [35]

    Verification of initial-state opacity in security applications of discrete event systems

    Anooshiravan Saboori and Christoforos N Hadjicostis. Verification of initial-state opacity in security applications of discrete event systems. Information Sciences, 246:115–132, 2013

    work page 2013

  36. [36]

    Existence conditions for confidentiality in discrete-event systems

    Bryony H Schonewille and Karen Rudie. Existence conditions for confidentiality in discrete-event systems. In2024 American Control Conference (ACC), pages 5412–5418. IEEE, 2024

    work page 2024

  37. [37]

    Synthesis of opacity-enforcing winning strategies against colluded op- ponent

    Chongyang Shi, Abhishek N Kulkarni, Hazhar Rahmani, and Jie Fu. Synthesis of opacity-enforcing winning strategies against colluded op- ponent. In2023 62nd IEEE Conference on Decision and Control (CDC), pages 7240–7246. IEEE, 2023

    work page 2023

  38. [38]

    Privacy-preserving co-synthesis against sensor–actuator eavesdropping intruder.Automat- ica, 150:110860, 2023

    Ruochen Tai, Liyong Lin, Yuting Zhu, and Rong Su. Privacy-preserving co-synthesis against sensor–actuator eavesdropping intruder.Automat- ica, 150:110860, 2023

    work page 2023

  39. [39]

    A formula for the supremal con- trollable and opaque sublanguage arising in supervisory control.SICE Journal of Control, Measurement, and System Integration, 1(4):307–311, 2008

    Shigemasa Takai and Yusuke Oka. A formula for the supremal con- trollable and opaque sublanguage arising in supervisory control.SICE Journal of Control, Measurement, and System Integration, 1(4):307–311, 2008

    work page 2008

  40. [40]

    Verification of k-step and infinite- step opacity of bounded labeled petri nets.Automatica, 140:110221, 2022

    Yin Tong, Hao Lan, and Carla Seatzu. Verification of k-step and infinite- step opacity of bounded labeled petri nets.Automatica, 140:110221, 2022

    work page 2022

  41. [41]

    Verification of state-based opacity using petri nets.IEEE Transactions on Automatic Control, 62(6):2823–2837, 2017

    Yin Tong, Zhiwu Li, Carla Seatzu, and Alessandro Giua. Verification of state-based opacity using petri nets.IEEE Transactions on Automatic Control, 62(6):2823–2837, 2017

    work page 2017

  42. [42]

    Current- state opacity enforcement in discrete event systems under incomparable observations.Discrete Event Dynamic Systems, 28(2):161–182, 2018

    Yin Tong, Zhiwu Li, Carla Seatzu, and Alessandro Giua. Current- state opacity enforcement in discrete event systems under incomparable observations.Discrete Event Dynamic Systems, 28(2):161–182, 2018

    work page 2018

  43. [43]

    Synthesis of dynamic masks for information-theoretic opacity in stochastic systems

    Sumukha Udupa, Chongyang Shi, and Jie Fu. Synthesis of dynamic masks for information-theoretic opacity in stochastic systems. In Proceedings of the ACM/IEEE 16th International Conference on Cyber- Physical Systems (with CPS-IoT Week 2025), pages 1–12, 2025

    work page 2025

  44. [44]

    Integrat- ing obfuscation and control for privacy.IEEE Transactions on Automatic Control, 2025

    Andrew Wintenberg, Necmiye Ozay, and St ´ephane Lafortune. Integrat- ing obfuscation and control for privacy.IEEE Transactions on Automatic Control, 2025

    work page 2025

  45. [45]

    Supervisory control of discrete-event systems: A brief history.Annual Reviews in Control, 45:250–256, 2018

    Walter Murry Wonham, Kai Cai, and Karen Rudie. Supervisory control of discrete-event systems: A brief history.Annual Reviews in Control, 45:250–256, 2018

    work page 2018

  46. [46]

    Opacity enforcing supervisory control using nondeterministic supervisors.IEEE Transactions on Automatic Control, 67(12):6567–6582, 2021

    Yifan Xie, Xiang Yin, and Shaoyuan Li. Opacity enforcing supervisory control using nondeterministic supervisors.IEEE Transactions on Automatic Control, 67(12):6567–6582, 2021

    work page 2021

  47. [47]

    Secure-by- construction controller synthesis for stochastic systems under linear temporal logic specifications

    Yifan Xie, Xiang Yin, Shaoyuan Li, and Majid Zamani. Secure-by- construction controller synthesis for stochastic systems under linear temporal logic specifications. In2021 60th IEEE Conference on Decision and Control (CDC), pages 7015–7021. IEEE, 2021

    work page 2021

  48. [48]

    Secure your intention: On notions of pre- opacity in discrete-event systems.IEEE Transactions on Automatic Control, 68(8):4754–4766, 2022

    Shuo Yang and Xiang Yin. Secure your intention: On notions of pre- opacity in discrete-event systems.IEEE Transactions on Automatic Control, 68(8):4754–4766, 2022

    work page 2022

  49. [49]

    A uniform approach for synthesiz- ing property-enforcing supervisors for partially-observed discrete-event systems.IEEE Transactions on Automatic Control, 61(8):2140–2154, 2015

    Xiang Yin and St ´ephane Lafortune. A uniform approach for synthesiz- ing property-enforcing supervisors for partially-observed discrete-event systems.IEEE Transactions on Automatic Control, 61(8):2140–2154, 2015

    work page 2015

  50. [50]

    A new approach for the verification of infinite-step and k-step opacity using two-way observers.Automatica, 80:162–171, 2017

    Xiang Yin and St ´ephane Lafortune. A new approach for the verification of infinite-step and k-step opacity using two-way observers.Automatica, 80:162–171, 2017

    work page 2017

  51. [51]

    On approximate opacity of cyber-physical systems.IEEE Transactions on Automatic Control, 66(4):1630–1645, 2021

    Xiang Yin, Majid Zamani, and Siyuan Liu. On approximate opacity of cyber-physical systems.IEEE Transactions on Automatic Control, 66(4):1630–1645, 2021

    work page 2021

  52. [52]

    En- forcement of opacity for interval weighted discrete-event system by supervisory control.IEEE Transactions on Automatic Control, 2025

    Yiwei Zheng, Aiwen Lai, Weiyao Lan, Xiao Yu, and Rong Su. En- forcement of opacity for interval weighted discrete-event system by supervisory control.IEEE Transactions on Automatic Control, 2025

    work page 2025

  53. [53]

    Secure-by-construction synthesis for control systems.IEEE Transactions on Automatic Control, 2025

    Bingzhuo Zhong, Siyuan Liu, Marco Caccamo, and Majid Zamani. Secure-by-construction synthesis for control systems.IEEE Transactions on Automatic Control, 2025

    work page 2025

  54. [54]

    Online verification of k- step opacity by petri nets in centralized and decentralized structures

    Guanghui Zhu, Zhiwu Li, and Naiqi Wu. Online verification of k- step opacity by petri nets in centralized and decentralized structures. Automatica, 145:110528, 2022. APPENDIX Proof of Proposition 1 Proof.The conclusions for the first and third components are straightforward according to the definition of the intruder state estimator. We now prove the seco...

    work page 2022