Strong Current-State Opacity Verification of Discrete-Event Systems Modeled With Time Labeled Petri Nets

Tao Qin; Li Yin; Gaiyun Liu; Naiqi Wu; Zhiwu Li

doi:10.1109/JAS.2024.124560

IEEE/CAA Journal of Automatica Sinica

JCR Impact Factor: 15.3, Top 1 (SCI Q1)

CiteScore: 23.5, Top 2% (Q1)
Google Scholar h5-index: 77， TOP 5

Turn off MathJax

Article Contents

Article Navigation > IEEE/CAA Journal of Automatica Sinica > 2025 > In Press, Accepted Manuscript

T. Qin, L. Yin, G. Liu, N. Wu, and Z. Li, “Strong current-state opacity verification of discrete-event systems modeled with time labeled Petri nets,” IEEE/CAA J. Autom. Sinica, vol. 12, no. 1, pp. 1–15, Jan. 2025. doi: 10.1109/JAS.2024.124560

Citation:

T. Qin, L. Yin, G. Liu, N. Wu, and Z. Li, “Strong current-state opacity verification of discrete-event systems modeled with time labeled Petri nets,” IEEE/CAA J. Autom. Sinica, vol. 12, no. 1, pp. 1–15, Jan. 2025. doi: 10.1109/JAS.2024.124560

Citation:

PDF( 1575 KB)

Strong Current-State Opacity Verification of Discrete-Event Systems Modeled With Time Labeled Petri Nets

doi: 10.1109/JAS.2024.124560

Tao Qin^,,
Li Yin^,,
Gaiyun Liu^{,
,},
Naiqi Wu^,,
Zhiwu Li^,

Funds: This work was supported by the Special Fund for Scientific and Technological Innovation Strategy of Guangdong Province (2022A0505030025) and the Science and Technology Fund, FDCT, Macau SAR (0064/2021/A2)

More Information

Author Bio:
Tao Qin received the M.S. degree in intelligent technology from the Macau University of Science and Technology, Macau, China, in 2022. He is currently pursuing the Ph.D. degree with the Institute of System Engineering, Macau University of Science and Technology, Macau, China. His current research interests include Petri nets, opacity, state estimation, verification, and supervisory control of discrete-event systems

Li Yin received the B.E. degree in remote sensing from Wuhan University, Wuhan, China, in 2007, the M.S. degree in GIS from the CNNC Beijing Research Institute of Uranium Geology, Beijing, in 2014, and the Ph.D. degree from the Macau University of Science and Technology, Macau, China. He is currently an Assistant Professor with the Institute of Systems Engineering, Macau University of Science and Technology. His research interests include discrete-event systems and fault-tolerant dynamic systems with applications to manufacturing

Gaiyun Liu (Senior Member, IEEE) received the B.S. degree in measurement and control technology and instrumentation and the Ph.D. degree in mechanical engineering from Xidian University, Xi’an, China, in 2006 and 2011, respectively. In 2011, she joined Xidian University, where she is currently an Associate Professor with the School of Electro-Mechanical Engineering. She has authored or coauthored more than 30 publications. Her current research interests include formal methods, robust supervisory control of manufacturing systems, and security analysis and supervisory control of discrete event systems

Naiqi Wu (Fellow, IEEE) received his B.S. Degree in electrical engineering from Anhui University of Technology, Huainan, China, in 1982, the M.S. and Ph.D. Degrees in systems engineering both from Xi’an Jiaotong University, Xi’an, China in 1985 and 1988, respectively. From 1988 to 1995, he was with Shenyang Institute of Automation, Chinese Academy of Sciences, Shenyang, China, and from 1995 to 1998, with Shantou University, Shantou, China. He moved to Guangdong University of Technology, Guangzhou, China in 1998. He joined Macau University of Science and Technology, Taipa, Macau in 2013. He is currently a Professor at the Institute of Systems Engineering, Macau University of Science and Technology, Taipa, Macau. 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 130+ peer-reviewed journal papers

