Decidability of opacity verification problems in labeled Petri net systems

被引：47
|
作者：
Tong, Yin [1 ,3 ]
Li, Zhiwu [1 ,2 ]
Seatzu, Carla [3 ]
Giua, Alessandro [3 ,4 ]
机构：
[1] Xidian Univ, Sch Electromech Engn, Xian 710071, Peoples R China
[2] Macau Univ Sci & Technol, Inst Syst Engn, Taipa, Macau, Peoples R China
[3] Univ Cagliari, Dept Elect & Elect Engn, I-09123 Cagliari, Italy
[4] Univ Toulon & Var, Aix Marseille Univ, CNRS, ENSAM,LSIS, Marseille, France
来源：
AUTOMATICA | 2017年 / 80卷
基金：
中国国家自然科学基金;
关键词：
Discrete event systems; Petri nets; Opacity; Decidability problems; DISCRETE-EVENT SYSTEMS; ENFORCEMENT; VALIDATION; NOTIONS;
D O I：
10.1016/j.automatica.2017.01.013
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
A system is said to be opaque if an intruder that observes its evolution through a mask cannot infer that the system's evolution belongs to a given secret behavior. Opacity verification is the problem of determining whether the system is opaque with respect to a given secret or not. In this paper we address the decidability of the opacity verification problem. Using reduction approaches, we show that verification of initial-state, current-state, and language opacity is undecidable in labeled Petri nets. (C) 2017 Elsevier Ltd. All rights reserved.
引用
收藏
页码：48 / 53
页数：6
相关论文
共 50 条
  • [1] Verification of Archive System Opacity With Bounded Labeled Petri Nets
    Liu, Zhenzhong
    [J]. IEEE ACCESS, 2024, 12 : 57185 - 57193
  • [2] Verification of Infinite-step Opacity Using Labeled Petri Nets
    Lan, Hao
    Tong, Yin
    Seatzu, Carla
    [J]. IFAC PAPERSONLINE, 2020, 53 (02): : 1729 - 1734
  • [3] 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
  • [4] 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
  • [5] DECIDABILITY OF THE PETRI NET REACHABILITY PROBLEM
    BUDINAS, BL
    [J]. AUTOMATION AND REMOTE CONTROL, 1988, 49 (11) : 1393 - 1422
  • [6] Language-based Opacity Verification and Enforcement in the Framework of Labeled Petri Nets
    Habbachi, Salwa
    Li, Zhiwu
    Wu, Naiqi
    Khalgui, Mohamed
    [J]. SCIENCE PROGRESS, 2022, 105 (01)
  • [7] Assessment of initial-state-opacity in live and bounded labeled Petri net systems via optimization techniques
    Basile, Francesco
    De Tommasi, Gianmaria
    Motta, Carlo
    [J]. AUTOMATICA, 2023, 152
  • [8] On the Decidability and Complexity of Diagnosability for Labeled Petri Nets
    Yin, Xiang
    Lafortune, Stephane
    [J]. IEEE TRANSACTIONS ON AUTOMATIC CONTROL, 2017, 62 (11) : 5931 - 5938
  • [9] Diagnosability Analysis of Labeled Time Petri Net Systems
    Basile, Francesco
    Cabasino, Maria Paola
    Seatzu, Carla
    [J]. IEEE TRANSACTIONS ON AUTOMATIC CONTROL, 2017, 62 (03) : 1384 - 1396
  • [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
12345