IEEE/CAA Journal of Automatica Sinica
Citation:  Y. Dong, N. Wu, and Z. Li, “Statebased 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 
The opaque property plays an important role in the operation of a securitycritical system, implying that predefined secret information of the system is not able to be inferred through partially observing its behavior. This paper addresses the verification of currentstate, initialstate, infinitestep, and Kstep 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 currentstate and initialstate opacity, respectively. Then, we propose a structure called an Iobserver that is combined with secret states to verify whether a networked discrete event system is infinitestep opaque or Kstep opaque. Due to the utilization of symbolic approaches for the statebased 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.
[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/s102070080058x

[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 initialstate 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 Kstep 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 infinitestep 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/s106260120145z

[12] 
X. Yin and S. Lafortune, “A new approach for the verification of infinitestep and Kstep opacity using twoway 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/s1062601401964

[14] 
Z. Ma, X. Yin, and Z. Li, “Verification and enforcement of strong infinite and kstep 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 statebased 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, “Online verification of currentstate 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, “Online verification of initialstate 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 currentstate 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 infinitestep opacity using labeled Petri nets,” IFACPapersOnLine, 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 Kstep and infinitestep 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 Kstep 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, “Datadriven control of distributed eventtriggered 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 livenessenforcing supervisor tolerant to sensorreading 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 multiagent systems using faultestimationintheloop: Dynamic eventtriggered 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 statespace 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 statespace 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/OpacityinNDESs. Accessed: Oct. 7th, 2023.

[38] 
J. Babar and A. Miner, “Meddly: Multiterminal and edgevalued 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,” IFACPapersOnLine, vol. 51, no. 7, pp. 316–322, 2018. doi: 10.1016/j.ifacol.2018.06.319
