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 条
  • [41] A Petri Net-Based Model for Verification of Obligations and Accountability in Cooperative Systems
    Du, YuYue
    Jiang, ChangJun
    Zhou, MengChu
    IEEE TRANSACTIONS ON SYSTEMS MAN AND CYBERNETICS PART A-SYSTEMS AND HUMANS, 2009, 39 (02): : 299 - 308
  • [42] THE RESIDUE OF VECTOR SETS WITH APPLICATIONS TO DECIDABILITY PROBLEMS IN PETRI NETS
    VALK, R
    JANTZEN, M
    LECTURE NOTES IN COMPUTER SCIENCE, 1985, 188 : 234 - 258
  • [43] A fuzzy Petri net tool for modeling and verification of knowledge-based systems
    Koriem, SM
    COMPUTER JOURNAL, 2000, 43 (03): : 206 - 223
  • [44] THE RESIDUE OF VECTOR SETS WITH APPLICATIONS TO DECIDABILITY PROBLEMS IN PETRI NETS
    VALK, R
    JANTZEN, M
    ACTA INFORMATICA, 1985, 21 (06) : 643 - 674
  • [45] A coloured Petri net approach to protocol verification
    Billington, J
    Gallasch, GE
    Han, B
    LECTURES ON CONCURRENCY AND PETRI NETS: ADVANCES IN PETRI NETS, 2004, 3098 : 210 - 290
  • [46] Verification of Service Replaceability with Colored Petri Net
    Liu, Ying
    Zhang, Bin
    Wang, De-shuai
    Zhang, Ming-wei
    Zhu, Zhi-liang
    2009 INTERNATIONAL SYMPOSIUM ON INTELLIGENT UBIQUITOUS COMPUTING AND EDUCATION, 2009, : 400 - +
  • [47] Petri net modeling and verification of transactional workflows
    Klai, Kais
    Gaaloul, Walid
    2011 20TH IEEE INTERNATIONAL WORKSHOPS ON ENABLING TECHNOLOGIES: INFRASTRUCTURE FOR COLLABORATIVE ENTERPRISES (WETICE), 2011, : 176 - 184
  • [48] On the Verification of Non-autonomous Petri Net Models Using Autonomous Petri Net Tools
    Barros, Joao Paulo
    Gomes, Luis
    Costa, Aniko
    38TH ANNUAL CONFERENCE ON IEEE INDUSTRIAL ELECTRONICS SOCIETY (IECON 2012), 2012, : 6138 - 6143
  • [49] An algebraic characterization of language-based opacity in labeled Petri nets
    Basile, F.
    De Tommasi, G.
    IFAC PAPERSONLINE, 2018, 51 (07): : 329 - 336
  • [50] Transforming Opacity Verification to Nonblocking Verification in Modular Systems
    Mohajerani, Sahar
    Lafortune, Stephane
    IEEE TRANSACTIONS ON AUTOMATIC CONTROL, 2020, 65 (04) : 1739 - 1746
12345