Zhiwu Li (Fellow, IEEE) received the B.S., M.S., and Ph.D. degrees all from Xidian University, Xi’an, China, in 1989, 1992, and 1995, respectively. Dr. Li held visiting professor positions at the University of Toronto, Technion (Israel Institute of Technology), Martin-Luther University at Halle (supported by Alexander von Humboldt Foundation), University of Cagliari, Politecnico di Bari, Conservatoire National des Arts et Métiers (Cnam, supported by the program of Research in Paris), King Saud University, and Meliksah University. He has published three monographs in Springer (2009; 2023) and CRC Press (2013). His research was cited by leading business giants including IBM, HP, ABB, Volvo, GE, GM, Mitsubishi, Ford Car, and Huawei. His current research interests include Petri net theory & applications, supervisory control of discrete-event systems, data modeling, and production automation. He is a Fellow of IEEE (2016) and was selected as Thomson Reuters Highly Cited Researchers in the category of Engineering from 2014–2018
Corresponding author: Gaiyun Liu, e-mail: gyliu@xidian.edu.cn
Received Date: 2024-02-15
Revised Date: 2024-04-11
Accepted Date: 2024-05-19

Available Online: 2024-09-12

Abstract

Abstract

This paper addresses the verification of strong current-state opacity with respect to real-time observations generated from a discrete-event system that is modeled with time labeled Petri nets. The standard current-state opacity cannot completely characterize higher-level security. To ensure the higher-level security requirements of a time-dependent system, we propose a strong version of opacity known as strong current-state opacity. For any path (state-event sequence with time information) π derived from a real-time observation that ends at a secret state, the strong current-state opacity of the real-time observation signifies that there is a non-secret path with the same real-time observation as π. We propose general and non-secret state class graphs, which characterize the general and non-secret states of time-dependent systems, respectively. To capture the observable behavior of non-secret states, a non-secret observer is proposed. Finally, we develop a structure called a real-time concurrent verifier to verify the strong current-state opacity of time labeled Petri nets. This approach is efficient since the real-time concurrent verifier can be constructed by solving a certain number of linear programming problems.
- Discrete-event system,
- real-time observation,
- strong current-state opacity,
- time labeled Petri net

FullText(HTML)

References(42)

References

