{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,13]],"date-time":"2026-04-13T04:58:17Z","timestamp":1776056297664,"version":"3.50.1"},"reference-count":36,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2023,10,1]],"date-time":"2023-10-01T00:00:00Z","timestamp":1696118400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,10,1]],"date-time":"2023-10-01T00:00:00Z","timestamp":1696118400000},"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":["J Syst Sci Complex"],"published-print":{"date-parts":[[2023,10]]},"DOI":"10.1007\/s11424-023-2114-z","type":"journal-article","created":{"date-parts":[[2023,10,19]],"date-time":"2023-10-19T08:02:16Z","timestamp":1697702536000},"page":"1830-1850","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Infinite- and K-Step Opacity Verification of Discrete-Event Systems Under Nondeterministic Observations"],"prefix":"10.1007","volume":"36","author":[{"given":"Qian","family":"Chu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jiahui","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xiaoguang","family":"Han","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhiwu","family":"Li","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zengqiang","family":"Chen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,10,19]]},"reference":[{"key":"2114_CR1","unstructured":"Mazar\u00e9 L, Using unification for opacity properties, Verimag Technical Report, 2004."},{"key":"2114_CR2","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/j.entcs.2004.10.010","volume":"121","author":"J W Bryans","year":"2005","unstructured":"Bryans J W, Koutny M, and Ryan P, Modelling opacity using Petri nets, Electronic Notes in Theoretical Computer Science, 2005, 121: 101\u2013115.","journal-title":"Electronic Notes in Theoretical Computer Science"},{"issue":"6","key":"2114_CR3","doi-asserted-by":"publisher","first-page":"421","DOI":"10.1007\/s10207-008-0058-x","volume":"7","author":"J W Bryans","year":"2008","unstructured":"Bryans J W, Koutny M, Mazar\u00e9 L, et al., Opacity generalised to transition systems, International Journal of Information Security, 2008, 7(6): 421\u2013435.","journal-title":"International Journal of Information Security"},{"key":"2114_CR4","doi-asserted-by":"crossref","unstructured":"Saboori A and Hadjicostis C N, Notions of security and opaicty in discrete event systems, Procceedings of 46th IEEE Conference on Decision and Control, 2007, 5056\u20135061.","DOI":"10.1109\/CDC.2007.4434515"},{"issue":"3","key":"2114_CR5","doi-asserted-by":"publisher","first-page":"549","DOI":"10.1109\/TASE.2011.2106775","volume":"8","author":"A Saboori","year":"2011","unstructured":"Saboori A and Hadjicostis C N, Verification of K-step opacity and analysis of its complexity, IEEE Transactions on Automation Science and Engineering, 2011, 8(3): 549\u2013559.","journal-title":"IEEE Transactions on Automation Science and Engineering"},{"issue":"5","key":"2114_CR6","doi-asserted-by":"publisher","first-page":"1265","DOI":"10.1109\/TAC.2011.2173774","volume":"57","author":"A Saboori","year":"2012","unstructured":"Saboori A, Verification of infinite-step opacity and complexity considerations, IEEE Transactions on Automatic Control, 2012, 57(5): 1265\u20131269.","journal-title":"IEEE Transactions on Automatic Control"},{"key":"2114_CR7","doi-asserted-by":"crossref","unstructured":"Saboori A and Hadjicostis C N, Verification of initial-state opacity in security applications of DES, Proceedings of the 9th International Workshop on Discrete Event Systems, 2008, 328\u2013333.","DOI":"10.1109\/WODES.2008.4605967"},{"key":"2114_CR8","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 and Hadjicostis C N, Verification of initial-state opacity in security appications of discrete event systems, Information Sciences, 2013, 246: 115\u2013132.","journal-title":"Information Sciences"},{"key":"2114_CR9","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 and Lafortune S, A new approach for the verification of infinite-step and K-step opacity using two-way observers, Automatica, 2017, 80: 162\u2013171.","journal-title":"Automatica"},{"key":"2114_CR10","doi-asserted-by":"crossref","first-page":"109273","DOI":"10.1016\/j.automatica.2020.109273","volume":"124","author":"H Lan","year":"2021","unstructured":"Lan H, Tong, Y, Guo J, et al., Comments \u201cA new approach for the verification of infinite-step and K-step opacity using two-way observers\u201d [Automatica, 2017, 80: 162\u2013171], Automatica, 2021, 124: 109273.","journal-title":"Automatica"},{"issue":"4","key":"2114_CR11","doi-asserted-by":"publisher","first-page":"531","DOI":"10.1007\/s10626-014-0196-4","volume":"25","author":"Y Falcone","year":"2015","unstructured":"Falcone Y and Marchand H, Enforcement and validation (at runtime) of various notions of opacity, Discrete Event Dynamic Systems, 2015, 25(4): 531\u2013570.","journal-title":"Discrete Event Dynamic Systems"},{"key":"2114_CR12","doi-asserted-by":"publisher","first-page":"108476","DOI":"10.1016\/j.automatica.2019.06.028","volume":"108","author":"Y Ji","year":"2019","unstructured":"Ji Y, Yin X, and Lafortune S, Enforcing opacity by insertion functions under multiple energy constraints, Automatica, 2019, 108: 108476.","journal-title":"Automatica"},{"issue":"10","key":"2114_CR13","doi-asserted-by":"publisher","first-page":"4369","DOI":"10.1109\/TAC.2019.2897553","volume":"64","author":"Y Ji","year":"2019","unstructured":"Ji Y, Yin X, and Lafortune S, Opacity enforcement using nondeterministic publicly-known edit functions, IEEE Transactions on Automatic Control, 2019, 64(10): 4369\u20134376.","journal-title":"IEEE Transactions on Automatic Control"},{"issue":"8","key":"2114_CR14","doi-asserted-by":"publisher","first-page":"3349","DOI":"10.1109\/TAC.2019.2946165","volume":"65","author":"S Mohajerani","year":"2020","unstructured":"Mohajerani S, Ji Y, and Lafortune S, Compositional and abstraction-based approach for synthesis of edit functions for opacity enforcement, IEEE Transations on Automatic Control, 2020, 65(8): 3349\u20133364.","journal-title":"IEEE Transations on Automatic Control"},{"issue":"4","key":"2114_CR15","doi-asserted-by":"publisher","first-page":"1429","DOI":"10.1109\/TAC.2019.2916940","volume":"65","author":"X Yin","year":"2020","unstructured":"Yin X and Li S, Synthesis of dynamic masks for infinite-step opacity, IEEE Transactions on Automatic Control, 2020, 65(4): 1429\u20131441.","journal-title":"IEEE Transactions on Automatic Control"},{"key":"2114_CR16","doi-asserted-by":"publisher","first-page":"110212","DOI":"10.1016\/j.automatica.2022.110212","volume":"140","author":"R Liu","year":"2022","unstructured":"Liu R and Lu J, Enforcement for infinite-step opacity and K-step opacity via insertion, Automatica, 2022, 140: 110212.","journal-title":"Automatica"},{"issue":"6","key":"2114_CR17","doi-asserted-by":"publisher","first-page":"2823","DOI":"10.1109\/TAC.2016.2620429","volume":"62","author":"Y Tong","year":"2016","unstructured":"Tong Y, Li Z, Seatzu C, et al., Verification of state-based opacity using Petri nets, IEEE Transations on Automatic Control, 2016, 62(6): 2823\u20132837.","journal-title":"IEEE Transations on Automatic Control"},{"key":"2114_CR18","doi-asserted-by":"publisher","first-page":"110221","DOI":"10.1016\/j.automatica.2022.110221","volume":"140","author":"Y Tong","year":"2022","unstructured":"Tong Y, Lan H, and Seatzu C, Verification of K-step and infinite-step opacity of bounded labeled Petri nets, Automatica, 2022, 140: 110221.","journal-title":"Automatica"},{"issue":"2","key":"2114_CR19","doi-asserted-by":"publisher","first-page":"884","DOI":"10.1109\/TCNS.2021.3050131","volume":"8","author":"S Yang","year":"2021","unstructured":"Yang S, Hou J, Yin X, et al., Opacity of networked supervisory control systems over insecure communication channels, IEEE Transactions on Control of Network Systems, 2021, 8(2): 884\u2013896.","journal-title":"IEEE Transactions on Control of Network Systems"},{"key":"2114_CR20","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1016\/j.ins.2020.07.017","volume":"543","author":"J Yang","year":"2021","unstructured":"Yang J, Deng W, Jiang C, et al., Opacity of networked discrete event systems, Information Sciences, 2021, 543: 328\u2013344.","journal-title":"Information Sciences"},{"issue":"3","key":"2114_CR21","doi-asserted-by":"publisher","first-page":"885","DOI":"10.1109\/TFUZZ.2020.3044359","volume":"30","author":"W Deng","year":"2020","unstructured":"Deng W, Qiu D, and Yang J, Fuzzy infinite-step opacity measure of discrete event systems and its applications, IEEE Transactions on Fuzzy Systems, 2020, 30(3): 885\u2013892.","journal-title":"IEEE Transactions on Fuzzy Systems"},{"issue":"9","key":"2114_CR22","doi-asserted-by":"publisher","first-page":"2612","DOI":"10.1109\/TFUZZ.2020.3005335","volume":"29","author":"W Deng","year":"2021","unstructured":"Deng W, Qiu D, and Yang J, Opacity measures of fuzzy discrete event systems, IEEE Transactions on Fuzzy Systems, 2021, 29(9): 2612\u20132622.","journal-title":"IEEE Transactions on Fuzzy Systems"},{"issue":"2","key":"2114_CR23","doi-asserted-by":"publisher","first-page":"294","DOI":"10.3182\/20140514-3-FR-4046.00092","volume":"47","author":"M Alves","year":"2014","unstructured":"Alves M, Basilio J, Cunha A, et al., Robust supervisory control against intermittent loss of observations, IFAC Proceedings Volumes, 2014, 47(2): 294\u2013299.","journal-title":"IFAC Proceedings Volumes"},{"issue":"2","key":"2114_CR24","doi-asserted-by":"publisher","first-page":"1276","DOI":"10.1137\/130914942","volume":"52","author":"F Lin","year":"2014","unstructured":"Lin F, Control of networked discrete event system: Dealing with communication delays and losses, SIAM Journal on Control and Optimization, 2014, 52(2): 1276\u20131298.","journal-title":"SIAM Journal on Control and Optimization"},{"key":"2114_CR25","doi-asserted-by":"crossref","unstructured":"Xu S and Kumar R, Discrete event control under nondeterministic partial observation, Proceedings of 2009 IEEE International Conference on Automation Science and Engineering, 2009, 127\u2013132.","DOI":"10.1109\/COASE.2009.5234123"},{"issue":"3","key":"2114_CR26","doi-asserted-by":"publisher","first-page":"799","DOI":"10.1109\/TAC.2015.2449051","volume":"61","author":"T Ushio","year":"2016","unstructured":"Ushio T and Takai S, Nonblocking supervisory control of discrete event systems modeled by Mealy automata with nondeterministic output functions, IEEE Transactions on Automatic Control, 2016, 61(3): 799\u2013804.","journal-title":"IEEE Transactions on Automatic Control"},{"issue":"3","key":"2114_CR27","doi-asserted-by":"publisher","first-page":"798","DOI":"10.1109\/TAC.2012.2185881","volume":"57","author":"S Takai","year":"2012","unstructured":"Takai S and Ushio T, Verification of codiagnosability for discrete event systems modeled by Mealy automata with nondeterministic output functions, IEEE Transactions on Automatic Control, 2012, 57(3): 798\u2013804.","journal-title":"IEEE Transactions on Automatic Control"},{"issue":"3","key":"2114_CR28","doi-asserted-by":"publisher","first-page":"1315","DOI":"10.1109\/TASE.2020.3001356","volume":"18","author":"L Zhou","year":"2021","unstructured":"Zhou L, Shu S, and Lin F, Detectability of discrete-event systems under nondeterministic observations, IEEE Transactions on Automation Sciencce Engineering, 2021, 18(3): 1315\u20131327.","journal-title":"IEEE Transactions on Automation Sciencce Engineering"},{"issue":"5","key":"2114_CR29","doi-asserted-by":"publisher","first-page":"2576","DOI":"10.1109\/TAC.2016.2601118","volume":"62","author":"X Yin","year":"2017","unstructured":"Yin X, Supervisor synthesis for Mealy automata with output functions: A model transformation approach, IEEE Transactions on Automatic Control, 2017, 62(5): 2576\u20132581.","journal-title":"IEEE Transactions on Automatic Control"},{"key":"2114_CR30","doi-asserted-by":"publisher","DOI":"10.1142\/8323","volume-title":"An Introduction to Semi-Tensor Product of Matrices and Its Applications","author":"D Cheng","year":"2012","unstructured":"Cheng D, An Introduction to Semi-Tensor Product of Matrices and Its Applications, World Scientific, Singapore, 2012."},{"key":"2114_CR31","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1016\/j.ins.2020.10.019","volume":"548","author":"X Han","year":"2021","unstructured":"Han X, Yang W, Chen X, et al., Detectability verification of probabilistic Boolean networks, Information Sciences, 2021, 548: 313\u2013327.","journal-title":"Information Sciences"},{"issue":"2","key":"2114_CR32","doi-asserted-by":"publisher","first-page":"436","DOI":"10.1007\/s11424-017-6145-1","volume":"31","author":"D Jiang","year":"2018","unstructured":"Jiang D and Zhang K, Observability of Boolean control networks with time-variant delays in states, Journal of Systems Science & Complexity, 2018, 31(2): 436\u2013445.","journal-title":"Journal of Systems Science & Complexity"},{"key":"2114_CR33","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1016\/j.sysconle.2018.10.014","volume":"123","author":"X Han","year":"2019","unstructured":"Han X, Chen Z, and Su R, Synthesis of minimally restrictive optimal stability-enforcing supervisors for nondeterministic discrete event systems, Systems & Control Letters, 2019, 123: 33\u201339.","journal-title":"Systems & Control Letters"},{"issue":"1","key":"2114_CR34","doi-asserted-by":"publisher","first-page":"662","DOI":"10.1109\/TASE.2022.3165382","volume":"20","author":"X Han","year":"2023","unstructured":"Han X, Wang J, Li Z, et al., Revisiting state estimation and weak detectability of discrete-event systems, IEEE Transactions on Automation Science and Engineering, 2023, 20(1): 662\u2013674.","journal-title":"IEEE Transactions on Automation Science and Engineering"},{"key":"2114_CR35","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72274-6","volume-title":"Introduction to Discrete Event Systems","author":"C G Cassandras","year":"2021","unstructured":"Cassandras C G and Lafortune S, Introduction to Discrete Event Systems, 3rd Ed., Springer, Switzerland, 2021.","edition":"3rd Ed."},{"key":"2114_CR36","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 and Lafortune S, Comparative analysis of related notions of opacity in centralized and coordinated architectures, Discrete Event Dynamic Systems, 2013, 23: 307\u2013339.","journal-title":"Discrete Event Dynamic Systems"}],"container-title":["Journal of Systems Science and Complexity"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11424-023-2114-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11424-023-2114-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11424-023-2114-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,10,19]],"date-time":"2023-10-19T08:43:17Z","timestamp":1697704997000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11424-023-2114-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,10]]},"references-count":36,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2023,10]]}},"alternative-id":["2114"],"URL":"https:\/\/doi.org\/10.1007\/s11424-023-2114-z","relation":{},"ISSN":["1009-6124","1559-7067"],"issn-type":[{"value":"1009-6124","type":"print"},{"value":"1559-7067","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,10]]},"assertion":[{"value":"2 March 2022","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"1 July 2022","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"19 October 2023","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"The authors declare no conflict of interest.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of Interest"}}]}}