{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,24]],"date-time":"2026-07-24T22:35:22Z","timestamp":1784932522865,"version":"3.55.0"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031711619","type":"print"},{"value":"9783031711626","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T00:00:00Z","timestamp":1726012800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T00:00:00Z","timestamp":1726012800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Opacity serves as a critical security and confidentiality property, which concerns whether an intruder can unveil a system\u2019s secret based on structural knowledge and observed behaviors. Opacity in timed systems presents greater complexity compared to untimed systems, and it has been established that opacity for timed automata is undecidable. However, the original proof cannot be applied to decide the opacity of one-clock timed automata directly. In this paper, we explore three types of opacity within timed automata: language-based timed opacity, initial-location timed opacity, and current-location timed opacity. We begin by formalizing these concepts and establishing transformation relations among them. Subsequently, we demonstrate the undecidability of the opacity problem for one-clock timed automata. Furthermore, we offer a constructive proof for the conjecture regarding the decidability of opacity for timed automata in discrete-time semantics. Additionally, we present a sufficient condition and a necessary condition for the decidability of opacity in specific subclasses of timed automata.<\/jats:p>","DOI":"10.1007\/978-3-031-71162-6_32","type":"book-chapter","created":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T02:02:27Z","timestamp":1725933747000},"page":"620-637","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["The Opacity of\u00a0Timed Automata"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9260-9697","authenticated-orcid":false,"given":"Jie","family":"An","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Qiang","family":"Gao","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lingtai","family":"Wang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3298-3817","authenticated-orcid":false,"given":"Naijun","family":"Zhan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8300-4650","authenticated-orcid":false,"given":"Ichiro","family":"Hasuo","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2024,9,11]]},"reference":[{"key":"32_CR1","unstructured":"Abdulla, P.A., Deneux, J., Ouaknine, J., Quaas, K., Worrell, J.: Universality analysis for one-clock timed automata. Fundam. Informaticae 89(4), 419\u2013450 (2008). http:\/\/content.iospress.com\/articles\/fundamenta-informaticae\/fi89-4-04"},{"issue":"2","key":"32_CR2","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183\u2013235 (1994). https:\/\/doi.org\/10.1016\/0304-3975(94)90010-8","journal-title":"Theor. Comput. Sci."},{"issue":"1\u20132","key":"32_CR3","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1016\/S0304-3975(97)00173-4","volume":"211","author":"R Alur","year":"1999","unstructured":"Alur, R., Fix, L., Henzinger, T.A.: Event-clock automata: a determinizable class of timed automata. Theor. Comput. Sci. 211(1\u20132), 253\u2013273 (1999). https:\/\/doi.org\/10.1016\/S0304-3975(97)00173-4","journal-title":"Theor. Comput. Sci."},{"key":"32_CR4","doi-asserted-by":"publisher","unstructured":"Ammar, I., Touati, Y.E., Yeddes, M., Mullins, J.: Bounded opacity for timed systems. J. Inf. Secur. Appl. 61, 102926:1\u2013102926:13 (2021). https:\/\/doi.org\/10.1016\/j.jisa.2021.102926","DOI":"10.1016\/j.jisa.2021.102926"},{"key":"32_CR5","doi-asserted-by":"publisher","unstructured":"Andr\u00e9, \u00c9., Lime, D., Marinho, D., Sun, J.: Guaranteeing timed opacity using parametric timed model checking. ACM Trans. Softw. Eng. Methodol. 31(4), 64:1\u201364:36 (2022). https:\/\/doi.org\/10.1145\/3502851","DOI":"10.1145\/3502851"},{"key":"32_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/978-3-030-31784-3_7","volume-title":"Automated Technology for Verification and Analysis","author":"\u00c9 Andr\u00e9","year":"2019","unstructured":"Andr\u00e9, \u00c9., Sun, J.: Parametric timed model checking for guaranteeing timed opacity. In: Chen, Y.-F., Cheng, C.-H., Esparza, J. (eds.) ATVA 2019. LNCS, vol. 11781, pp. 115\u2013130. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-31784-3_7"},{"issue":"4","key":"32_CR7","doi-asserted-by":"publisher","first-page":"425","DOI":"10.1007\/s10626-007-0020-5","volume":"17","author":"\u00c9 Badouel","year":"2007","unstructured":"Badouel, \u00c9., Bednarczyk, M.A., Borzyszkowski, A.M., Caillaud, B., Darondeau, P.: Concurrent secrets. Discret. Event. Dyn. Syst. 17(4), 425\u2013446 (2007). https:\/\/doi.org\/10.1007\/s10626-007-0020-5","journal-title":"Discret. Event. Dyn. Syst."},{"key":"32_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/978-3-540-27755-2_3","volume-title":"Lectures on Concurrency and Petri Nets","author":"J Bengtsson","year":"2004","unstructured":"Bengtsson, J., Yi, W.: Timed automata: semantics, algorithms and tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) ACPN 2003. LNCS, vol. 3098, pp. 87\u2013124. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-27755-2_3"},{"key":"32_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/3-540-60922-9_22","volume-title":"STACS 96","author":"B B\u00e9rard","year":"1996","unstructured":"B\u00e9rard, B., Gastin, P., Petit, A.: On the power of non-observable actions in timed automata. In: Puech, C., Reischuk, R. (eds.) STACS 1996. LNCS, vol. 1046, pp. 255\u2013268. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-60922-9_22"},{"key":"32_CR10","doi-asserted-by":"publisher","unstructured":"Bortz, A., Boneh, D.: Exposing private information by timing web applications. In: Williamson, C.L., Zurko, M.E., Patel-Schneider, P.F., Shenoy, P.J. (eds.) WWW 2007, pp. 621\u2013628. ACM (2007). https:\/\/doi.org\/10.1145\/1242572.1242656","DOI":"10.1145\/1242572.1242656"},{"key":"32_CR11","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":"32_CR12","doi-asserted-by":"publisher","unstructured":"Dima, C.: Real-time automata. J. Autom. Lang. Comb. 6(1), 3\u201323 (2001). https:\/\/doi.org\/10.25596\/jalc-2001-003","DOI":"10.25596\/jalc-2001-003"},{"issue":"4","key":"32_CR13","doi-asserted-by":"publisher","first-page":"531","DOI":"10.1007\/s10626-014-0196-4","volume":"25","author":"Y Falcone","year":"2015","unstructured":"Falcone, Y., Marchand, H.: Enforcement and validation (at runtime) of various notions of opacity. Discret. Event Dyn. Syst. 25(4), 531\u2013570 (2015). https:\/\/doi.org\/10.1007\/s10626-014-0196-4","journal-title":"Discret. Event Dyn. Syst."},{"key":"32_CR14","doi-asserted-by":"publisher","unstructured":"Felten, E.W., Schneider, M.A.: Timing attacks on web privacy. In: Gritzalis, D., Jajodia, S., Samarati, P. (eds.) CCS 2000, pp. 25\u201332. ACM (2000). https:\/\/doi.org\/10.1145\/352600.352606","DOI":"10.1145\/352600.352606"},{"key":"32_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1007\/11505877_24","volume-title":"Developments in Language Theory","author":"H Gruber","year":"2005","unstructured":"Gruber, H., Holzer, M., Kiehn, A., K\u00f6nig, B.: On timed automata with discrete time \u2013 structural and language theoretical characterization. In: De Felice, C., Restivo, A. (eds.) DLT 2005. LNCS, vol. 3572, pp. 272\u2013283. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11505877_24"},{"key":"32_CR16","doi-asserted-by":"publisher","unstructured":"Han, X., Zhang, K., Li, Z.: Verification of strong k-step opacity for discrete-event systems. In: CDC 2022, pp. 4250\u20134255. IEEE (2022). https:\/\/doi.org\/10.1109\/CDC51059.2022.9993023","DOI":"10.1109\/CDC51059.2022.9993023"},{"key":"32_CR17","unstructured":"Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages and Computation. Addison-Wesley (1979)"},{"key":"32_CR18","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1016\/j.arcontrol.2016.04.015","volume":"41","author":"R Jacob","year":"2016","unstructured":"Jacob, R., Lesage, J., Faure, J.: Overview of discrete event systems opacity: models, validation, and quantification. Annu. Rev. Control. 41, 135\u2013146 (2016). https:\/\/doi.org\/10.1016\/j.arcontrol.2016.04.015","journal-title":"Annu. Rev. Control."},{"key":"32_CR19","doi-asserted-by":"publisher","unstructured":"Jancar, J., et al.: \u201cThey\u2019re not that hard to mitigate\u201d: what cryptographic library developers think about timing attacks. In: S &P 2022, pp. 632\u2013649. IEEE (2022). https:\/\/doi.org\/10.1109\/SP46214.2022.9833713","DOI":"10.1109\/SP46214.2022.9833713"},{"issue":"3","key":"32_CR20","doi-asserted-by":"publisher","first-page":"496","DOI":"10.1016\/j.automatica.2011.01.002","volume":"47","author":"F Lin","year":"2011","unstructured":"Lin, F.: Opacity of discrete event systems and its applications. Automatica 47(3), 496\u2013503 (2011). https:\/\/doi.org\/10.1016\/j.automatica.2011.01.002","journal-title":"Automatica"},{"key":"32_CR21","doi-asserted-by":"publisher","unstructured":"Liu, S., Yin, X., Zamani, M.: On a notion of approximate opacity for discrete-time stochastic control systems. In: ACC 2020, pp. 5413\u20135418. IEEE (2020). https:\/\/doi.org\/10.23919\/ACC45564.2020.9147235","DOI":"10.23919\/ACC45564.2020.9147235"},{"key":"32_CR22","doi-asserted-by":"publisher","unstructured":"Ouaknine, J., Worrell, J.: Revisiting digitization, robustness, and decidability for timed automata. In: LICS 2003, pp. 198\u2013207. IEEE Computer Society (2003). https:\/\/doi.org\/10.1109\/LICS.2003.1210059","DOI":"10.1109\/LICS.2003.1210059"},{"key":"32_CR23","doi-asserted-by":"publisher","unstructured":"Saboori, A., Hadjicostis, C.N.: Notions of security and opacity in discrete event systems. In: CDC 2007, pp. 5056\u20135061. IEEE (2007). https:\/\/doi.org\/10.1109\/CDC.2007.4434515","DOI":"10.1109\/CDC.2007.4434515"},{"issue":"5","key":"32_CR24","doi-asserted-by":"publisher","first-page":"1265","DOI":"10.1109\/TAC.2011.2173774","volume":"57","author":"A Saboori","year":"2012","unstructured":"Saboori, A., Hadjicostis, C.N.: Verification of infinite-step opacity and complexity considerations. IEEE Trans. Autom. Control 57(5), 1265\u20131269 (2012). https:\/\/doi.org\/10.1109\/TAC.2011.2173774","journal-title":"IEEE Trans. Autom. Control"},{"key":"32_CR25","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/j.ins.2013.05.033","volume":"246","author":"A Saboori","year":"2013","unstructured":"Saboori, A., Hadjicostis, C.N.: Verification of initial-state opacity in security applications of discrete event systems. Inf. Sci. 246, 115\u2013132 (2013). https:\/\/doi.org\/10.1016\/j.ins.2013.05.033","journal-title":"Inf. Sci."},{"key":"32_CR26","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":"32_CR27","doi-asserted-by":"publisher","unstructured":"Wang, L., Zhan, N., An, J.: The opacity of real-time automata. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 37(11), 2845\u20132856 (2018). https:\/\/doi.org\/10.1109\/TCAD.2018.2857363","DOI":"10.1109\/TCAD.2018.2857363"},{"issue":"3","key":"32_CR28","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/s10626-012-0145-z","volume":"23","author":"Y Wu","year":"2013","unstructured":"Wu, Y., Lafortune, S.: Comparative analysis of related notions of opacity in centralized and coordinated architectures. Discret. Event Dyn. Syst. 23(3), 307\u2013339 (2013). https:\/\/doi.org\/10.1007\/s10626-012-0145-z","journal-title":"Discret. Event Dyn. Syst."},{"key":"32_CR29","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1016\/j.automatica.2017.02.037","volume":"80","author":"X Yin","year":"2017","unstructured":"Yin, X., Lafortune, S.: A new approach for the verification of infinite-step and k-step opacity using two-way observers. Automatica 80, 162\u2013171 (2017). https:\/\/doi.org\/10.1016\/j.automatica.2017.02.037","journal-title":"Automatica"},{"issue":"4","key":"32_CR30","doi-asserted-by":"publisher","first-page":"1630","DOI":"10.1109\/TAC.2020.2998733","volume":"66","author":"X Yin","year":"2021","unstructured":"Yin, X., Zamani, M., Liu, S.: On approximate opacity of cyber-physical systems. IEEE Trans. Autom. Control 66(4), 1630\u20131645 (2021). https:\/\/doi.org\/10.1109\/TAC.2020.2998733","journal-title":"IEEE Trans. Autom. Control"},{"key":"32_CR31","doi-asserted-by":"publisher","unstructured":"Zhang, K.: State-based opacity of real-time automata. In: Castillo-Ramirez, A., Guillon, P., Perrot, K. (eds.) 27th IFIP WG 1.5 International Workshop on Cellular Automata and Discrete Complex Systems, AUTOMATA 2021. OASIcs, vol.\u00a090, pp. 12:1\u201312:15. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2021). https:\/\/doi.org\/10.4230\/OASIcs.AUTOMATA.2021.12","DOI":"10.4230\/OASIcs.AUTOMATA.2021.12"}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-71162-6_32","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T02:08:44Z","timestamp":1725934124000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-71162-6_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9,11]]},"ISBN":["9783031711619","9783031711626"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-71162-6_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,9,11]]},"assertion":[{"value":"11 September 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Milan","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 September 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 September 2024","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":"fm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.fm24.polimi.it\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}