[1]	L. Mazaré, “Using unification for opacity properties,” in Proc. Workshop Issues in the Theory of Security, Barcelona, Spain, 2004, pp. 165–176.
[2]	S. Yang, J. Hou, X. Yin, and S. Li, “Opacity of networked supervisory control systems over insecure communication channels,” IEEE Trans. Control Netw. Syst., vol. 8, no. 2, pp. 884–896, Jun. 2021. doi: 10.1109/TCNS.2021.3050131
[3]	W. Duo, M. C. 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, May 2022. doi: 10.1109/JAS.2022.105548
[4]	C. Gu, X. Wang, and Z. Li, “Synthesis of supervisory control with partial observation on normal state-tree structures,” IEEE Trans. Autom. Sci. Eng., vol. 16, no. 2, pp. 984–997, Apr. 2019. doi: 10.1109/TASE.2018.2880178
[5]	Y. Tong, Z. Li, and A. Giua, “On the equivalence of observation structures for Petri net generators,” IEEE Trans. Automat. Contr., vol. 61, no. 9, pp. 2448–2462, Sep. 2016. doi: 10.1109/TAC.2015.2496500
[6]	L. Shen, S. Miao, A. Lai, and J. Komenda, “Verification of initial-and-final-state opacity for unambiguous weighted automata,” ISA Trans., vol. 148, pp. 237–246, May 2024. doi: 10.1016/j.isatra.2024.03.019
[7]	N. Ran, A. Giua, and C. Seatzu, “Enforcement of diagnosability in labeled Petri nets via optimal sensor selection,” IEEE Trans. Automat. Contr., vol. 64, no. 7, pp. 2997–3004, Jul. 2019. doi: 10.1109/TAC.2018.2874020
[8]	C. Liu, “Formal modeling and discovery of multi-instance business processes: A cloud resource management case study,” IEEE/CAA J. Autom. Sinica, vol. 9, no. 12, pp. 2151–2160, Dec. 2022. doi: 10.1109/JAS.2022.106109
[9]	F. Basile, G. De Tommasi, and C. Motta, “Assessment of initial-state-opacity in live and bounded labeled Petri net systems via optimization techniques,” Automatica, vol. 152, p. 110911, Jun. 2023. doi: 10.1016/j.automatica.2023.110911
[10]	Y. Tong, Z. Li, C. Seatzu, and A. Giua, “Verification of state-based opacity using Petri nets,” IEEE Trans. Automat. Contr., vol. 62, no. 6, pp. 2823–2837, Jun. 2017. doi: 10.1109/TAC.2016.2620429
[11]	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, Oct. 2019. doi: 10.1016/j.isatra.2019.01.023
[12]	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, Jun. 2022. doi: 10.1016/j.automatica.2022.110221
[13]	J. Balun and T. Masopust, “Verifying weak and strong k-step opacity in discrete-event systems,” Automatica, vol. 155, p. 111153, Sep. 2023. doi: 10.1016/j.automatica.2023.111153
[14]	Y. Tong, Z. Ma, Z. Li, C. Seactzu, and A. Giua, “Verification of language-based opacity in Petri nets using verifier,” in Proc. American Control Conf., Boston, USA, 2016, pp. 757–763.
[15]	Y. Falcone and H. Marchand, “Enforcement and validation (at runtime) of various notions of opacity,” Discrete Event Dyn. Syst., vol. 25, no. 4, pp. 531–570, Dec. 2015. doi: 10.1007/s10626-014-0196-4
[16]	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, Nov. 2021. doi: 10.1016/j.automatica.2021.109838
[17]	X. Han, K. Zhang, J. Zhang, Z. Li, and Z. Chen, “Strong current-state and initial-state opacity of discrete-event systems,” Automatica, vol. 148, p. 110756, Feb. 2023. doi: 10.1016/j.automatica.2022.110756
[18]	J. Zhou, J. Wang, and J. Wang, “A simulation engine for stochastic timed Petri nets and application to emergency healthcare systems,” IEEE/CAA J. Autom. Sinica, vol. 6, no. 4, pp. 969–980, Jul. 2019. doi: 10.1109/JAS.2019.1911576
[19]	X. Chen, H. Peng, J. Wang, and F. Hao, “Supervisory control of discrete event systems under asynchronous spiking neuron P systems,” Inf. Sci., vol. 597, pp. 253–273, Jun. 2022. doi: 10.1016/j.ins.2022.03.003
[20]	E. André, S. Bolat, E. Lefaucheux, and D. Marinho, “strategFTO: Untimed control for timed opacity,” in Proc. 8th ACM SIGPLAN Int. Workshop Formal Techniques for Safety-Critical Systems, Auckland, New Zealand, 2022, pp. 27–33.
[21]	B. Huang, M. C. Zhou, A. Abusorrah, and K. Sedraoui, “Scheduling robotic cellular manufacturing systems with timed Petri net, A^* search, and admissible heuristic function,” IEEE Trans. Autom. Sci. Eng., vol. 19, no. 1, pp. 243–250, Jan. 2022. doi: 10.1109/TASE.2020.3026351
[22]	J. Wang, J. Wang, Q. Zeng, and G. Liu, “Formal analysis of emergency department staffing based on stochastic timed Petri net models,” IFAC-PapersOnLine, vol. 53, no. 4, pp. 405–410, Jan. 2020. doi: 10.1016/j.ifacol.2021.04.038
[23]	T. Qin, Y. Dong, L. Yin, and Z. Li, “Liveness enforcement for production systems modeled by time Petri nets,” Inf. Sci., vol. 648, p. 119564, Nov. 2023. doi: 10.1016/j.ins.2023.119564
[24]	J. Yang, X. Wang, and Y. Zhao, “Parallel manufacturing for industrial metaverses: A new paradigm in smart manufacturing,” IEEE/CAA J. Autom. Sinica, vol. 9, no. 12, pp. 2063–2070, Dec. 2022. doi: 10.1109/JAS.2022.106097
[25]	H. Boucheneb, K. Barkaoui, Q. Xing, K. Wang, G. Liu, and Z. Li, “Time based deadlock prevention for Petri nets,” Automatica, vol. 137, p. 110119, Mar. 2022.
[26]	J. Wang, “Healthcare patient flow modeling and analysis with timed Petri nets,” in Advances in Computing, Informatics, Networking and Cybersecurity, P. Nicopolitidis, S. Misra, L. T. Yang, B. Zeigler, and Z. Ning, Eds. Cham, Germany: Springer, 2022, pp. 181–204.
[27]	J. Wang, “Patient flow modeling and optimal staffing for emergency departments: A Petri net approach,” IEEE Trans. Comput. Soc. Syst., vol. 10, no. 4, pp. 2022–2032, Aug. 2023. doi: 10.1109/TCSS.2022.3186249
[28]	A. M. Mangini and M. Roccotelli, “Innovative services for electric mobility based on virtual sensors and Petri nets,” IEEE/CAA J. Autom. Sinica, vol. 10, no. 9, pp. 1845–1859, Sep. 2023. doi: 10.1109/JAS.2023.123699
[29]	R. Hadjidj and H. Boucheneb, “Efficient reachability analysis for time Petri nets,” IEEE Trans. Comput., vol. 60, no. 8, pp. 1085–1099, Aug. 2011. doi: 10.1109/TC.2010.195
[30]	X. Wang, C. Mahulea, and M. Silva, “Diagnosis of time Petri nets using fault diagnosis graph,” IEEE Trans. Automat. Contr., vol. 60, no. 9, pp. 2321–2335, Sep. 2015. doi: 10.1109/TAC.2015.2405293
[31]	L. Li, F. Basile, and Z. Li, “Closed-loop deadlock-free supervision for GMECs in time Petri net systems,” IEEE Trans. Automat. Contr., vol. 66, no. 11, pp. 5326–5341, Nov. 2021. doi: 10.1109/TAC.2020.3044520
[32]	F. Basile, M. P. Cabasino, and C. Seatzu, “Diagnosability analysis of labeled time Petri net systems,” IEEE Trans. Automat. Contr., vol. 62, no. 3, pp. 1384–1396, Mar. 2017. doi: 10.1109/TAC.2016.2588736
[33]	Z. Ma, Z. Li, and A. Giua, “Marking estimation in a class of time labeled Petri nets,” IEEE Trans. Automat. Contr., vol. 65, no. 2, pp. 493–506, Feb. 2020. doi: 10.1109/TAC.2019.2907413
[34]	X. Cong, M. P. Fanti, A. M. Mangini, and Z. Li, “Critical observability of labeled time Petri net systems,” IEEE Trans. Autom. Sci. Eng., vol. 20, no. 3, pp. 2063–2074, Jul. 2023. doi: 10.1109/TASE.2022.3193493
[35]	F. Basile, M. P. Cabasino, and C. Seatzu, “State estimation and fault diagnosis of labeled time Petri net systems with unobservable transitions,” IEEE Trans. Automat. Contr., vol. 60, no. 4, pp. 997–1009, Apr. 2015. doi: 10.1109/TAC.2014.2363916
[36]	I. Ammar, Y. El Touati, M. Yeddes, and J. Mullins, “Bounded opacity for timed systems,” J. Inf. Secur. Appl., vol. 61, p. 102926, Sep. 2021.
[37]	L. Wang, N. Zhan, and J. An, “The opacity of real-time automata,” IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst., vol. 37, no. 11, pp. 2845–2856, Nov. 2018. doi: 10.1109/TCAD.2018.2857363
[38]	K. Zhang, “State-based opacity of labeled real-time automata,” Theor. Comput. Sci., vol. 987, p. 114373, Mar. 2024. doi: 10.1016/j.tcs.2023.114373
[39]	C. G. Cassandras and S. Lafortune, Introduction to Discrete Event Systems. 3rd ed. Cham, Switzerland: Springer, 2021.
[40]	T. Qin, L. Yin, N. Wu, and Z. Li, “Verification of current-state opacity in time labeled Petri nets with its application to smart houses,” IEEE Trans. Autom. Sci. Eng., 2023. doi: 10.1109/TASE.2023.3346523
[41]	B. Bérard, F. Cassez, S. Haddad, D. Lime, and O. H. Roux, “Comparison of different semantics for time Petri nets,” in Proc. 3rd Int. Symp. Automated Technology for Verification and Analysis, Taipei, China, 2005, pp. 293–307.
[42]	C. Seatzu, M. Silva, and J. H. van Schuppen, Control of Discrete-Event Systems: Automata and Petri Net Perspectives. New York, USA: Springer, 2013.

Supplements(0)

Cited By

Proportional views

Proportional views

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

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

Figures(7) / Tables(2)

Get Citation

PDF

XML

Article Metrics

Article views (33) PDF downloads(11)

Strong Current-State Opacity Verification of Discrete-Event Systems Modeled With Time Labeled Petri Nets

doi: 10.1109/JAS.2024.124560

Abstract

References

Proportional views

Catalog

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

Article Metrics

Export File

Citation

Format

Content