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 条
  • [31] Decidability problems in grammar systems
    Mihalache, V
    [J]. THEORETICAL COMPUTER SCIENCE, 1999, 215 (1-2) : 169 - 189
  • [32] Verification of State-Based Opacity Using Petri Nets
    Tong, Yin
    Li, Zhiwu
    Seatzu, Carla
    Giua, Alessandro
    [J]. IEEE TRANSACTIONS ON AUTOMATIC CONTROL, 2017, 62 (06) : 2823 - 2837
  • [33] Verification of Current-State Opacity Using Petri Nets
    Tong, Yin
    Li, Zhiwu
    Seatzu, Carla
    Giua, Alessandro
    [J]. 2015 AMERICAN CONTROL CONFERENCE (ACC), 2015, : 1935 - 1940
  • [34] Marking diagnosability verification in labeled Petri nets
    Ma, Ziyue
    Yin, Xiang
    Li, Zhiwu
    [J]. AUTOMATICA, 2021, 131
  • [35] Current-state opacity verification in discrete event systems using an observer net
    Labed, Abdeldjalil
    Saadaoui, Ikram
    Wu, Naiqi
    Yu, Jiaxin
    Li, Zhiwu
    [J]. SCIENTIFIC REPORTS, 2022, 12 (01):
  • [36] Current-state opacity verification in discrete event systems using an observer net
    Abdeldjalil Labed
    Ikram Saadaoui
    Naiqi Wu
    Jiaxin Yu
    Zhiwu Li
    [J]. Scientific Reports, 12 (1)
  • [37] A Petri Net-Based Model for Verification of Obligations and Accountability in Cooperative Systems
    Du, YuYue
    Jiang, ChangJun
    Zhou, MengChu
    [J]. IEEE TRANSACTIONS ON SYSTEMS MAN AND CYBERNETICS PART A-SYSTEMS AND HUMANS, 2009, 39 (02): : 299 - 308
  • [38] Fuzzy Petri net tool for modeling and verification of knowledge-based systems
    [J]. Koriem, Samir M., 1600, Oxford Univ Press, Oxford, United Kingdom (43):
  • [39] A fuzzy Petri net tool for modeling and verification of knowledge-based systems
    Koriem, SM
    [J]. COMPUTER JOURNAL, 2000, 43 (03): : 206 - 223
  • [40] THE RESIDUE OF VECTOR SETS WITH APPLICATIONS TO DECIDABILITY PROBLEMS IN PETRI NETS
    VALK, R
    JANTZEN, M
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1985, 188 : 234 - 258
12345