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

Yifan Dong; Naiqi Wu; Zhiwu Li

doi:10.1109/JAS.2023.124128

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

Article Navigation > IEEE/CAA Journal of Automatica Sinica > 2024 > 11(5): 1274-1291

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

Citation:

PDF( 3004 KB)

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

Author Bio:
Yifan Dong received the B.S. degree in automated mechanical design and manufacturing from Southwest University of Science and Technology in 2017, and the M.S. degree in precision instrument and machinery from University of Electronic Science and Technology of China in 2020. He is currently a Ph.D. candidate in intelligent science and systems at the Institute of System Engineering, Macau University of Science and Technology, Macau, China. His current research interests include Petri nets, state estimation, and supervisory control in discrete event systems

Naiqi Wu (Fellow, IEEE) received the B.S. degree in electrical engineering from Anhui University of Technology in 1982, the M.S. and Ph.D. degrees in systems engineering both from Xi’an Jiaotong University in 1985 and 1988, respectively. From 1988 to 1995, he was with Shenyang Institute of Automation, Chinese Academy of Sciences, and from 1995 to 1998, with Shantou University. He moved to Guangdong University of Technology in 1998. He joined Macau University of Science and Technology, Macau, China in 2013. He is currently a Chair Professor at the Institute of Systems Engineering, Macau University of Science and Technology, Macau, China. His research interests include production planning and scheduling, manufacturing system modeling and control, discrete event systems, Petri net theory and applications, intelligent transportation systems, and energy systems. He is the author or coauthor of one book, five book chapters, and 200+ peer-reviewed journal papers. He served as an Associate Editor of the IEEE Transactions on Systems, Man, and Cybernetics, Part C, IEEE Transactions on Automation Science and Engineering, IEEE Transactions on Systems, Man, and Cybernetics: Systems, and Editor-in-Chief of Industrial Engineering Journal, and is an Associate Editor of Information Sciences and IEEE/CAA Journal of Automatica Sinica

Zhiwu Li (Fellow, IEEE) received the B.S., M.S. and Ph.D. degrees in mechanical engineering, automatic control, and manufacturing engineering, respectively, all from Xidian University in 1989, 1992 and 1995, respectively. He joined Xidian University in 1992. Over the past decade, he was a Visiting Professor at the University of Toronto, Technion (Israel Institute of Technology), Martin-Luther University, Conservatoire National des Arts et Métiers (Cnam), Meliksah Universitesi, King Saud University, and the University of Cagliari. He is now also with the Institute of Systems Engineering, Macau University of Science and Technology, Macau, China. His current research interests include Petri net theory and application, supervisory control of discrete event systems, workflow modeling and analysis, system reconfiguration, game theory, and data and process mining. He is a Member of Discrete Event Systems Technical Committee of the IEEE Systems, Man, and Cybernetics Society, and a Member of IFAC Technical Committee on Discrete Event and Hybrid Systems from 2011 to 2014. He serves as a frequent reviewer for 100+ international journals including Automatica and a number of the IEEE Transactions as well as many international conferences. He is listed in Marquis Who’s Who in the world, 27th Edition, 2010. He is a recipient of an Alexander von Humboldt Research Grant, Alexander von Humboldt Foundation, Germany, and Research in Paris, France. He is the founding chair of Xi’an Chapter of IEEE Systems, Man, and Cybernetics Society
Corresponding author: Zhiwu Li, e-mail: zwli@must.edu.mo
¹ In this paper, we use \begin{document}$ \mathbb{N} $\end{document} to represent the set of non-negative integers.
² 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”.
³ The symbol “\begin{document}$ \check{\ } $\end{document}” over a notation denoting an MDD is a set of markings represented by the MDD. Here, \begin{document}$ \check{q }_o $\end{document} is a set of markings represented by the MDD \begin{document}$ q_o $\end{document}.
⁴ With a slight abuse of notation, write \begin{document}$ |\cdot| $\end{document}, where “\begin{document}$ \cdot $\end{document}” denotes a sequence, to represent the length, i.e., the number of elements in a default sequence.
⁵ The symbol “\begin{document}$ \hat{\ } $\end{document}” over a notation denoting a set of markings implies that the set is represented by an MDD.
Received Date: 2023-10-23
Accepted Date: 2023-11-21

Available Online: 2024-03-04

Abstract

Abstract

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.
- Labeled Petri net,
- multi-valued decision diagram,
- networked discrete event system,
- state-based opacity

FullText(HTML)

¹ In this paper, we use $ \mathbb{N} $ to represent the set of non-negative integers.
² 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”.
³ 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 $.
⁴ 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.
⁵ The symbol “$ \hat{\ } $” over a notation denoting a set of markings implies that the set is represented by an MDD.

References(39)

References

[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

Supplements(0)

Cited By

Proportional views

Proportional views

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

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

Figures(11) / Tables(11)

Get Citation

PDF

XML

Article Metrics

Article views (125) PDF downloads(25)

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
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

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

doi: 10.1109/JAS.2023.124128

Abstract

References

Proportional views

Catalog

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

Article Metrics

Highlights

Export File

Citation

Format

Content