IEEE/CAA Journal of Automatica Sinica
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. 54–68, Jan. 2025. doi: 10.1109/JAS.2024.124560 |
[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.
|