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 条
  • [31] Symbolic Verification of Current-State Opacity of Discrete Event Systems Using Petri Nets
    Dong, Yifan
    Li, Zhiwu
    Wu, Naiqi
    IEEE TRANSACTIONS ON SYSTEMS MAN CYBERNETICS-SYSTEMS, 2022, 52 (12): : 7628 - 7641
  • [32] Verification of Current-state Opacity for Discrete Event Systems Modeled With Unbounded Petri Nets*
    Zhu, Haoming
    Yin, Li
    Wu, Naiqi
    Li, Zhiwu
    2022 8TH INTERNATIONAL CONFERENCE ON CONTROL, DECISION AND INFORMATION TECHNOLOGIES (CODIT'22), 2022, : 1261 - 1266
  • [33] DECIDABILITY PROBLEMS FOR ACTOR SYSTEMS
    De Boer, Frank S.
    Jaghoori, Mohammad Mahdi
    Laneve, Cosimo
    Zavattaro, Gianluigi
    LOGICAL METHODS IN COMPUTER SCIENCE, 2014, 10 (04)
  • [34] Decidability Problems for Actor Systems
    de Boer, Frank S.
    Jaghoori, Mandi M.
    Laneve, Cosimo
    Zavattaro, Gianluigi
    CONCUR 2012 - CONCURRENCY THEORY, 2012, 7454 : 562 - 577
  • [35] Decidability problems in grammar systems
    Mihalache, V
    THEORETICAL COMPUTER SCIENCE, 1999, 215 (1-2) : 169 - 189
  • [36] Verification of State-Based Opacity Using Petri Nets
    Tong, Yin
    Li, Zhiwu
    Seatzu, Carla
    Giua, Alessandro
    IEEE TRANSACTIONS ON AUTOMATIC CONTROL, 2017, 62 (06) : 2823 - 2837
  • [37] Verification of Current-State Opacity Using Petri Nets
    Tong, Yin
    Li, Zhiwu
    Seatzu, Carla
    Giua, Alessandro
    2015 AMERICAN CONTROL CONFERENCE (ACC), 2015, : 1935 - 1940
  • [38] Marking diagnosability verification in labeled Petri nets
    Ma, Ziyue
    Yin, Xiang
    Li, Zhiwu
    AUTOMATICA, 2021, 131
  • [39] Current-state opacity verification in discrete event systems using an observer net
    Labed, Abdeldjalil
    Saadaoui, Ikram
    Wu, Naiqi
    Yu, Jiaxin
    Li, Zhiwu
    SCIENTIFIC REPORTS, 2022, 12 (01):
  • [40] Current-state opacity verification in discrete event systems using an observer net
    Abdeldjalil Labed
    Ikram Saadaoui
    Naiqi Wu
    Jiaxin Yu
    Zhiwu Li
    Scientific Reports, 12 (1)
12345