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

作　　者：Yifan Dong Naiqi Wu Zhiwu Li 

机构地区：[1]The authors are with the Institute of Systems Engineering,Macao University of Science and Technology,Taipa 999078,Macao,China

出　　处：《IEEE/CAA Journal of Automatica Sinica》2024年第5期1274-1291,共18页自动化学报（英文版）

基　　金：supported by the National R&D Program of China(2018YFB 1700104);the Science and Technology Development Fund;Macao Special Administrative Region(MSAR)(0029/2023/RIA1)。

摘　　要：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.

关 键 词：INFINITE SYSTEM SYMBOLIC 

分 类 号：TP301.1[自动化与计算机技术—计算机系统结构] TP13[自动化与计算机技术—计算机科学与技术]