Current-State Opacity Verification in Petri Nets Using Fusion-Based Opacity Analysis and Graph Isomorphism Networks

Sichen Ding; Zhiwu Li

doi:10.1109/JAS.2025.125936

Volume 13 Issue 5

May 2026

IEEE/CAA Journal of Automatica Sinica

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

CiteScore: 28.2, Top 1% (Q1)
Google Scholar h5-index: 95， TOP 5

Turn off MathJax

Article Contents

Article Navigation > IEEE/CAA Journal of Automatica Sinica > 2026 > 13(5): 1122-1134

S. Ding and Z. Li, “Current-state opacity verification in Petri nets using fusion-based opacity analysis and graph isomorphism networks,” IEEE/CAA J. Autom. Sinica, vol. 13, no. 5, pp. 1122–1134, May 2026. doi: 10.1109/JAS.2025.125936

Citation:

S. Ding and Z. Li, “Current-state opacity verification in Petri nets using fusion-based opacity analysis and graph isomorphism networks,” IEEE/CAA J. Autom. Sinica, vol. 13, no. 5, pp. 1122–1134, May 2026. doi: 10.1109/JAS.2025.125936

Citation:

PDF( 1264 KB)

Current-State Opacity Verification in Petri Nets Using Fusion-Based Opacity Analysis and Graph Isomorphism Networks

doi: 10.1109/JAS.2025.125936

Sichen Ding^,,
Zhiwu Li^{,
,}

Funds: This work was partially supported by the Science Technology Development Fund, MSAR (0029/2023/RIA1)

More Information

Abstract

Abstract

Current-state opacity is a critical security property for discrete event systems, but its verification in large-scale Petri nets is hampered by the state-space explosion problem. To address this challenge, we propose the fusion-based opacity analysis and graph isomorphism network (FOA-GIN), a novel deep learning framework. The method transforms current-state opacity verification into a graph classification task by applying a tailored graph isomorphism network to basis reachability graphs—a compact representation of the system’s dynamics. This approach integrates the theoretical strengths of basis reachability graphs with the scalability of graph neural networks to capture essential structural and behavioral features for opacity analysis. Unlike classical algorithms that require exponential state-space traversal, the proposed model’s online verification complexity is linear in the size of the input basis reachability graph. Experiments demonstrate high accuracy and robustness, establishing FOA-GIN as a powerful and practical solution for verifying current-state opacity in complex, large-scale systems.

FullText(HTML)

References(37)

References

