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 条
  • [21] Decidability analysis of some classes of extended function Petri net
    Ohta, Atsushi
    Tsuji, Kohkichi
    2012 THIRD INTERNATIONAL CONFERENCE ON NETWORKING AND COMPUTING (ICNC 2012), 2012, : 414 - 419
  • [22] Petri Net Reachability Graphs: Decidability Status of FO Properties
    Darondeau, Philippe
    Demri, Stephane
    Meyer, Roland
    Morvan, Christophe
    IARCS ANNUAL CONFERENCE ON FOUNDATIONS OF SOFTWARE TECHNOLOGY AND THEORETICAL COMPUTER SCIENCE (FSTTCS 2011), 2011, 13 : 140 - 151
  • [23] Weak (approximate) detectability of labeled Petri net systems with inhibitor arcs
    Zhang, Kuize
    Giva, Alessandro
    IFAC PAPERSONLINE, 2018, 51 (07): : 167 - 171
  • [24] Verification of Prognosability for Labeled Petri Nets
    Yin, Xiang
    IEEE TRANSACTIONS ON AUTOMATIC CONTROL, 2018, 63 (06) : 1828 - 1834
  • [25] Verification of Initial-State Opacity in Petri Nets
    Tong, Yin
    Li, Zhiwu
    Seatzu, Carla
    Giua, Alessandro
    2015 54TH IEEE CONFERENCE ON DECISION AND CONTROL (CDC), 2015, : 344 - 349
  • [26] Verification of Detectability in Labeled Petri Nets
    Tong, Yin
    Lan, Hao
    Guo, Jin
    2019 AMERICAN CONTROL CONFERENCE (ACC), 2019, : 5627 - 5632
  • [27] Assessment of initial-state-opacity in live and bounded labeled Petri net systems via optimization techniques (vol 152, 110911, 2023)
    Basile, Francesco
    De Tommasi, Gianmaria
    Motta, Carlo
    AUTOMATICA, 2025, 171
  • [28] Modeling and formal verification of embedded systems based on a Petri net representation
    Cortés, LA
    Eles, P
    Peng, Z
    JOURNAL OF SYSTEMS ARCHITECTURE, 2003, 49 (12-15) : 571 - 598
  • [29] Diagnosability verification with Petri net unfoldings
    Madalinski, Agnes
    Nouioua, Farid
    Dague, Philippe
    INTERNATIONAL JOURNAL OF KNOWLEDGE-BASED AND INTELLIGENT ENGINEERING SYSTEMS, 2010, 14 (02) : 49 - 55
  • [30] Open problems in Petri net modeling and simulation of biological systems
    Chen, Ming
    Hofestdt, Ralf
    IT-INFORMATION TECHNOLOGY, 2014, 56 (02): : 76 - 81
12345