Noninterference Analysis of Bounded Labeled Petri Nets

• 成果类型: Article
• 署名作者: Ran, Ning; Wu, Zhengguang; Zhang, Shaokang; He, Zhou; Seatzu, Carla
• 署名单位: Hebei University; Zhejiang University; Hebei University; Shaanxi University of Science & Technology; University of Cagliari
• 刊物名称: IEEE TRANSACTIONS ON AUTOMATIC CONTROL
• ISSN/ISSBN: 0018-9286
• DOI: 10.1109/TAC.2026.3661908
• 发表日期: 2026
• 关键词: K-STEP OPACITY; INFINITE-STEP; ENFORCEMENT

摘要

This article focuses on a fundamental problem on information security of bounded labeled Petri nets: noninterference analysis. As in hierarchical control, we assume that a system is observed by users at different levels, namely, high-level users and low-level users. The output events produced by the firing of transitions are also partitioned into high-level output events and low-level output events. In general, high-level users can observe the occurrence of all the output events, while low-level users can only observe the occurrence of low-level output events. A system is said to be noninterferent if low-level users cannot infer the firing of transitions labeled with high-level output events by looking at low-level outputs. In this article, we study a particular noninterference property, namely strong nondeterministic noninterference (SNNI), using a special automation called SNNI Verifier, and propose a necessary and sufficient condition for SNNI.