Enforcement of Opacity for Interval Weighted Discrete-Event System by Supervisory Control

• 成果类型: Article
• 署名作者: Zheng, Yiwei; Lai, Aiwen; Lan, Weiyao; Yu, Xiao; Su, Rong
• 署名单位: Xiamen University; Xiamen University; Xiamen University; Nanyang Technological University
• 刊物名称: IEEE TRANSACTIONS ON AUTOMATIC CONTROL
• ISSN/ISSBN: 0018-9286
• DOI: 10.1109/TAC.2025.3611993
• 发表日期: 2026
• 关键词: K-STEP OPACITY; INFINITE-STEP; verification

摘要

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.