Assessment of initial-state-opacity in live and bounded labeled Petri net systems via optimization techniques

被引：7
|
作者：
Basile, Francesco [1 ]
De Tommasi, Gianmaria [2 ]
Motta, Carlo [2 ]
机构：
[1] Univ Salerno, DIEM, I-84084 Fisciano, Italy
[2] Univ Napoli Federico II, DIETI, I-80125 Naples, Italy
来源：
AUTOMATICA | 2023年 / 152卷
关键词：
Opacity; Labeled Petri nets; DES; Integer linear programming; NONINTERFERENCE; DIAGNOSABILITY; VERIFICATION;
D O I：
10.1016/j.automatica.2023.110911
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
Opacity is a property of discrete event systems (DES) that is related to the possibility of hiding a secret to external observers, the so called intruders. If the secret is the system initial state, then the related opacity problem is referred to as Initial State Opacity (ISO). This paper gives a necessary and sufficient condition to check ISO in DES modeled as bounded and live labeled Petri nets (PNs). The proposed approach relies on both the algebraic representation of labeled PNs dynamic, and on their structural representation in terms of minimal support T-invariants. The proposed necessary and sufficient condition enables ISO assessment by means of the solution of Integer Linear Programming problems, which can be efficiently solved nowadays by means of off-the-shelf optimization tools.(c) 2023 Elsevier Ltd. All rights reserved.
引用
收藏
页数：9
相关论文
共 14 条
  • [1] Assessment of Initial-State-Opacity in Live Bounded and Reversible Discrete Event Systems via Integer Linear Programming
    Basile, Francesco
    De Tommasi, Gianmaria
    Motta, Carlo
    Petrillo, Alberto
    Santini, Stefania
    [J]. 2022 30TH MEDITERRANEAN CONFERENCE ON CONTROL AND AUTOMATION (MED), 2022, : 994 - 999
  • [2] Necessary and Sufficient Condition to Assess Initial-State-Opacity in Live Bounded and Reversible Discrete Event Systems
    Basile, Francesco
    De Tommasi, Gianmaria
    Motta, Carlo
    Sterle, Claudio
    [J]. IEEE CONTROL SYSTEMS LETTERS, 2022, 6 : 2683 - 2688
  • [3] Decidability of opacity verification problems in labeled Petri net systems
    Tong, Yin
    Li, Zhiwu
    Seatzu, Carla
    Giua, Alessandro
    [J]. AUTOMATICA, 2017, 80 : 48 - 53
  • [4] An optimization-based approach to assess non-interference in labeled and bounded Petri net systems
    Basile, Francesco
    Boccia, Maurizio
    De Tommasi, Gianmaria
    Motta, Carlo
    Sterle, Claudio
    [J]. NONLINEAR ANALYSIS-HYBRID SYSTEMS, 2022, 44
  • [5] Observability analysis of bounded petri net systems via a matrix approach
    [J]. Chen, Zeng-Qiang (chenzq@nankai.edu.cn), 2018, South China University of Technology (35):
  • [6] State-Based Opacity Verification of Networked Discrete Event Systems Using Labeled Petri Nets
    Yifan Dong
    Naiqi Wu
    Zhiwu Li
    [J]. IEEE/CAA Journal of Automatica Sinica, 2024, 11 (05) : 1274 - 1291
  • [7] State-Based Opacity Verification of Networked Discrete Event Systems Using Labeled Petri Nets
    Dong, Yifan
    Wu, Naiqi
    Li, Zhiwu
    [J]. IEEE-CAA JOURNAL OF AUTOMATICA SINICA, 2024, 11 (05) : 1274 - 1291
  • [8] State Estimation and Fault Diagnosis of Labeled Time Petri Net Systems With Unobservable Transitions
    Basile, Francesco
    Cabasino, Maria Paola
    Seatzu, Carla
    [J]. IEEE TRANSACTIONS ON AUTOMATIC CONTROL, 2015, 60 (04) : 997 - 1009
  • [9] State estimation in labeled time Petri net systems using observed modified state class graph
    Li, Liang
    Deng, Mingxi
    Liu, Bin
    Lib, Zhiwu
    [J]. INFORMATION SCIENCES, 2024, 656
  • [10] Strong Current-State Opacity Verification of Discrete-Event Systems Modeled With Time Labeled Petri Nets
    Tao Qin
    Li Yin
    Gaiyun Liu
    Naiqi Wu
    Zhiwu Li
    [J]. IEEE/CAA Journal of Automatica Sinica., 2025, 12 (01) - 68
12