首页|State-Based Opacity Verification of Networked Dis-crete Event Systems Using Labeled Petri Nets

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

扫码查看
原文链接
  • 国家科技期刊平台
  • NETL
  • NSTL
  • 万方数据
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 verifi-cation of current-state,initial-state,infinite-step,and K-step opac-ity 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 com-bined 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 ver-ification,the computation of the reachability graphs of labeled Petri nets is avoided,which dramatically reduces the computa-tional overheads stemming from networked discrete event sys-tems.

Labeled Petri netmulti-valued decision diagramnetworked discrete event systemstate-based opacity

Yifan Dong、Naiqi Wu、Zhiwu Li

展开 >

Institute of Systems Engineering,Macau University of Science and Technology,Taipa 999078,Macau,China

National Research and Development Program of ChinaScience and Technology Development Fund,Macao Special Administrative Region(MSAR)

2018YFB 17001040029/2023/RIA1

2024

10.1109/JAS.2023.124128

自动化学报(英文版)
中国自动化学会,中国科学院自动化研究所,中国科技出版传媒股份有限公司

自动化学报(英文版)

CSTPCDEI
ISSN：2329-9266
年,卷(期)：2024.11(5)
  • 39