{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,11]],"date-time":"2026-02-11T13:00:28Z","timestamp":1770814828512,"version":"3.50.1"},"reference-count":35,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2022,2,2]],"date-time":"2022-02-02T00:00:00Z","timestamp":1643760000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,2,2]],"date-time":"2022-02-02T00:00:00Z","timestamp":1643760000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Discrete Event Dyn Syst"],"published-print":{"date-parts":[[2022,6]]},"DOI":"10.1007\/s10626-021-00357-x","type":"journal-article","created":{"date-parts":[[2022,2,2]],"date-time":"2022-02-02T09:04:01Z","timestamp":1643792641000},"page":"253-289","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":25,"title":["A general language-based framework for specifying and verifying notions of opacity"],"prefix":"10.1007","volume":"32","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7522-5309","authenticated-orcid":false,"given":"Andrew","family":"Wintenberg","sequence":"first","affiliation":[]},{"given":"Matthew","family":"Blischke","sequence":"additional","affiliation":[]},{"given":"St\u00e9phane","family":"Lafortune","sequence":"additional","affiliation":[]},{"given":"Necmiye","family":"Ozay","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,2,2]]},"reference":[{"issue":"2","key":"357_CR1","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1017\/S0960129513000637","volume":"25","author":"B B\u00e9rard","year":"2015","unstructured":"B\u00e9rard B, Mullins J, Sassolas M (2015) Quantifying Opacity. Math Struct Comput Sci 25 (2):361\u2013403. https:\/\/doi.org\/10.1017\/S0960129513000637, arXiv:1301.6799","journal-title":"Math Struct Comput Sci"},{"key":"357_CR2","doi-asserted-by":"publisher","unstructured":"B\u00e9rard B, Haar S, Schmitz S, Schwoon S (2017) The Complexity of Diagnosability and Opacity Verification for Petri Nets. In Application and Theory of Petri Nets and Concurrency (pp. 200\u2013220). Springer International Publishing. https:\/\/doi.org\/10.1007\/978-3-319-57861-3_13","DOI":"10.1007\/978-3-319-57861-3_13"},{"key":"357_CR3","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/j.entcs.2004.10.010","volume":"121","author":"J Bryans","year":"2005","unstructured":"Bryans J, Koutny M, Ryan P (2005) Modelling Opacity Using Petri Nets. Electr Notes Theor Comput Sci 121:101\u2013115. https:\/\/doi.org\/10.1016\/j.entcs.2004.10.010","journal-title":"Electr Notes Theor Comput Sci"},{"issue":"6","key":"357_CR4","doi-asserted-by":"publisher","first-page":"421","DOI":"10.1007\/s10207-008-0058-x","volume":"7","author":"JW Bryans","year":"2008","unstructured":"Bryans J W, Koutny M, Mazar\u00e9 L, Ryan P Y A (2008) Opacity generalised to transition systems. Int J Inf Secur 7(6):421\u2013435. https:\/\/doi.org\/10.1007\/s10207-008-0058-x","journal-title":"Int J Inf Secur"},{"key":"357_CR5","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-68612-7","volume-title":"Introduction to discrete event systems","author":"CG Cassandras","year":"2008","unstructured":"Cassandras C G, Lafortune S (2008) Introduction to discrete event systems, 2nd edn. Springer, New York","edition":"2nd edn."},{"key":"357_CR6","doi-asserted-by":"crossref","unstructured":"Cassez F (2009) The Dark Side of Timed Opacity. In: Park J H, Chen H-H, Atiquzzaman M, Lee C, Kim T-, Yeo S-S (eds) Advances in Information Security and Assurance, Lecture Notes in Computer Science. Springer, Berlin, pp 21\u201330","DOI":"10.1007\/978-3-642-02617-1_3"},{"key":"357_CR7","doi-asserted-by":"crossref","unstructured":"Cassez F, Dubreil J, Marchand H (2009) Dynamic Observers for the Synthesis of Opaque Systems. In: Liu Z, Ravn A P (eds) Automated Technology for Verification and Analysis, Lecture Notes in Computer Science. Springer, Berlin, pp 352\u2013367","DOI":"10.1007\/978-3-642-04761-9_26"},{"key":"357_CR8","doi-asserted-by":"crossref","unstructured":"Clarkson M R, Finkbeiner B, Koleini M, Micinski K K, Rabe M N, S\u00e3nchez C (2014) Temporal Logics for Hyperproperties. In: Abadi M, Kremer S (eds) Principles of Security and Trust, Lecture Notes in Computer Science. Springer, Berlin, pp 265\u2013284","DOI":"10.1007\/978-3-642-54792-8_15"},{"issue":"1","key":"357_CR9","doi-asserted-by":"publisher","first-page":"5","DOI":"10.2168\/LMCS-5(1:5)2009","volume":"5","author":"L Doyen","year":"2009","unstructured":"Doyen L, Raskin J-F (2009) Antichains for the Automata-Based Approach to Model-Checking. Log Methods Comput Sci 5(1):5. https:\/\/doi.org\/10.2168\/LMCS-5(1:5)2009, arXiv:0902.3958","journal-title":"Log Methods Comput Sci"},{"issue":"5","key":"357_CR10","doi-asserted-by":"publisher","first-page":"1089","DOI":"10.1109\/TAC.2010.2042008","volume":"55","author":"J Dubreil","year":"2010","unstructured":"Dubreil J, Darondeau P, Marchand H (2010) Supervisory Control for Opacity. IEEE Trans Autom Control 55(5):1089\u20131100. https:\/\/doi.org\/10.1109\/TAC.2010.2042008, IEEE Transactions on Automatic Control","journal-title":"IEEE Trans Autom Control"},{"key":"357_CR11","doi-asserted-by":"publisher","unstructured":"Falcone Y, Marchand H (2013) Runtime Enforcement of K-step Opacity, pp 7271\u20137278. https:\/\/doi.org\/10.1109\/CDC.2013.6761043","DOI":"10.1109\/CDC.2013.6761043"},{"issue":"4","key":"357_CR12","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 (2015) Enforcement and validation (at runtime) of various notions of opacity. Discret Event Dyn Syst 25(4):531\u2013570. https:\/\/doi.org\/10.1007\/s10626-014-0196-4","journal-title":"Discret Event Dyn Syst"},{"key":"357_CR13","doi-asserted-by":"crossref","unstructured":"Focardi R, Gorrieri R, Martinelli F (2000) Non Interference for the Analysis of Cryptographic Protocols. In: Montanari U, Rolim J D P, Welzl E (eds) Automata, Languages and Programming, Lecture Notes in Computer Science. Springer, Berlin, pp 354\u2013372","DOI":"10.1007\/3-540-45022-X_31"},{"key":"357_CR14","doi-asserted-by":"publisher","unstructured":"Hadjicostis C N (2020) Introduction to Estimation and Inference in Discrete Event Systems. In: Hadjicostis C N (ed) Estimation and Inference in Discrete Event Systems: A Model-Based Approach with Finite Automata, Communications and Control Engineering. Springer International Publishing, Cham, pp 1\u201314. https:\/\/doi.org\/10.1007\/978-3-030-30821-6_1","DOI":"10.1007\/978-3-030-30821-6_1"},{"key":"357_CR15","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-J, Faure J-M (2016) Overview of discrete event systems opacity: Models, validation, and quantification. Annu Rev Control 41:135\u2013146. https:\/\/doi.org\/10.1016\/j.arcontrol.2016.04.015, https:\/\/www.sciencedirect.com\/science\/article\/pii\/S1367578816300189","journal-title":"Annu Rev Control"},{"key":"357_CR16","doi-asserted-by":"publisher","first-page":"109290","DOI":"10.1016\/j.automatica.2020.109290","volume":"122","author":"H Lan","year":"2020","unstructured":"Lan H, Tong Y, Guo J, Giua A (2020) Comments on \u201cA new approach for the verification of infinite-step and K-step opacity using two-way observers\u201d? [Automatica 80 (2017) 162\u2013171]. Automatica 122:109290. https:\/\/doi.org\/10.1016\/j.automatica.2020.109290, https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0005109820304891","journal-title":"Automatica"},{"issue":"3","key":"357_CR17","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 (2011) Opacity of discrete event systems and its applications. Automatica 47(3):496\u2013503. https:\/\/doi.org\/10.1016\/j.automatica.2011.01.002, http:\/\/www.sciencedirect.com\/science\/article\/pii\/S0005109811000173","journal-title":"Automatica"},{"key":"357_CR18","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1016\/j.automatica.2018.12.019","volume":"101","author":"T Masopust","year":"2019","unstructured":"Masopust T, Yin X (2019) Complexity of detectability, opacity and A-diagnosability for modular discrete event systems. Automatica 101:290\u2013295. https:\/\/doi.org\/10.1016\/j.automatica.2018.12.019, https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0005109818306253","journal-title":"Automatica"},{"key":"357_CR19","unstructured":"Mazar\u00e9 L (2004) Using unification for opacity properties. In: Proceedings of the Workshop on Issues in the Theory of Security (wits\u201904), pp 165\u2013176"},{"issue":"1","key":"357_CR20","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1145\/290163.290168","volume":"1","author":"MK Reiter","year":"1998","unstructured":"Reiter M K, Rubin A D (1998) Crowds: anonymity for Web transactions. ACM Trans Inf Syst Secur 1(1):66\u201392. https:\/\/doi.org\/10.1145\/290163.290168","journal-title":"ACM Trans Inf Syst Secur"},{"key":"357_CR21","doi-asserted-by":"crossref","unstructured":"Saboori A, Hadjicostis C N (2009a) Verification of K-step opacity and analysis of its complexity. In: Proceedings of the 48h IEEE Conference on Decision and Control (CDC) held jointly with 2009 28th Chinese Control Conference, pp 205\u2013210. ISSN: 0191-2216","DOI":"10.1109\/CDC.2009.5400083"},{"issue":"5","key":"357_CR22","doi-asserted-by":"publisher","first-page":"46","DOI":"10.3182\/20090610-3-IT-4004.00013","volume":"42","author":"A Saboori","year":"2009","unstructured":"Saboori A, Hadjicostis C N (2009b) Verification of infinite-step opacity and analysis of its complexity*. IFAC Proc Vol 42(5):46\u201351. https:\/\/doi.org\/10.3182\/20090610-3-IT-4004.00013, https:\/\/www.sciencedirect.com\/science\/article\/pii\/S1474667015355944","journal-title":"IFAC Proc Vol"},{"key":"357_CR23","doi-asserted-by":"crossref","unstructured":"Saboori A, Hadjicostis C N (2007) Notions of security and opacity in discrete event systems. In: 2007 46th IEEE Conference on Decision and Control, pp 5056\u20135061. ISSN: 0191-2216","DOI":"10.1109\/CDC.2007.4434515"},{"key":"357_CR24","doi-asserted-by":"crossref","unstructured":"Saboori A, Hadjicostis C N (2008) Verification of initial-state opacity in security applications of DES. In: 2008 9th International Workshop on Discrete Event Systems, pp 328\u2013333","DOI":"10.1109\/WODES.2008.4605967"},{"key":"357_CR25","doi-asserted-by":"publisher","unstructured":"Stockmeyer L J, Meyer A R (1973) Word problems requiring exponential time(Preliminary Report). In: Proceedings of the fifth annual ACM symposium on Theory of computing, STOC \u201973. https:\/\/doi.org\/10.1145\/800125.804029. Association for Computing Machinery, New York, pp 1\u20139","DOI":"10.1145\/800125.804029"},{"issue":"6","key":"357_CR26","doi-asserted-by":"publisher","first-page":"2823","DOI":"10.1109\/TAC.2016.2620429","volume":"62","author":"Y Tong","year":"2017","unstructured":"Tong Y, Li Z, Seatzu C, Giua A (2017) Verification of State-Based Opacity Using Petri Nets. IEEE Trans Autom Control 62(6):2823\u20132837. https:\/\/doi.org\/10.1109\/TAC.2016.2620429. IEEE Transactions on Automatic Control","journal-title":"IEEE Trans Autom Control"},{"issue":"6","key":"357_CR27","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1109\/MCS.2007.906923","volume":"27","author":"JC Willems","year":"2007","unstructured":"Willems J C (2007) The Behavioral Approach to Open and Interconnected Systems. IEEE Control Syst Mag 27(6):46\u201399. https:\/\/doi.org\/10.1109\/MCS.2007.906923. IEEE Control Systems Magazine","journal-title":"IEEE Control Syst Mag"},{"key":"357_CR28","doi-asserted-by":"crossref","unstructured":"Wintenberg A, Blischke M, Lafortune S, Ozay N (2021) A General Language-Based Framework for Specifying and Verifying Notions of Opacity. arXiv:2103.10501","DOI":"10.1007\/s10626-021-00357-x"},{"issue":"3","key":"357_CR29","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/s10626-012-0145-z","volume":"23","author":"Y-C Wu","year":"2013","unstructured":"Wu Y-C, Lafortune S (2013) Comparative analysis of related notions of opacity in centralized and coordinated architectures. Discret Event Dyn Syst 23 (3):307\u2013339. https:\/\/doi.org\/10.1007\/s10626-012-0145-z","journal-title":"Discret Event Dyn Syst"},{"issue":"5","key":"357_CR30","doi-asserted-by":"publisher","first-page":"1336","DOI":"10.1016\/j.automatica.2014.02.038","volume":"50","author":"Y-C Wu","year":"2014","unstructured":"Wu Y-C, Lafortune S (2014) Synthesis of insertion functions for enforcement of opacity security properties. Automatica 50(5):1336\u20131348. https:\/\/doi.org\/10.1016\/j.automatica.2014.02.038, https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0005109814000764","journal-title":"Automatica"},{"issue":"1","key":"357_CR31","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/s10817-017-9420-x","volume":"60","author":"Y-C Wu","year":"2018","unstructured":"Wu Y-C, Raman V, Rawlings B C, Lafortune S, Seshia S A (2018) Synthesis of Obfuscation Policies to Ensure Privacy and Utility. J Autom Reason 60(1):107\u2013131. https:\/\/doi.org\/10.1007\/s10817-017-9420-x","journal-title":"J Autom Reason"},{"issue":"2","key":"357_CR32","doi-asserted-by":"publisher","first-page":"33","DOI":"10.3182\/20140514-3-FR-4046.00008","volume":"47","author":"Y-C Wu","year":"2014","unstructured":"Wu Y-C, Sankararaman K A, Lafortune S (2014) Ensuring Privacy in Location-Based Services: An Approach Based on Opacity Enforcement. IFAC Proc Vol 47 (2):33\u201338. https:\/\/doi.org\/10.3182\/20140514-3-FR-4046.00008, https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1474667015373778","journal-title":"IFAC Proc Vol"},{"key":"357_CR33","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 (2017) A new approach for the verification of infinite-step and K-step opacity using two-way observers. Automatica 80:162\u2013171. https:\/\/doi.org\/10.1016\/j.automatica.2017.02.037, http:\/\/www.sciencedirect.com\/science\/article\/pii\/S0005109817301115","journal-title":"Automatica"},{"key":"357_CR34","doi-asserted-by":"crossref","unstructured":"Yin X, Li Z, Wang W, Li S (2017) Infinite-step opacity of stochastic discrete-event systems. In: 2017 11th Asian Control Conference (ASCC), pp 102\u2013107","DOI":"10.1109\/ASCC.2017.8287150"},{"key":"357_CR35","doi-asserted-by":"publisher","unstructured":"Yin X, Zamani M, Liu S (2020) On Approximate Opacity of Cyber-Physical Systems. IEEE Trans Autom Control:1\u20131. https:\/\/doi.org\/10.1109\/TAC.2020.2998733, IEEE Transactions on Automatic Control","DOI":"10.1109\/TAC.2020.2998733"}],"container-title":["Discrete Event Dynamic Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10626-021-00357-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10626-021-00357-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10626-021-00357-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,5,5]],"date-time":"2022-05-05T08:43:51Z","timestamp":1651740231000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10626-021-00357-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,2,2]]},"references-count":35,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2022,6]]}},"alternative-id":["357"],"URL":"https:\/\/doi.org\/10.1007\/s10626-021-00357-x","relation":{},"ISSN":["0924-6703","1573-7594"],"issn-type":[{"value":"0924-6703","type":"print"},{"value":"1573-7594","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,2,2]]},"assertion":[{"value":"14 February 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"4 December 2021","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"2 February 2022","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}