Opacity Enforcement in Discrete Event Systems Using Extended Insertion Functions Under Inserted Language Constraints

• 成果类型: Article
• 署名作者: Li, Xiaoyan; Hadjicostis, Christoforos N.; Li, Zhiwu
• 署名单位: University of Cyprus; Xidian University; Macau University of Science & Technology
• 刊物名称: IEEE TRANSACTIONS ON AUTOMATIC CONTROL
• ISSN/ISSBN: 0018-9286
• DOI: 10.1109/TAC.2023.3239433
• 发表日期: 2023
• 页码: 6797-6803
• 关键词: Discrete event system; extended insertion function; finite state automaton; inserted language constraint; opacity.

摘要

Opacity is a confidentiality property capturing the fact that certain secret behavior of a system cannot be revealed under any system evolution. Current-state opacity can be enforced by using an extended insertion mechanism, which is capable of inserting fake symbols before and after an actual output, in real time as the system evolves. This article studies the enforcement of current-state opacity for systems modeled by finite state automata using an extended insertion strategy under constraints on the way symbols can be inserted before and after an actual symbol generated by the system (e.g., constraints on the type, order, and number of inserted symbols). More specifically, we consider inserted language constraints captured by the notion of (L-b, L-a)-enforceability, where L-b is the set of strings that can be inserted before, and L-a is the set of strings that can be inserted after an observed event. If L-b and L-a are regular languages, a verifier is constructed to derive a necessary and sufficient condition for opacity enforceability, and also to formulate an extended insertion strategy (if viable).