A journal of IEEE and CAA , publishes high-quality papers in English on original theoretical/experimental research and development in all areas of automation
Volume 11 Issue 5
May  2024

IEEE/CAA Journal of Automatica Sinica

  • JCR Impact Factor: 11.8, Top 4% (SCI Q1)
    CiteScore: 17.6, Top 3% (Q1)
    Google Scholar h5-index: 77, TOP 5
Turn off MathJax
Article Contents
Y. Dong, N. Wu, and  Z. Li,  “State-based opacity verification of networked discrete event systems using labeled Petri nets,” IEEE/CAA J. Autom. Sinica, vol. 11, no. 5, pp. 1274–1291, May 2024. doi: 10.1109/JAS.2023.124128
Citation: Y. Dong, N. Wu, and  Z. Li,  “State-based opacity verification of networked discrete event systems using labeled Petri nets,” IEEE/CAA J. Autom. Sinica, vol. 11, no. 5, pp. 1274–1291, May 2024. doi: 10.1109/JAS.2023.124128

State-Based Opacity Verification of Networked Discrete Event Systems Using Labeled Petri Nets

doi: 10.1109/JAS.2023.124128
Funds:  This work was supported by the National R&D Program of China (2018YFB1700104) and the Science and Technology Development Fund, Macao Special Administrative Region (MSAR) (0029/2023/RIA1)
More Information
  • The opaque property plays an important role in the operation of a security-critical system, implying that pre-defined secret information of the system is not able to be inferred through partially observing its behavior. This paper addresses the verification of current-state, initial-state, infinite-step, and K-step opacity of networked discrete event systems modeled by labeled Petri nets, where communication losses and delays are considered. Based on the symbolic technique for the representation of states in Petri nets, an observer and an estimator are designed for the verification of current-state and initial-state opacity, respectively. Then, we propose a structure called an I-observer that is combined with secret states to verify whether a networked discrete event system is infinite-step opaque or K-step opaque. Due to the utilization of symbolic approaches for the state-based opacity verification, the computation of the reachability graphs of labeled Petri nets is avoided, which dramatically reduces the computational overheads stemming from networked discrete event systems.

     

  • loading
  • 1 In this paper, we use $ \mathbb{N} $ to represent the set of non-negative integers.
    2 Unless otherwise stated, we refer the reader to the note entitled “Supplementary Contents for NDESs” on the web “https://github.com/dongyifan199/Opacity-in-NDESs”.
    3 The symbol “$ \check{\ } $” over a notation denoting an MDD is a set of markings represented by the MDD. Here, $ \check{q }_o $ is a set of markings represented by the MDD $ q_o $.
    4 With a slight abuse of notation, write $ |\cdot| $, where “$ \cdot $” denotes a sequence, to represent the length, i.e., the number of elements in a default sequence.
    5 The symbol “$ \hat{\ } $” over a notation denoting a set of markings implies that the set is represented by an MDD.
  • [1]
    L. Mazaré, “Using unification for opacity properties,” in Proc. Workshop Issues Theory Security, 2004, pp. 165–176.
    [2]
    J. W. Bryans, M. Koutny, L. Mazaré, and P. Y. Ryan, “Opacity generalised to transition systems,” Int. J. Information Security, vol. 7, no. 6, pp. 421–435, 2008. doi: 10.1007/s10207-008-0058-x
    [3]
    J. W. Bryans, M. Koutny, and P. Y. Ryan, “Modelling opacity using Petri nets,” Electronic Notes in Theoretical Computer Science, vol. 121, pp. 101–115, 2005. doi: 10.1016/j.entcs.2004.10.010
    [4]
    A. Saboori and C. N. Hadjicostis, “Notions of security and opacity in discrete event systems,” in Proc. 46th IEEE Conf. Decision and Control, 2007, pp. 5056–5061.
    [5]
    A. Saboori and C. N. Hadjicostis, “Verification of initial-state opacity in security applications of discrete event systems,” Information Sciences, vol. 246, pp. 115–132, 2013. doi: 10.1016/j.ins.2013.05.033
    [6]
    A. Saboori and C. N. Hadjicostis, “Verification of K-step opacity and analysis of its complexity,” IEEE Trans. Autom. Science and Engineering, vol. 8, no. 3, pp. 549–559, 2011. doi: 10.1109/TASE.2011.2106775
    [7]
    A. Saboori and C. N. Hadjicostis, “Verification of infinite-step opacity and complexity considerations,” IEEE Trans. Autom. Control, vol. 57, no. 5, pp. 1265–1269, 2011.
    [8]
    F. Lin, “Opacity of discrete event systems and its applications,” Automatica, vol. 47, no. 3, pp. 496–503, 2011. doi: 10.1016/j.automatica.2011.01.002
    [9]
    F. Cassez, J. Dubreil, and H. Marchand, “Dynamic observers for the synthesis of opaque systems,” in Int. Symposium on Automated Technology for Verification and Analysis. Berlin, Germany: Springer, 2009, pp. 352–367.
    [10]
    C. G. Cassandras and S. Lafortune, Introduction to Discrete Event Systems, 2nd ed. New York, USA: Springer, 2009.
    [11]
    Y.-C. Wu and S. Lafortune, “Comparative analysis of related notions of opacity in centralized and coordinated architectures,” Discrete Event Dynamic Systems, vol. 23, no. 3, pp. 307–339, 2013. doi: 10.1007/s10626-012-0145-z
    [12]
    X. Yin and S. Lafortune, “A new approach for the verification of infinite-step and K-step opacity using two-way observers,” Automatica, vol. 80, pp. 162–171, 2017. doi: 10.1016/j.automatica.2017.02.037
    [13]
    Y. Falcone and H. Marchand, “Enforcement and validation (at runtime) of various notions of opacity,” Discrete Event Dynamic Systems, vol. 25, no. 4, pp. 531–570, 2015. doi: 10.1007/s10626-014-0196-4
    [14]
    Z. Ma, X. Yin, and Z. Li, “Verification and enforcement of strong infinite- and k-step opacity using state recognizers,” Automatica, vol. 133, p. 109838, 2021. doi: 10.1016/j.automatica.2021.109838
    [15]
    Y. Tong, Z. Li, C. Seatzu, and A. Giua, “Verification of state-based opacity using Petri nets,” IEEE Trans. Autom. Control, vol. 62, no. 6, pp. 2823–2837, 2016.
    [16]
    X. Cong, M. P. Fanti, A. M. Mangini, and Z. Li, “On-line verification of current-state opacity by Petri nets and integer linear programming,” Automatica, vol. 94, pp. 205–213, 2018. doi: 10.1016/j.automatica.2018.04.021
    [17]
    X. Cong, M. P. Fanti, A. M. Mangini, and Z. Li, “On-line verification of initial-state opacity by Petri nets and integer linear programming,” ISA Trans., vol. 93, pp. 108–114, 2019. doi: 10.1016/j.isatra.2019.01.023
    [18]
    Y. Dong, Z. Li, and N. Wu, “Symbolic verification of current-state opacity of discrete event systems using Petri nets,” IEEE Trans. Systems,Man,and Cyber.: Systems, vol. 52, no. 12, pp. 7628–7641, 2022. doi: 10.1109/TSMC.2022.3151695
    [19]
    H. Lan, Y. Tong, and C. Seatzu, “Verification of infinite-step opacity using labeled Petri nets,” IFAC-PapersOnLine, vol. 53, no. 2, pp. 1729–1734, 2020. doi: 10.1016/j.ifacol.2020.12.2287
    [20]
    Y. Tong, H. Lan, and C. Seatzu, “Verification of K-step and infinite-step opacity of bounded labeled Petri nets,” Automatica, vol. 140, p. 110221, 2022. doi: 10.1016/j.automatica.2022.110221
    [21]
    G. Zhu, Z. Li, and N. Wu, “Online verification of K-step opacity by Petri nets in centralized and decentralized structures,” Automatica, vol. 145, p. 110528, 2022. doi: 10.1016/j.automatica.2022.110528
    [22]
    W. Duo, M. Zhou, and A. Abusorrah, “A survey of cyber attacks on cyber physical systems: Recent advances and challenges,” IEEE/CAA J. Autom. Sinica, vol. 9, no. 5, pp. 784–800, 2022. doi: 10.1109/JAS.2022.105548
    [23]
    X. Wang, J. Sun, G. Wang, F. Allgöwer, and J. Chen, “Data-driven control of distributed event-triggered network systems,” IEEE/CAA J. Autom. Sinica, vol. 10, no. 2, pp. 351–364, 2023. doi: 10.1109/JAS.2023.123225
    [24]
    D. You, S. Wang, M. Zhou, and C. Seatzu, “Supervisory control of Petri nets in the presence of replacement attacks,” IEEE Trans. Autom. Control, vol. 67, no. 3, pp. 1466–1473, 2022. doi: 10.1109/TAC.2021.3063699
    [25]
    D. You, S. Wang, and C. Seatzu, “A liveness-enforcing supervisor tolerant to sensor-reading modification attacks,” IEEE Trans. Systems,Man,and Cyber.: Systems, vol. 52, no. 4, pp. 2398–2411, 2022. doi: 10.1109/TSMC.2021.3051096
    [26]
    F. Lin, “Control of networked discrete event systems: Dealing with communication delays and losses,” SIAM J. Control and Optimization, vol. 52, no. 2, pp. 1276–1298, 2014. doi: 10.1137/130914942
    [27]
    S. Shu and F. Lin, “Supervisor synthesis for networked discrete event systems with communication delays,” IEEE Trans. Autom. Control, vol. 60, no. 8, pp. 2183–2188, 2014.
    [28]
    Y. Ju, D. Ding, X. He, Q.-L. Han, and G. Wei, “Consensus control of multi-agent systems using fault-estimation-in-the-loop: Dynamic event-triggered case,” IEEE/CAA J. Autom. Sinica, vol. 9, no. 8, pp. 1440–1451, 2021.
    [29]
    S. Shu and F. Lin, “Predictive networked control of discrete event systems,” IEEE Trans. Autom. Control, vol. 62, no. 9, pp. 4698–4705, 2016.
    [30]
    Z. Liu, X. Yin, S. Shu, F. Lin, and S. Li, “Online supervisory control of networked discrete event systems with control delays,” IEEE Trans. Autom. Control, vol. 67, no. 5, pp. 2314–2329, 2022. doi: 10.1109/TAC.2021.3080495
    [31]
    J. Yang, W. Deng, D. Qiu, and C. Jiang, “Opacity of networked discrete event systems,” Information Sciences, vol. 543, pp. 328–344, 2021. doi: 10.1016/j.ins.2020.07.017
    [32]
    T. Murata, “Petri nets: Properties, analysis and applications,” Proc. IEEE, vol. 77, pp. 541–580, 1989. doi: 10.1109/5.24143
    [33]
    A. S. Miner and G. Ciardo, “Efficient reachability set generation and storage using decision diagrams,” in Proc. Int. Conf. Application and Theory of Petri Nets, 1999, pp. 6–25.
    [34]
    A. S. Miner, “Implicit GSPN reachability set generation using decision diagrams,” Performance Evaluation, vol. 56, no. 1–4, pp. 145–165, 2004. doi: 10.1016/j.peva.2003.07.005
    [35]
    G. Ciardo, G. Lüttgen, and R. Siminiceanu, “Efficient symbolic state-space construction for asynchronous systems,” in Proc. Int. Conf. Application and Theory of Petri Nets, 2000, pp. 103–122.
    [36]
    M. Wan and G. Ciardo, “Symbolic state-space generation of asynchronous systems using extensible decision diagrams,” in Proc. Int. Conf. Current Trends in Theory and Practice of Computer Science, 2009, pp. 582–594.
    [37]
    Y. Dong, Z. Li, and N. Wu, “Supplementary contents for NDESs.” [Online]. Available: https://github.com/dongyifan199/Opacity-in-NDESs. Accessed: Oct. 7th, 2023.
    [38]
    J. Babar and A. Miner, “Meddly: Multi-terminal and edge-valued decision diagram library,” in Proc. 7th Int. Conf. Quantitative Evaluation of Systems, 2010, pp. 195–196.
    [39]
    S. Liu, Y. Tong, C. Seatzu, and A. Giua, “Petribar: A Matlab tool- box for Petri nets implementing basis reachability approaches,” IFAC-PapersOnLine, vol. 51, no. 7, pp. 316–322, 2018. doi: 10.1016/j.ifacol.2018.06.319

Catalog

    通讯作者: 陈斌, bchen63@163.com
    • 1. 

      沈阳化工大学材料科学与工程学院 沈阳 110142

    1. 本站搜索
    2. 百度学术搜索
    3. 万方数据库搜索
    4. CNKI搜索

    Figures(11)  / Tables(11)

    Article Metrics

    Article views (168) PDF downloads(32) Cited by()

    Highlights

    • We formulate the current-state, initial-state, infinite-step, and K-step opacity verification problems of networked discrete event systems under the framework of labeled Petri nets
    • Symbolic structures are presented to reduce the computational overheads stemming from networked discrete event systems. Particularly, in this paper, we design symbolic observers and estimators for the verification of current-state and initial-state opacity of networked discrete event systems, respectively
    • We explore the relation between the delayed state estimations of networked discrete event systems under communication delays and under both communication losses and delays
    • Besides, based on the proposed observers and estimators, we design a symbolic two-way observer to compute delayed state estimations with respect to all possible observations, where the communication losses are considered
    • By adding secret states to the proposed two-way observer, we construct a graph called an I-observer that can be used for the verification of infinite-step and K-step opacity of a networked discrete event system

    /

    DownLoad:  Full-Size Img  PowerPoint
    Return
    Return