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 条
  • [31] COMPOSITIONAL DESIGN AND VERIFICATION OF COMMUNICATION PROTOCOLS, USING LABELED PETRI NETS
    LLORET, JC
    AZEMA, P
    VERNADAT, F
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1991, 531 : 96 - 105
  • [32] Fuzzy Infinite-Step Opacity Measure of Discrete Event Systems and Its Applications
    Deng, Weilin
    Qiu, Daowen
    Yang, Jingkai
    [J]. IEEE TRANSACTIONS ON FUZZY SYSTEMS, 2022, 30 (03) : 885 - 892
  • [33] Comments on "A new approach for the verification of infinite-step and K -step opacity using two-way observers"[Automatica 80 (2017) 162-171]
    Lan, Hao
    Tong, Yin
    Guo, Jin
    Giua, Alessandro
    [J]. AUTOMATICA, 2020, 122
  • [34] Verification of communication hexagonal grid with the infinite petri nets
    Shmeleva, T.R.
    [J]. Telecommunications and Radio Engineering (English translation of Elektrosvyaz and Radiotekhnika), 2019, 78 (02): : 125 - 135
  • [35] K-Codiagnosability Verification of Labeled Petri Nets
    Ran, Ning
    Hao, Jinyuan
    Dong, Zijian
    He, Zhou
    Liu, Zhiheng
    Ruan, Yuan
    Wang, Shouguang
    [J]. IEEE ACCESS, 2019, 7 : 185055 - 185062
  • [36] Decidability of opacity verification problems in labeled Petri net systems
    Tong, Yin
    Li, Zhiwu
    Seatzu, Carla
    Giua, Alessandro
    [J]. AUTOMATICA, 2017, 80 : 48 - 53
  • [37] An algebraic characterization of language-based opacity in labeled Petri nets
    Basile, F.
    De Tommasi, G.
    [J]. IFAC PAPERSONLINE, 2018, 51 (07): : 329 - 336
  • [38] Critical Observability Verification and Enforcement of Labeled Petri Nets by Using Basis Markings
    Cong, Xuya
    Fanti, Maria Pia
    Mangini, Agostino Marcello
    Li, Zhiwu
    [J]. IEEE TRANSACTIONS ON AUTOMATIC CONTROL, 2023, 68 (12) : 8158 - 8164
  • [39] Verification of Fault-predictability in Labeled Petri Nets Using Predictor Graphs
    You, Dan
    Wang, ShouGuang
    Seatzu, Carla
    [J]. IEEE TRANSACTIONS ON AUTOMATIC CONTROL, 2019, 64 (10) : 4353 - 4360
  • [40] A symbolic approach to the verification and enforcement of current-state opacity using labelled Petri nets
    Peng, Kun
    Chen, Yufeng
    Li, Zhiwu
    [J]. IET CONTROL THEORY AND APPLICATIONS, 2024, 18 (02): : 171 - 183
12345