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
Source PublicationIEEE/CAA Journal of Automatica Sinica
ISSN2329-9266
2024
Volume11Issue:5Pages:1274-1291
AbstractThe 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.
KeywordLabeled Petri net multi-valued decision diagram networked discrete event system state-based opacity
DOI10.1109/JAS.2023.124128
Citation statistics
Document Type期刊论文
Identifierhttp://ir.ia.ac.cn/handle/173211/55715
Collection学术期刊_IEEE/CAA Journal of Automatica Sinica
Recommended Citation
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.
Files in This Item: Download All
File Name/Size DocType Version Access License
JAS-2023-1113.pdf(7338KB)期刊论文出版稿开放获取CC BY-NC-SAView Download
Related Services
Recommend this item
Bookmark
Usage statistics
Export to Endnote
Google Scholar
Similar articles in Google Scholar
[Yifan Dong]'s Articles
[Naiqi Wu]'s Articles
[Zhiwu Li]'s Articles
Baidu academic
Similar articles in Baidu academic
[Yifan Dong]'s Articles
[Naiqi Wu]'s Articles
[Zhiwu Li]'s Articles
Bing Scholar
Similar articles in Bing Scholar
[Yifan Dong]'s Articles
[Naiqi Wu]'s Articles
[Zhiwu Li]'s Articles
Terms of Use
No data!
Social Bookmark/Share
File name: JAS-2023-1113.pdf
Format: Adobe PDF
All comments (0)
No comment.
 

Items in the repository are protected by copyright, with all rights reserved, unless otherwise indicated.