[1]	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, May 2022.
[2]	L. Mazaré, “Using unification for opacity properties,” in Proc. 4th IFIP WG1.7 Workshop on Issues in the Theory of Security, Barcelona, Spain, 2004, pp. 165−176.
[3]	J. W. Bryans, M. Koutny, L. Mazaré, and P. Y. A. Ryan, “Opacity generalised to transition systems,” Int. J. Inf. Secur., vol. 7, no. 6, pp. 421–435, May 2008. doi: 10.1007/s10207-008-0058-x
[4]	J. W. Bryans, M. Koutny, and P. Y. A. Ryan, “Modelling opacity using Petri nets,” Electron. Notes Theor. Comput. Sci., vol. 121, pp. 101–115, Feb. 2005. doi: 10.1016/j.entcs.2004.10.010
[5]	A. Saboori and C. N. Hadjicostis, “Notions of security and opacity in discrete event systems,” in Proc. 46th IEEE Conf. Decision and Control, New Orleans, USA, 2007, pp. 5056−5061.
[6]	F. Cassez, “The dark side of timed opacity,” in Proc. 3rd Int. Conf. and Workshops on Advances in Information Security and Assurance, Seoul, Korea (South), 2009, pp. 21−30.
[7]	A. Saboori and C. N. Hadjicostis, “Verification of initial-state opacity in security applications of discrete event systems,” Inf. Sci., vol. 246, pp. 115–132, Oct. 2013. doi: 10.1016/j.ins.2013.05.033
[8]	Y. C. Wu and S. Lafortune, “Comparative analysis of related notions of opacity in centralized and coordinated architectures,” Discret. Event Dyn. Syst., vol. 23, no. 3, pp. 307–339, Sep. 2013. doi: 10.1007/s10626-012-0145-z
[9]	E. Badouel, M. Bednarczyk, A. Borzyszkowski, B. Caillaud, and P. Darondeau, “Concurrent secrets,” Discret. Event Dyn. Syst., vol. 17, no. 4, pp. 425–446, Dec. 2007. doi: 10.1007/s10626-007-0020-5
[10]	Y. Falcone and H. Marchand, “Enforcement and validation (at runtime) of various notions of opacity,” Discret. Event Dyn. Syst., vol. 25, no. 4, pp. 531–570, Dec. 2015. doi: 10.1007/s10626-014-0196-4
[11]	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., vol. 21, no. 4, pp. 7616–7628, Oct. 2024. doi: 10.1109/TASE.2023.3346523
[12]	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. 54–68, Jan. 2025. doi: 10.1109/JAS.2024.124560
[13]	F. Cassez, J. Dubreil, and H. Marchand, “Dynamic observers for the synthesis of opaque systems,” in Proc. 7th Int. Symp. Automated Technology for Verification and Analysis, Macao, China, 2009, pp. 352−367.
[14]	R. Jacob, J. J. Lesage, and J. M. Faure, “Overview of discrete event systems opacity: Models, validation, and quantification,” Annu. Rev. Control, vol. 41, pp. 135−146, 2016.
[15]	C. N. Hadjicostis and C. Keroglou, “Opacity formulations and verification in discrete event systems,” in Proc. IEEE Emerging Technology and Factory Automation, Barcelona, Spain, 2014, pp. 1−12.
[16]	M. P. Cabasino, A. Giua, and C. Seatzu, “Fault detection for discrete event systems using Petri nets with unobservable transitions,” Automatica, vol. 46, no. 9, pp. 1531–1539, Sep. 2010. doi: 10.1016/j.automatica.2010.06.013
[17]	M. P. Cabasino, A. Giua, M. Pocci, and C. Seatzu, “Discrete event diagnosis using labeled Petri nets. An application to manufacturing systems,” Control Eng. Pract., vol. 19, no. 9, pp. 989–1001, Sep. 2011. doi: 10.1016/j.conengprac.2010.12.010
[18]	A. Giua, C. Seatzu, and D. Corona, “Marking estimation of Petri nets with silent transitions,” IEEE Trans. Autom. Control, vol. 52, no. 9, pp. 1695–1699, Sep. 2007. doi: 10.1109/TAC.2007.904281
[19]	M. P. Cabasino, A. Giua, and C. Seatzu, “Diagnosability of discrete-event systems using labeled Petri nets,” IEEE Trans. Autom. Sci. Eng., vol. 11, no. 1, pp. 144–153, Jan. 2014. doi: 10.1109/TASE.2013.2289360
[20]	Z. Ma, Y. Tong, Z. Li, and A. Giua, “Basis marking representation of Petri net reachability spaces and its application to the reachability problem,” IEEE Trans. Autom. Control, vol. 62, no. 3, pp. 1078–1093, Mar. 2017. doi: 10.1109/TAC.2016.2574120
[21]	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, Jun. 2017. doi: 10.1109/TAC.2016.2620429
[22]	I. Saadaoui, Z. Li, and N. Wu, “Current-state opacity modelling and verification in partially observed Petri nets,” Automatica, vol. 1089, Art. no. 11607, Jun. 2020. doi: 10.1016/j.automatica.2020.108907
[23]	Y. Dong, Z. Li, and N. Wu, “Symbolic verification of current-state opacity of discrete event systems using Petri nets,” IEEE Trans. Syst., Man, Cybern.: Syst., vol. 52, no. 12, pp. 7628–7641, Dec. 2022. doi: 10.1109/TSMC.2022.3151695
[24]	C. G. Cassandras and S. Lafortune, Introduction to Discrete Event Systems. 3rd ed. Cham, Germany: Springer, 2021.
[25]	T. N. Kipf and M. Welling, “Semi-supervised classification with graph convolutional networks,” in Proc. 5th Int. Conf. Learning Representations, Toulon, France, 2017, pp. 1−14.
[26]	P. Veličković, G. Cucurull, A. Casanova, A. Romero, P. Liò, and Y. Bengio, “Graph attention networks,” in Proc. 6th Int. Conf. Learning Representations, Vancouver, Canada, 2018, pp. 1−12.
[27]	W. L. Hamilton, R. Ying, and J. Leskovec, “Inductive representation learning on large graphs,” in Proc. 31st Int. Conf. Neural Information Processing Systems, Long Beach, USA, 2017, pp. 1025−1035.
[28]	Y. Yuan, Y. Wang, and X. Luo, “A node-collaboration-informed graph convolutional network for highly accurate representation to undirected weighted graph,” IEEE Trans. Neural Netw., vol. 36, no. 6, pp. 11507–11519, Jun. 2025. doi: 10.1109/tnnls.2024.3514652/mm1
[29]	L. Wang, K. Liu, and Y. Yuan, “GT-A.2T: Graph tensor alliance attention network,” IEEE/CAA J. Autom. Sinica, vol. 12, no. 10, pp. 2165–2167, Oct. 2025. doi: 10.1109/JAS.2024.124863
[30]	M. Han, L. Wang, Y. Yuan, and X. Luo, “SGD-DyG: Self-reliant global dependency apprehending on dynamic graphs,” in Proc. 31st ACM SIGKDD Conf. Knowledge Discovery and Data Mining V.2, Toronto, Canada, 2025, pp. 802−813.
[31]	K. Xu, W. Hu, J. Leskovec, and S. Jegelka, “How powerful are graph neural networks?” in Proc. 7th Int. Conf. Learning Representations, New Orleans, USA, 2019, pp. 1−17.
[32]	W. Hu, B. Liu, J. Gomes, M. Zitnik, P. Liang, V. Pande, and J. Leskovec, “Strategies for pre-training graph neural networks,” in Proc. 8th Int. Conf. Learning Representations, Addis Ababa, Ethiopia, 2020, pp. 1−22.
[33]	H. Qi, J. Wang, C. Yan, and C. Jiang, “The probabilistic liveness decision method of unbounded Petri nets based on machine learning,” IEEE Trans. Syst., Man, Cybern.: Syst., vol. 54, no. 2, pp. 1070–1081, Feb. 2024. doi: 10.1109/TSMC.2023.3323342
[34]	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
[35]	K. Hornik, M. Stinchcombe, and H. White, “Multilayer feedforward networks are universal approximators,” Neural Networks, vol. 2, no. 5, pp. 359−366, 1989.
[36]	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
[37]	R. Ying, D. Bourgeois, J. You, M. Zitnik, and J. Leskovec, “GNNExplainer: Generating explanations for graph neural networks,” in Proc. 33rd Int. Conf. Neural Information Processing Systems, Vancouver, Canada, 2019, Article No. 829.