State-Based Opacity Verification of Networked Discrete Event Systems Using Labeled Petri Nets

doi:10.1109/JAS.2023.124128

CASIA OpenIR > 学术期刊 > IEEE/CAA Journal of Automatica Sinica

	State-Based Opacity Verification of Networked Discrete Event Systems Using Labeled Petri Nets
	Yifan Dong; Naiqi Wu; Zhiwu Li
发表期刊	IEEE/CAA Journal of Automatica Sinica
ISSN	2329-9266
	2024
卷号	11 期号:5 页码:1274-1291
摘要	The opaque property plays an important role in the operation of a security-critical system, implying that pre-defined secret information of the system is not able to be inferred through partially observing its behavior. This paper addresses the verification of current-state, initial-state, infinite-step, and K-step opacity of networked discrete event systems modeled by labeled Petri nets, where communication losses and delays are considered. Based on the symbolic technique for the representation of states in Petri nets, an observer and an estimator are designed for the verification of current-state and initial-state opacity, respectively. Then, we propose a structure called an I-observer that is combined with secret states to verify whether a networked discrete event system is infinite-step opaque or K-step opaque. Due to the utilization of symbolic approaches for the state-based opacity verification, the computation of the reachability graphs of labeled Petri nets is avoided, which dramatically reduces the computational overheads stemming from networked discrete event systems.
关键词	Labeled Petri net multi-valued decision diagram networked discrete event system state-based opacity
DOI	10.1109/JAS.2023.124128
引用统计
文献类型	期刊论文
条目标识符	http://ir.ia.ac.cn/handle/173211/55715
专题	学术期刊_IEEE/CAA Journal of Automatica Sinica
推荐引用方式 GB/T 7714	Yifan Dong,Naiqi Wu,Zhiwu Li. State-Based Opacity Verification of Networked Discrete Event Systems Using Labeled Petri Nets[J]. IEEE/CAA Journal of Automatica Sinica,2024,11(5):1274-1291.
APA	Yifan Dong,Naiqi Wu,&Zhiwu Li.(2024).State-Based Opacity Verification of Networked Discrete Event Systems Using Labeled Petri Nets.IEEE/CAA Journal of Automatica Sinica,11(5),1274-1291.
MLA	Yifan Dong,et al."State-Based Opacity Verification of Networked Discrete Event Systems Using Labeled Petri Nets".IEEE/CAA Journal of Automatica Sinica 11.5(2024):1274-1291.

条目包含的文件		下载所有文件
文件名称/大小	文献类型	版本类型	开放类型	使用许可
JAS-2023-1113.pdf（7338KB）	期刊论文	出版稿	开放获取	CC BY-NC-SA	浏览下载