Verification of Infinite-step Opacity Using Labeled Petri Nets

被引：9
|
作者：
Lan, Hao [1 ,2 ]
Tong, Yin [1 ]
Seatzu, Carla [2 ]
机构：
[1] Southwest Jiaotong Univ, Sch Informat Sci & Technol, Chengdu 611756, Peoples R China
[2] Univ Cagliari, Dept Elect & Elect Engn, I-09123 Cagliari, Italy
来源：
IFAC PAPERSONLINE | 2020年 / 53卷 / 02期
基金：
中国国家自然科学基金;
关键词：
Discrete event systems; Petri nets; Infinite-step opacity; NOTIONS;
D O I：
10.1016/j.ifacol.2020.12.2287
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
Opacity is an important information secure property. A system is said to be infinite-step opaque if the intruder is never able to ascertain that the system is or has been in a secret state at some time, based on its observation of the system evolution. This work aims to verify infinite-step opacity of discrete event systems modeled with labeled Petri nets. Based on the notion of basis reachability graph, a new structure called basis two-way observer is proposed to check infinite-step opacity of a bounded system, which is shown to be more efficient than the standard method based on the reachability graph. Copyright (C) 2020 The Authors.
引用
收藏
页码：1729 / 1734
页数：6
相关论文
共 50 条
  • [1] Verification of K-step and infinite-step opacity of bounded labeled Petri nets
    Tong, Yin
    Lan, Hao
    Seatzu, Carla
    [J]. AUTOMATICA, 2022, 140
  • [2] Verification of Infinite-Step Opacity and Complexity Considerations
    Saboori, Anooshiravan
    Hadjicostis, Christoforos N.
    [J]. IEEE TRANSACTIONS ON AUTOMATIC CONTROL, 2012, 57 (05) : 1265 - 1269
  • [3] Verification of approximate infinite-step opacity using barrier certificates
    Kalat, Shadi Tasdighi
    Liu, Siyuan
    Zamani, Majid
    [J]. 2022 EUROPEAN CONTROL CONFERENCE (ECC), 2022, : 175 - 180
  • [4] Verification of Archive System Opacity With Bounded Labeled Petri Nets
    Liu, Zhenzhong
    [J]. IEEE ACCESS, 2024, 12 : 57185 - 57193
  • [5] Synthesis of Dynamic Masks for Infinite-Step Opacity
    Yin, Xiang
    Li, Shaoyuan
    [J]. IFAC PAPERSONLINE, 2018, 51 (07): : 343 - 348
  • [6] A new approach for the verification of infinite-step and K-step opacity using two-way observers
    Yin, Xiang
    Lafortune, Stephane
    [J]. AUTOMATICA, 2017, 80 : 162 - 171
  • [7] Synthesis of Dynamic Masks for Infinite-Step Opacity
    Yin, Xiang
    Li, Shaoyuan
    [J]. IEEE TRANSACTIONS ON AUTOMATIC CONTROL, 2020, 65 (04) : 1429 - 1441
  • [8] On Two-Way Observer and Its Application to the Verification of Infinite-Step and K-Step Opacity
    Yin, Xiang
    Lafortune, Stephane
    [J]. 2016 13TH INTERNATIONAL WORKSHOP ON DISCRETE EVENT SYSTEMS (WODES), 2016, : 361 - 366
  • [9] 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)
  • [10] Enforcement for infinite-step opacity and K-step opacity via insertion mechanism
    Liu, Rongjian
    Lu, Jianquan
    [J]. AUTOMATICA, 2022, 140
12345