Two transitions can share the same event label but carry different algebraic weights. The observer sees labels and weights together, so a weight can leak information a label alone would not.
● Scope of this page
Weighted automata attach an algebraic weight, typically from the max-plus (tropical) semiring, to each transition, on top of the usual event label. Weights accumulate by addition along a run, and the literature on this page works specifically with unambiguous weighted automata, where each word has at most one accepting run, so there's never more than one run's weight to combine: the semiring's max operation, which would otherwise resolve ambiguity between competing runs, plays no role here. The observer sees both the sequence of labels and the accumulated weight, so information can leak through the weight even when the label sequence alone would be safe.
The literature builds on a shared weighted-observer construction for unambiguous weighted automata, where the weight of any given run is uniquely determined by its label sequence. From there it has extended one classical opacity notion at a time (initial-state, then initial-and-final-state, then multi-step) before moving from pure verification to enforcement and, most recently, path planning.
A
Notions & Verification
The core literature for this formalism: each article extends a classical opacity notion (initial-state, initial-and-final-state, or multi-step) to unambiguous weighted automata, where the observer's information includes the accumulated transition weight, not just the event sequence. All three build on the same weighted-observer / weighted state-estimator machinery introduced by the founding article.
Initial-State Detectability and Initial-State Opacity of Unambiguous Weighted Automata
In this paper, we investigate the verification problem of initial-state detectability (I-detectability) and initial-state opacity (I-opacity) in discrete event systems modeled by unambiguous weighted automata. An I-observer is constructed so as to derive necessary and sufficient conditions for checking strong I-detectability, weak I-detectability, and I-opacity, with exponential complexity. In addition, an approach based on diagnosability analysis is proposed for verifying strong I-detectability. Compared with an I-observer-based approach, the diagnosability-based approach has a lower complexity, and in the case where all the unobservable events in an unambiguous weighted automaton are represented by a unique symbol, the diagnosability-based approach has polynomial complexity.
Verification of Initial-and-Final-State Opacity for Unambiguous Weighted Automata
Initial-and-final-state opacity (IFO) is a type of opacity that characterizes a system’s ability to prevent the disclosure of information about whether its evolution starts at an initial state and ends at a final state. In this paper, we extend the notion of IFO from the logical automata to the framework of unambiguous weighted automata (UWAs) that do not contain any cycle composed solely of unobservable events. For the verification of IFO, we first construct a labeled observer and a trellis-based initial state estimator for a given UWA. Even though the labeled observer has much smaller state space compared to the trellis-based initial state estimator, it cannot be used when the set of secret state pairs or the set of non-secret state pairs is not in the Cartesian product form. Based on the labeled observer, we present a more efficient method to verify IFO in the case when the set of non-secret state pairs is expressed as a Cartesian product, regardless of whether the set of secret state pairs is in the Cartesian product form. Furthermore, we use the labeled observer to verify initial-state opacity for a UWA.
Multi-Step State-Based Opacity for Unambiguous Weighted Machines
Zhipeng Zhang, Chengyi Xia, Guoyuan Qi, et al. · Science China Information Sciences, 67(11), article 212204, 2024 · doi.org/10.1007/s11432-023-4041-6
opacity · weighted-automata
Show abstractHide abstract
Opacity is a central concept in the issue of privacy security and has been studied extensively in fields such as finite automata, probabilistic automata, and stochastic automata. Here, we investigate the problem of validating multi-step opaque properties through unambiguous weighted machines from the perspective of cyber-physical systems. First, the notion of multi-step state-based opacity for unambiguous weighted machines is presented and defined. It includes two variants of delays with a finite K and infinite steps. Subsequently, the weighted state estimate with K (infinite)-step delay is established by abstracting the possible state set that the system could have through these weighted observations. Meanwhile, to keep the observable weighted sequence consistent between the bidirectional observers, the unobserved weights of the reverse weighted machine are assumed to be reserved. Subsequently, the existence conditions are developed, and the corresponding algorithms, termed the weighted bidirectional observer, are generalized to verify these properties. Finally, several numerical examples are illustrated to demonstrate the effectiveness of the proposed method. Taken together, the current approach will be conducive to a deep understanding of the security and privacy of cyber-physical systems.
B
Enforcement & Planning
Where category A only verifies whether a weighted system is already opaque, this category goes further and actively builds something opacity-preserving: a supervisor, a controller, or a planned trajectory, rather than just a yes/no answer.
Optimal Path Planning With Opacity-Preserving Temporal Logic Specifications Using Bipartite Synthesizers
Yiwei Zheng, Aiwen Lai, Weiyao Lan, Xiao Yu · 2023 62nd IEEE Conference on Decision and Control (CDC), pp. 7862–7867 · doi.org/10.1109/CDC49753.2023.10383570
This paper investigates an optimal planning problem with the requirement of preventing high-level mission specifications from being revealed to the intruder. We assume that the behavior of the robotic system at some specific locations is partially observable, and the intruder is modeled as a passive observer for the observable behavior and the corresponding overall transition cost of the trajectories. We first use the transition system to model the robot system. Then, we say that the transition system is LTL-based opaque with respect to high-level mission specifications if the intruder cannot infer the exact behavior of the system via the observable sequence of the system. We design a synthesizer for the product automaton of the transition system and the Büchi automaton to find the evolutions of possible reachable states. Based on the synthesizer, the corresponding run can be synthesized in which the optimality, correctness, and opacity can be guaranteed.
Enforcement of Opacity for Interval Weighted Discrete-Event System by Supervisory Control
Yiwei Zheng, Aiwen Lai, Weiyao Lan, Xiao Yu, Rong Su · IEEE Transactions on Automatic Control, 71(3), pp. 1537–1552, 2026 · doi.org/10.1109/TAC.2025.3611993
enforcement · opacity · weighted-automata
Show abstractHide abstract
This article focuses on the problem of enforcing weighted opacity for interval weighted automata, a more general class of one-clock automata, in which the transition costs are allowed to be within an interval. The objective is to develop a supervisor synthesis algorithm such that the controlled system is enforced to be weighted opaque, that is, no weighted observation can lead to the exposure of specified states. First, we propose the tree of unobservable reach to synthesize the minimal full set of control patterns that covers all possible unobservable reach for the given state. Then, we propose a new structure named weighted all-inclusive controller (W-AIC), which shows all possible reachable states according to different control patterns and presents the reachable states under certain observations. Finally, based on our proposed structure, we can discover all states in which the secrets will be inevitably revealed. By removing these states and making the W-AIC consistent, the maximally permissive supervisors that enforce the non-opaque system to generate secret-preserving languages can be synthesized. It is proved that by employing W-AICs, the enforcement weighted opacity problem can be solved when the accumulated transition costs of successive observations are restricted to be lower than the user-defined cutoff weight.