Instead of one observer with one view, the system's behavior is split across several observation sites, which may or may not coordinate, and may communicate over channels with delays or losses. Opacity now has to be defined with respect to this whole architecture, not just a single observer.
● Scope of this page
Every other page in this index assumes a single observer with one fixed view of the system. This page covers what happens once that assumption is dropped: several observation sites, each seeing only part of the system's behavior, which may or may not coordinate with each other, and whose messages to a coordinator may be delayed, lost, or arrive out of order. The underlying system itself stays finite-state, as in the classical setting; what changes is the observation architecture.
This includes decentralized opacity (multiple independent or coordinating intruders), networked opacity (communication delays and losses between the system and its observer), and modular opacity (a large system decomposed into interacting components, verified or enforced component-by-component rather than on the full product). A much smaller literature than the classical single-observer setting, and noticeably newer.
A
Decentralized Systems
The system is watched by several independent observers, each with its own partial view, who may or may not be allowed to coordinate or combine what they've each seen. Opacity has to be redefined with respect to the whole observation architecture (can any single observer, or any coalition of them, deduce the secret?), not just a lone intruder.
Concurrent Secrets
Eric Badouel, Marek Bednarczyk, Andrzej Borzyszkowski, Benoît Caillaud, Philippe Darondeau · Discrete Event Dynamic Systems, 17(4), pp. 425–446, 2007 · doi.org/10.1007/s10626-007-0020-5 · research report: HAL: inria-00070249 (INRIA RR-5771, 2005)
distributed · opacity
Show abstractHide abstract
Given a finite state system with partial observers and for each observer, a regular set of trajectories which we call a secret, we consider the question whether the observers can ever find out that a trajectory of the system belongs to some secret. We search for a regular control on the system, enforcing the specified secrets on the observers, even though they have full knowledge of this control. We show that an optimal control always exists although it is generally not regular. We state sufficient conditions for computing a finite and optimal control of the system enforcing the concurrent secret as desired. We briefly point to applications.
In this paper, we investigate opacity of discrete event systems in a decentralized framework with several agents, each of them performing its observation of the system. We consider two cases, one without coordination among agents and one with coordination. Both cases are useful because many systems used today are distributed over a network, some with agents coordinating among themselves and some without. We introduce general definitions of decentralized opacity for both cases. The definitions are based on languages. Therefore, they are flexible and can include other properties of discrete event systems as special cases. In particular, we show that co-observability used in supervisory control is a special case of decentralized opacity. We illustrate the usefulness of decentralized opacity by applying it in solving an interesting security problem in computer systems.
Current-State Opacity Enforcement in Discrete Event Systems Under Incomparable Observations
In this paper we tackle the opacity enforcement problem in discrete event systems using supervisory control theory. In particular, we consider the case where the intruder and the supervisor may observe different sets of events and neither of these sets needs to be contained in the other one. Moreover, there may be controllable events that cannot be observed by the supervisor. We propose a finite structure, called an augmented I-observer, to characterize the strings that will not leak the secret. Based on such a structure, a locally optimal supervisor enforcing current-state opacity is designed.
Synthesis of Insertion Functions to Enforce Decentralized and Joint Opacity Properties of Discrete-Event Systems
Opacity is a confidentiality property that characterizes the non-disclosure of specified secret information of a system to an outside observer. In this paper, we consider the enforcement of opacity within the discrete-event system formalism in the presence of multiple intruders. We study two cases, one without coordination among the intruders and the other with coordination. We propose appropriate notions of opacity corresponding to the two cases, respectively, and propose enforcement mechanisms for these opacity properties based on the implementation of insertion functions, which manipulates the output of the system by inserting fictitious observable events whenever necessary. The insertion mechanism is adapted to the decentralized framework to enforce opacity when no coordination exists. Furthermore, we present a coordination and refinement procedure to synthesize appropriate insertion functions to enforce opacity when intruders may coordinate with each other by following an intersection-based coordination protocol. The effectiveness of the proposed opacity-enforcement approaches is validated through illustrative examples.
Notions of Centralized and Decentralized Opacity in Linear Systems
Bhaskar Ramasubramanian, Rance Cleaveland, Steven I. Marcus · IEEE Transactions on Automatic Control, 65(4), pp. 1442–1455, 2020 · doi.org/10.1109/TAC.2019.2920837 · preprint: arXiv:1903.06869
Extends k-ISO opacity of linear systems to multiple adversaries, with notions that vary with the presence of a centralized coordinator and with collusion; a graph-theoretic condition characterizes non-opacity under collusion.
We formulate notions of opacity for cyberphysical systems modeled as discrete-time linear time-invariant systems. A set of secret states is k-ISO with respect to a set of nonsecret states if, starting from these sets at time 0, the outputs at time k are indistinguishable to an adversarial observer. Necessary and sufficient conditions to ensure that a secret specification is k-ISO are established in terms of sets of reachable states. We also show how to adapt techniques for computing underapproximations and overapproximations of the set of reachable states of dynamical systems in order to soundly approximate k-ISO. Furthermore, we provide a condition for output controllability, if k-ISO holds, and show that the converse holds under an additional assumption. We extend the theory of opacity for single-adversary systems to the case of multiple adversaries and develop several notions of decentralized opacity. We study the following scenarios: first, the presence or lack of a centralized coordinator, and, second, the presence or absence of collusion among adversaries. In the case of colluding adversaries, we derive a condition for nonopacity that depends on the structure of the directed graph representing the communication between adversaries. Finally, we relax the condition that the outputs be indistinguishable and define a notion of ϵ-opacity, and also provide an extension to the case of nonlinear systems.
Online Verification of K-Step Opacity by Petri Nets in Centralized and Decentralized Structures
This paper presents an online approach to deal with the problem of state-based K-step opacity of a discrete event system modeled with labeled Petri nets. The secret states can be described by a set of either markings or generalized mutual exclusion constraints (GMECs), which is more general than the existing approaches in which the secret states are characterized by GMECs only. We formulate an integer linear programming (ILP) model to find a marking outside the set of secret states from each of the K-delayed state estimates, avoiding a complete enumeration of reachability set. Based on the ILP model, an online algorithm is developed to verify K-step opacity of an observation (i.e., an observed sequence). As an extension of K-step opacity, we define the notion of joint K-step opacity in a decentralized structure with two local sites and extend the proposed algorithm to verify the joint K-step opacity of an observation. In addition, the relationship between joint K-step opacity and K-step opacity is formally discussed.
Distributed Secret Securing in Discrete-Event Systems
In this paper, we study a security problem of protecting secrets in distributed systems. Specifically, we employ discrete-event systems to describe the structure and behaviour of distributed systems, in which global secret information is separated into pieces and stored in local component agents. The goal is to prevent such secrets from being exposed to intruders by imposing appropriate protection measures. This problem is formulated as to ensure that at least one piece of every distributed global secret is secured by a required number of protections, while the overall cost to apply protections is minimum. We first characterize the solvability of this security problem by providing a necessary and sufficient condition, and then develop an algorithm to compute a solution based on the supervisory control theory of discrete-event systems. Finally, we illustrate the effectiveness of our solution with an example system comprising distributed databases.
B
Modular Systems
A single system, but built by composing several local components (a product or synchronous composition of automata), and analyzed component-by-component rather than on the fully composed whole. The central question is how to check or enforce opacity without ever constructing that full composition, whose state space can be exponential in the number of components. Results here range from complexity lower bounds (showing the problem is provably harder modularly than centrally) to compositional algorithms, abstraction-based reductions, and GNN-based acceleration.
Reduced-Complexity Verification for Initial-State Opacity in Modular Discrete Event Systems
In this paper, we propose and analyze reduced-complexity methodologies for verifying initial-state opacity in modular discrete event systems. Initial-state opacity requires that the membership of the system initial state to a given set of secret statesS remains opaque (uncertain) to an intruder who has complete knowledge of the system model and observes system activity through some natural projection map. In the modular setting we consider, the given system is modeled as a composition (synchronous product) of M modules [G1, G2, …, GM] where each module Gi is a non-deterministic finite automaton with Ni states with the set of secret states S is of the form S = [(x1, x2, …, xM)|xi ∈ Si], where Si is the set of secret states for module Gi. Assuming that the pairwise shared events are pairwise observable and that the intruder observes events that are observable in at least one module, we provide a modular algorithm for verifying initial-state opacity with O(MNM−12N2) state and time complexity, where N = maxiNi. This is a considerable reduction compared to the O(2(NM)2) state and time complexity of the centralized verification method, which verifies initial-state opacity by considering the composed system as a monolithic system.
Complexity of Detectability, Opacity and A-Diagnosability for Modular Discrete Event Systems
Modular discrete event systems are modeled as a parallel composition of finite automata. While deciding weak detectability, opacity, and A-diagnosability for monolithic systems is PSPACE-complete, the complexity for modular systems is unknown. We show that for modular systems the problems are EXPSPACE-complete, and hence there is neither a polynomial-time nor a polynomial-space algorithm solving them. While the upper bound is a natural modification of the PSPACE algorithms for monolithic systems, the lower bound requires a novel and nontrivial construction. We further discuss a case where the complexity drops to PSPACE-complete.
Current-State Opacity Verification in Modular Discrete Event Systems
In this paper we address the opacity verification problem in modular discrete event systems. We assume that the system is composed by several components that are modeled by deterministic finite automata and there is one intruder. The notion of current-state opacity in modular systems is defined. Rather than constructing the modular system through parallel composition and its observer, we show that current-state opacity of modular systems can be locally determined, i.e., determined by opacity of its components.
In discrete-event systems, the opacity of a secret ensures that some behaviors or states cannot be inferred with certainty from partial observation of the system. Enforcing opacity in a discrete-event system, encoded by a finite labelled transition system (LTS), is a way to avoid information leakage. Checking opacity is decidable but costly (EXPTIME in the worst cases). This paper addresses opacity for modular systems in which every module, represented by an LTS, has to protect its own secret (a set of secret states S) w.r.t. a local attacker. Once the system is composed, we assume a coalition between the attackers that share their local view (called the global attacker). Assuming the global attacker can observe all interactions between modules, we provide a reduced-complexity opacity verification technique and an algorithm for constructing local controllers that enforces opacity for each secret separately.
Current-State Opacity and Initial-State Opacity of Modular Discrete Event Systems
The verifications of current-state opacity (CSO) and initial-state opacity (ISO) in discrete event systems (DESs) both suffer from the curse of dimensionality, as these issues were proved to be PSPACE-complete. Hence, how to reduce the state space is crucial. In this paper, we investigate CSO and ISO in modular DESs, which consist of several individual components. Necessary and sufficient conditions of CSO and ISO for modular DESs are derived under the assumption that all synchronous events are observable by each component of modular DESs. Moreover, we prove that the initial state estimator of modular system is isomorphic to the synchronous composition of initial state estimators for individual components. These results offer us the opportunity to reduce the complexity in verifying the opacity of modular DESs.
State-Labeled Safety Analysis of Modular Observers for Opacity Verification
Bengt Lennartson, Mona Noori-Hosseini, Christoforos N. Hadjicostis · IEEE Control Systems Letters, 6, pp. 2936–2941, 2022 · doi.org/10.1109/LCSYS.2022.3176531
distributed · modular · opacity
Show abstractHide abstract
Verification of opacity and anonymity for modular systems is in this letter formulated as safety analysis of local observers with state labels. A unified modeling strategy is presented based on a generalized synchronous composition, including both shared and non-shared state labels. The proposed modeling approach is shown to be flexible and general, making it possible to solve both local, global, and arbitrarily joint secret state problems simultaneously. A scalable modular n-floor, m-elevator security benchmark problem is also formulated and evaluated by two powerful safety analysis methods. It is shown that current-state opacity for non-trivial complex systems involving more than 1025 observer states can be verified in about one second.
Opacity Verification for a Class of Modular Discrete Event Systems
The verification of opacity of discrete event systems (DESs) is subjected to the curse of dimensionality because this issue has been proven to be EXPSPACE-complete. Therefore, how to improve the efficiency of opacity verification in DESs is crucial. We discuss in this paper the verification of several classes of opacity in modular discrete event systems (modular DESs) formalized as Cartesian composition of deterministic finite state automata. We derive the sufficient and necessary conditions for these opacity notions in modular DESs. Many examples are also used to explain the results obtained in this article. These results greatly reduce the computational complexity of verifying the opacity for modular DESs.
Don't Compose Blindly: Adaptive GNNs for Opacity Verification in Modular Discrete-Event Systems
Sarra Habbachi, Imene ben Hafaiedh, Zhiwu Li · 18th International Conference on Agents and Artificial Intelligence (ICAART 2026), Volume 5, pp. 4372–4379 · doi.org/10.5220/0014418100004052
distributed · modular · opacity
Show abstractHide abstract
Language-based opacity verification in modular discrete-event systems (DESs) is hindered by state-space explosion when constructing a global observer. Iterative compositional methods alleviate this issue but often rely on fixed composition sequences, leading to redundant computations when modules are locally non-opaque. We propose an adaptive framework using Graph Neural Networks (GNNs) to dynamically select optimal composition sequences. The GNN prioritizes compositions based on structural features, including inter-module coupling, transition patterns, and secret state distributions, reducing unnecessary computation. Experiments on synthetic and real-world benchmarks demonstrate an average speedup of 15.7×, a 68% reduction in compositions, and 99.8% verification accuracy. This approach enables scalable opacity verification for systems with up to 30 modules.
C
Networked Systems
A single system whose events are transmitted to the observer over a communication channel that may be insecure, introduce delays, or lose messages. The intruder exploits these channel properties to learn more than a local observer would, and the defender must account for all admissible channel behaviors when checking or enforcing opacity.
Initial-State Estimation of Multi-Channel Networked Discrete Event Systems
Initial-state estimation consists in determining the initial state of the system based on the observation from the system and the system structure. It is the basis for many problems in security applications, such as opacity, detectability and supervisory control. However, when it comes to cyber-physical systems (CPS) communication delays and losses are inevitable. In this letter, we study the initial-state estimation problem in a CPS that is modeled with a multi-channel networked discrete event system (NDES). In practice, the system is usually distributed over several locations, and the communication between the system and an agent (e.g., intruder, observer, supervisor) is carried out via a shared network, in which communication delays and losses may happen. In multi-channel NDESs, even when the first-in first-out rule is satisfied in each channel, the order of events received by the agent may still be shuffled due to random communication delays in each channel. To address these new challenges, we formalize the initial-state estimation problem in multi-channel NDESs and a networked initial-state estimator is proposed to generate the exact initial-state estimate.
Information Control in Networked Discrete Event Systems and Its Application to Battery Management Systems
Feng Lin, Le Yi Wang, Wen Chen, Weilin Wang, Fei Wang · Discrete Event Dynamic Systems, 30(2), pp. 243–268, 2020 · doi.org/10.1007/s10626-019-00303-y
distributed · networked · opacity
Show abstractHide abstract
Opacity is an important property in control of information flow among networked agents. In this paper, we investigate information control problems in networked discrete event systems using opacity. In a networked discrete event system, communication among agents is via a shared communication network. Since delays and losses are unavoidable in networked discrete event systems, they must be considered in investigating opacity. We call opacity under communication delays and losses network opacity. We first define three network opacities: strong network opacity, weak network opacity, and network non-opacity. We derive necessary and sufficient conditions for network opacities and develop methods to check network opacities. We then apply network opacity to solve a problem in battery management systems.
Opacity of Networked Supervisory Control Systems Over Insecure Communication Channels
Shuo Yang, Junyao Hou, Xiang Yin, Shaoyuan Li · IEEE Transactions on Control of Network Systems, 8(2), pp. 884–896, 2021 · doi.org/10.1109/TCNS.2021.3050131 · conference precursor: “Opacity of Networked Supervisory Control Systems Over Insecure Multiple Channel Networks”, 58th IEEE Conference on Decision and Control (CDC 2019), pp. 7641–7646 · doi.org/10.1109/CDC40024.2019.9030235
distributed · networked · opacity
Show abstractHide abstract
In this article, we investigate security and privacy issues in networked supervisory control systems over multiple channel networks. We consider a networked discrete-event system controlled by a supervisor that receives information from sensors and sends control decisions to actuators via observation channels and control channels, respectively. The security problem is studied for the scenario where some of the communication channels are insecure in the sense there exists a passive intruder (eavesdropper) that can access the information-flow in those insecure communication channels. We adopt the concept of opacity, an information flow security property, to characterize the security status of the supervisory control system. Specifically, we assume that the system has a secret and the system is said to be opaque if the intruder can never determine the secret of the system unambiguously based on the information-flow in the insecure channels. We consider the notions of current-state opacity, K-step opacity, and infinite-step opacity in the networked control setting. New network observers are proposed to estimate the state of the system with two-side incomparable channel information. We show that the opacity verification problems for the networked setting can be effectively solved using the proposed network observers.
Opacity of Networked Discrete Event Systems
Jingkai Yang, Weilin Deng, Daowen Qiu, Cheng Jiang · Information Sciences, 543, pp. 328–344, 2021 · doi.org/10.1016/j.ins.2020.07.017 · conference version: Jingkai Yang, Weilin Deng, Cheng Jiang, Daowen Qiu · 2019 IEEE 58th Conference on Decision and Control (CDC), pp. 6736–6741 · doi.org/10.1109/CDC40024.2019.9030250
distributed · networked · opacity
Show abstractHide abstract
Opacity is an important information-flow property, which is used to characterize whether or not the secrets of system have been leaked to the intruders. Over the past ten years, opacity of discrete event systems (DESs) modeled as automata and Petri nets have been well investigated under the assumption that the communication channels between systems and intruders are perfect. However, in networked discrete event systems (NDESs), the DESs run in a shared network, and the communication delays and losses are inevitable usually. In this paper, we investigate the problems of opacity in the framework of NDESs. We formulate four kinds of opacity for NDESs, including current-state opacity, initial-state opacity, initial-final-state opacity, and K-step opacity. We also present the verification algorithms for these notions. We extend the notions of opacity in classical DESs, that is, if the communication delays and losses disappear, then these new notions would reduce to their classical counterparts. A number of examples are provided to illustrate the results obtained.
Networked Opacity for Finite State Machine with Bounded Communication Delays
Networked finite state machines consider the delay factor in real-time communication networks, and the security has become an important research topic in cyber-physical systems (CPSs). In this brief paper, we explore the networked opacity of finite state machine with bounded communication delays. Firstly, the networked opacity is proposed from the perspective of security state reachability, and by use of the Boolean matrix semi-tensor product (STP), we introduce the reachability matrix with respect to all feasible events to give the current dynamics with bounded communication delays. Subsequently, based on the algebraic equation, we continue to discuss the corresponding current estimate of possible reachable states, which can be calculated by a matrix approach. Then, a more simple and effective verification criterion of networked opacity is derived by some matrix manipulations. Finally, a typical example is provided to validate the impact of communication delay on the opacity of CPSs, and our results contribute to deeply understanding the information security in the area of CPSs.
Enhancement of Opacity for Distributed State Estimation in Cyber-Physical Systems
The estimation network itself is the attack surface: nodes broadcast their estimates and an intruder eavesdrops on a subset. The enhancement mechanism keeps opacity without degrading estimation accuracy.
Opacity, a confidentiality property that characterizes whether a “secret” of a system can be inferred by an outside intruder, is an increasing concern in cyber–physical systems (CPSs). The existing distributed estimation algorithms allow each node to broadcast its explicit state information to its neighbors, which results in the disclosure of CPS’s secret state. To meet the confidentiality requirement, this paper formulates a new framework for opacity for distributed state estimation. Two opacity-enhancing algorithms are proposed against the intruder models with different eavesdropping capacities for a subset of nodes. Necessary and sufficient conditions to ensure that a secret state is opaque are established in terms of the rank of constructed structural matrices of the eavesdropped nodes. Moreover, it is shown that the use of enhancement mechanism does not compromise the estimation accuracy. The framework of opacity is further extended to the case of measurement noises.
Enforcing Opacity in Discrete Event Systems via Delayed Observations
Jiwei Wang, Simone Baldi, Wenwu Yu, Xiang Yin · IEEE Control Systems Letters, 9, pp. 2411–2416, 2025 · doi.org/10.1109/LCSYS.2025.3623658
distributed · networked · opacity
Show abstractHide abstract
Artificially introducing a delay in the observations of a system can be an effective mechanism to mask the system itself, with the goal to increase its opacity and thus its security. This letter investigates opacity in discrete event systems with delayed observations. We focus on two questions: how to verify opacity under delayed observations, and how to synthesize sensor activation policies that guarantee opacity under such delayed conditions. To address these questions, we first introduce the definition of opacity under delayed observation and develop a corresponding verification method. We then extend such analysis tool into a synthesis tool by proposing an optimization approach for designing sensor activation policies guaranteeing opacity under delayed observations. An example is used to illustrate the analysis and synthesis procedures.
Construction of Decentralized State Estimator Based on Partially Ordered Observation Sequences
Dajiang Sun, Christoforos N. Hadjicostis, Zhiwu Li · IEEE Transactions on Automatic Control, 71(5), pp. 3335–3342, 2026 · doi.org/10.1109/TAC.2025.3633985 · preprint: arXiv:2502.10367, "Decentralized State Estimation and Opacity Verification Based on Partially Ordered Observation Sequences"
distributed · networked · opacity
Show abstractHide abstract
In this article, we investigate state estimation and estimator construction problems within a decentralized observation architecture. Specifically, we consider a discrete event system whose behavior is recorded by a set of observation sites. These sites transmit their partially ordered sequences of observations to a coordinator whenever a synchronization occurs. To properly analyze the system behavior from the coordinator's viewpoint, we first introduce the notion of a complete synchronizing sequence structure (CSS structure), which concisely captures the state evolution of each system state upon different information provided by the observation sites. Based on the CSS structure, we then construct corresponding current- and initial-state estimators for offline state estimation at the coordinator. In particular, we discuss how to verify initial-state opacity and diagnosability at the coordinator, as well as a novel opacity notion, namely current-state-at-synchronization opacity.
Verification and Enforcement of K-Step Mutual Opacity of Networked Systems
Robia Arif, Gaiyun Liu, Abdulrahman Al-Ahmari, Zhiwu Li · Information Sciences, 748, article 123497, 2026 · doi.org/10.1016/j.ins.2026.123497
distributed · networked · opacity
Show abstractHide abstract
We delve into the verification and enforcement problem of K-step mutual opacity of discrete-event systems, which is a crucial aspect of information flow privacy. Specifically, K-step mutual opacity describes a scenario in which the secret states cannot be mutually revealed within K steps of observations by two or more adversaries. For the sake of simplicity, suppose that two agents engage in strategic competition in a system where each aims to reveal the other’s secrets while concealing its own. These agents partially observe system evolution and influence the behavior of the system by enabling or disabling events from their controllable event sets. A separation principle is used to construct state estimates, precisely for a two-way observer, that merge both the past and future information flow into one structure. Furthermore, the two-way observer supports a more efficient verification algorithm for K-step mutual opacity. For the enforcement of K-step mutual opacity, the analyses unfold in distinct scenarios. Primarily, agents are passive, in which the system is connected with a global controller capable of ensuring mutual opacity between the agents within K observations. This controller prevents the leakage of secret information from one adversary to the other. Moreover, we explore the feasibility of synthesizing separate controllers for the agents. The objective is to devise a winning state-dependent control strategy that ensures an agent consistently uncovers the secret of the other while securing its own. This research illuminates the intricate dynamics of information flow privacy in a competitive environment, providing insights that facilitate the development of effective privacy-preserving mechanisms in complex networked systems.
Enforcing Current-State Opacity and Utility of Cyber-Physical Systems Using Multipath Event Routing
Lucas N. R. Reis, Lilian K. Carvalho, Marcos V. Moreira · IEEE Transactions on Automatic Control, 71(6), pp. 4208–4214, 2026 · doi.org/10.1109/TAC.2026.3653255
Cross-listed as a networked-systems technique: opacity and utility are enforced over the channel to a remote receiver, using multipath event routing on top of event replacements.
Several strategies have been proposed in the literature to ensure data security in cyber-physical systems abstracted as networked discrete-event systems, such as enforcing opacity by using obfuscation policies. In these cases, if it is considered the existence of an intended receiver, the useful information can be hidden from him/her. This problem becomes worse when the confidentiality of the data must be ensured, i.e., when the intended receiver must always know the system current state from the observation of the obfuscated transmitted sequence. In this article, we propose a defense strategy to enforce current-state opacity using an obfuscation policy based on event replacements that also ensures the utility of the transmitted information. The notion of utility used, called current-state utility, is associated with the ability of the intended receiver to be always certain of the system current state. In order to implement the defense strategy, a multipath event routing technique is considered.