Decidability of opacity verification problems in labeled Petri net systems

被引：48
|
作者：
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 current-state opacity and opaque time for labeled time Petri net systems
    Wang, Yuting
    Li, Liang
    Li, Zhiwu
    AUTOMATICA, 2025, 176
  • [2] Verification of Detectability for Time Labeled Petri Net Systems with Unobservable Transitions
    Qin, Tao
    Li, Zhiwu
    MATHEMATICS, 2025, 13 (04)
  • [3] Verification of Archive System Opacity With Bounded Labeled Petri Nets
    Liu, Zhenzhong
    IEEE ACCESS, 2024, 12 : 57185 - 57193
  • [4] Verification of Infinite-step Opacity Using Labeled Petri Nets
    Lan, Hao
    Tong, Yin
    Seatzu, Carla
    IFAC PAPERSONLINE, 2020, 53 (02): : 1729 - 1734
  • [5] State-Based Opacity Verification of Networked Discrete Event Systems Using Labeled Petri Nets
    Dong, Yifan
    Wu, Naiqi
    Li, Zhiwu
    IEEE-CAA JOURNAL OF AUTOMATICA SINICA, 2024, 11 (05) : 1274 - 1291
  • [6] State-Based Opacity Verification of Networked Discrete Event Systems Using Labeled Petri Nets
    Yifan Dong
    Naiqi Wu
    Zhiwu Li
    IEEE/CAA Journal of Automatica Sinica, 2024, 11 (05) : 1274 - 1291
  • [7] DECIDABILITY OF THE PETRI NET REACHABILITY PROBLEM
    BUDINAS, BL
    AUTOMATION AND REMOTE CONTROL, 1988, 49 (11) : 1393 - 1422
  • [8] Language-based Opacity Verification and Enforcement in the Framework of Labeled Petri Nets
    Habbachi, Salwa
    Li, Zhiwu
    Wu, Naiqi
    Khalgui, Mohamed
    SCIENCE PROGRESS, 2022, 105 (01)
  • [9] Assessment of initial-state-opacity in live and bounded labeled Petri net systems via optimization techniques
    Basile, Francesco
    De Tommasi, Gianmaria
    Motta, Carlo
    AUTOMATICA, 2023, 152
  • [10] On the Decidability and Complexity of Diagnosability for Labeled Petri Nets
    Yin, Xiang
    Lafortune, Stephane
    IEEE TRANSACTIONS ON AUTOMATIC CONTROL, 2017, 62 (11) : 5931 - 5938
12345