{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T15:14:24Z","timestamp":1784214864267,"version":"3.55.0"},"publisher-location":"Singapore","reference-count":23,"publisher":"Springer Nature Singapore","isbn-type":[{"value":"9789819542123","type":"print"},{"value":"9789819542130","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,11,11]],"date-time":"2025-11-11T00:00:00Z","timestamp":1762819200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,11,11]],"date-time":"2025-11-11T00:00:00Z","timestamp":1762819200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-981-95-4213-0_16","type":"book-chapter","created":{"date-parts":[[2025,11,10]],"date-time":"2025-11-10T23:17:53Z","timestamp":1762816673000},"page":"285-304","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["A Unified Method to\u00a0Efficiently Verify Opacity of\u00a0Discrete-Timed Automata"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0005-2899-3934","authenticated-orcid":false,"given":"Julian","family":"Klein","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9547-103X","authenticated-orcid":false,"given":"Kuize","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-6946-3257","authenticated-orcid":false,"given":"Sabine","family":"Glesner","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,11,11]]},"reference":[{"key":"16_CR1","doi-asserted-by":"publisher","unstructured":"Alur, R., Dill, D.: The theory of timed automata. Theor. Comput. Sci. 183\u2013235 (1992). https:\/\/doi.org\/10.1016\/0304-3975(94)90010-8","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"16_CR2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jisa.2021.102926","author":"I Ammar","year":"2021","unstructured":"Ammar, I., El Touati, Y., Yeddes, M., Mullins, J.: Bounded opacity for timed systems. J. Inf. Secur. Appl. (2021). https:\/\/doi.org\/10.1016\/j.jisa.2021.102926","journal-title":"J. Inf. Secur. Appl."},{"key":"16_CR3","doi-asserted-by":"publisher","unstructured":"An, J., Gao, Q., Wang, L., Zhan, N., Hasuo, I.: The opacity of timed automata. In: Proceedings of the 2024 26th International Symposium on Formal Methods (FM). FM 2024, pp. 620\u2013637. Springer, Cham (2025). https:\/\/doi.org\/10.1007\/978-3-031-71162-6_32","DOI":"10.1007\/978-3-031-71162-6_32"},{"key":"16_CR4","doi-asserted-by":"publisher","unstructured":"Andr\u00e9, \u00c9., D\u00e9pernet, S., Lefaucheux, E.: The bright side of timed opacity. In: Proceedings of the 2024 25th International Conference on Formal Engineering Methods (ICFEM). ICFEM 2024, pp. 51\u201369. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-981-96-0617-7_4","DOI":"10.1007\/978-981-96-0617-7_4"},{"key":"16_CR5","doi-asserted-by":"publisher","unstructured":"Andr\u00e9, \u00c9., Lefaucheux, E., Marinho, D.: Expiring opacity problems in parametric timed automata. In: Proceedings of the 2023 27th International Conference on Engineering of Complex Computer Systems (ICECCS). ICECCS 2023, pp. 89\u201398. IEEE (2023). https:\/\/doi.org\/10.1109\/ICECCS59891.2023.00020","DOI":"10.1109\/ICECCS59891.2023.00020"},{"key":"16_CR6","doi-asserted-by":"publisher","unstructured":"Andr\u00e9, E., Lime, D., Marinho, D., Sun, J.: Guaranteeing timed opacity using parametric timed model checking. ACM Trans. Softw. Eng. Methodol. 64\u2013100 (2022). https:\/\/doi.org\/10.1145\/3502851","DOI":"10.1145\/3502851"},{"key":"16_CR7","doi-asserted-by":"publisher","unstructured":"Balun, J., Masopust, T.: On transformations among opacity notions. In: Proceedings of the 2022 25th IEEE International Conference on Systems, Man, and Cybernetics (SMC). SMC 2022, pp. 3012\u20133017. IEEE (2022). https:\/\/doi.org\/10.1109\/SMC53654.2022.9945608","DOI":"10.1109\/SMC53654.2022.9945608"},{"key":"16_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-642-02617-1_3","volume-title":"Advances in Information Security and Assurance","author":"F Cassez","year":"2009","unstructured":"Cassez, F.: The dark side of timed opacity. In: Park, J.H., Chen, H.-H., Atiquzzaman, M., Lee, C., Kim, T., Yeo, S.-S. (eds.) ISA 2009. LNCS, vol. 5576, pp. 21\u201330. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02617-1_3"},{"key":"16_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1007\/978-3-642-04761-9_26","volume-title":"Automated Technology for Verification and Analysis","author":"F Cassez","year":"2009","unstructured":"Cassez, F., Dubreil, J., Marchand, H.: Dynamic observers for the synthesis of opaque systems. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol. 5799, pp. 352\u2013367. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04761-9_26"},{"key":"16_CR10","unstructured":"Deng, W., Qiu, D., Yang, J.: New insights into the decidability of opacity in timed automata. arXiv preprint arXiv:2504.00625 (2025)"},{"key":"16_CR11","doi-asserted-by":"publisher","unstructured":"Klein, J., Kogel, P., Glesner, S.: Efficient state estimation of discrete-timed automata. In: Proceedings of the 2024 25th International Conference on Formal Engineering Methods (ICFEM). ICFEM 2024, pp. 85\u2013105. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-981-96-0617-7_6","DOI":"10.1007\/978-981-96-0617-7_6"},{"key":"16_CR12","doi-asserted-by":"publisher","unstructured":"Klein, J., Kogel, P., Glesner, S.: Verifying opacity of discrete-timed automata. In: Proceedings of the 2024 IEEE\/ACM 12th International Conference on Formal Methods in Software Engineering (FormaliSE). FormaliSE 2024, pp. 55\u201365. Association for Computing Machinery (2024). https:\/\/doi.org\/10.1145\/3644033.3644376","DOI":"10.1145\/3644033.3644376"},{"key":"16_CR13","doi-asserted-by":"publisher","unstructured":"Klein, J., Zhang, K., Glesner, S.: A unified method to efficiently verify opacity of discrete-timed automata - software prototype (2025). https:\/\/doi.org\/10.5281\/zenodo.16994338","DOI":"10.5281\/zenodo.16994338"},{"key":"16_CR14","doi-asserted-by":"publisher","unstructured":"Li, J., Lefebvre, D., Hadjicostis, C.N., Li, Z.: Observers for a class of timed automata based on elapsed time graphs. IEEE Trans. Autom. Control. 767\u2013779 (2021). https:\/\/doi.org\/10.1109\/TAC.2021.3064542","DOI":"10.1109\/TAC.2021.3064542"},{"key":"16_CR15","doi-asserted-by":"publisher","unstructured":"Li, J., Lefebvre, D., Hadjicostis, C.N., Li, Z.: Verification of state-based timed opacity for constant-time labeled automata. IEEE Trans. Autom. Control, 503\u2013509 (2025). https:\/\/doi.org\/10.1109\/TAC.2024.3432788","DOI":"10.1109\/TAC.2024.3432788"},{"key":"16_CR16","doi-asserted-by":"publisher","unstructured":"Noord, G.V.: Treatment of epsilon moves in subset construction. Comput. Linguist. 61\u201376 (2000). https:\/\/doi.org\/10.1162\/089120100561638","DOI":"10.1162\/089120100561638"},{"key":"16_CR17","doi-asserted-by":"publisher","unstructured":"Saboori, A., Hadjicostis, C.N.: Notions of security and opacity in discrete event systems. In: Proceedings of the 2007 46th International Conference on Conference on Decision and Control (CDC). CDC 2007, pp. 5056\u20135061. IEEE (2007). https:\/\/doi.org\/10.1109\/CDC.2007.4434515","DOI":"10.1109\/CDC.2007.4434515"},{"key":"16_CR18","doi-asserted-by":"publisher","unstructured":"Saboori, A., Hadjicostis, C.N.: Verification of k-step opacity and analysis of its complexity. IEEE Trans. Autom. Sci. Eng. 549\u2013559 (2011). https:\/\/doi.org\/10.1109\/TASE.2011.2106775","DOI":"10.1109\/TASE.2011.2106775"},{"key":"16_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1007\/978-3-030-01461-2_3","volume-title":"Symposium on Real-Time and Hybrid Systems","author":"L Wang","year":"2018","unstructured":"Wang, L., Zhan, N.: Decidability of the initial-state opacity of real-time automata. In: Jones, C., Wang, J., Zhan, N. (eds.) Symposium on Real-Time and Hybrid Systems. LNCS, vol. 11180, pp. 44\u201360. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-01461-2_3"},{"key":"16_CR20","doi-asserted-by":"publisher","unstructured":"Wang, L., Zhan, N., An, J.: The opacity of real-time automata. IEEE Trans. Comput.-Aided Des. Integr. Circ. Syst. 2845\u20132856 (2018). https:\/\/doi.org\/10.1109\/TCAD.2018.2857363","DOI":"10.1109\/TCAD.2018.2857363"},{"key":"16_CR21","doi-asserted-by":"publisher","unstructured":"Yin, X., Zamani, M., Liu, S.: On approximate opacity of cyber-physical systems. IEEE Trans. Autom. Control. 1630\u20131645 (2021). https:\/\/doi.org\/10.1109\/TAC.2020.2998733","DOI":"10.1109\/TAC.2020.2998733"},{"key":"16_CR22","doi-asserted-by":"publisher","DOI":"10.1016\/j.arcontrol.2023.100902","author":"K Zhang","year":"2023","unstructured":"Zhang, K.: A unified concurrent-composition method to state\/event inference and concealment in labeled finite-state automata as discrete-event systems. Annu. Rev. Control. (2023). https:\/\/doi.org\/10.1016\/j.arcontrol.2023.100902","journal-title":"Annu. Rev. Control."},{"key":"16_CR23","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2023.114373","author":"K Zhang","year":"2024","unstructured":"Zhang, K.: State-based opacity of labeled real-time automata. Theoret. Comput. Sci. (2024). https:\/\/doi.org\/10.1016\/j.tcs.2023.114373","journal-title":"Theoret. Comput. Sci."}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-981-95-4213-0_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,10]],"date-time":"2025-11-10T23:17:54Z","timestamp":1762816674000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-981-95-4213-0_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,11]]},"ISBN":["9789819542123","9789819542130"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-981-95-4213-0_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,11,11]]},"assertion":[{"value":"11 November 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ICFEM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Formal Engineering Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hangzhou","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"China","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 November 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 November 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"icfem2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/icfem2025.github.io\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}