{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T13:02:19Z","timestamp":1725886939029},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319578606"},{"type":"electronic","value":"9783319578613"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-57861-3_13","type":"book-chapter","created":{"date-parts":[[2017,5,4]],"date-time":"2017-05-04T02:10:40Z","timestamp":1493863840000},"page":"200-220","source":"Crossref","is-referenced-by-count":6,"title":["The Complexity of Diagnosability and Opacity Verification for Petri Nets"],"prefix":"10.1007","author":[{"given":"B\u00e9atrice","family":"B\u00e9rard","sequence":"first","affiliation":[]},{"given":"Stefan","family":"Haar","sequence":"additional","affiliation":[]},{"given":"Sylvain","family":"Schmitz","sequence":"additional","affiliation":[]},{"given":"Stefan","family":"Schwoon","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,5,5]]},"reference":[{"issue":"4","key":"13_CR1","doi-asserted-by":"publisher","first-page":"425","DOI":"10.1007\/s10626-007-0020-5","volume":"17","author":"E Badouel","year":"2007","unstructured":"Badouel, E., Bednarczyk, M.A., Borzyszkowski, A.M., Caillaud, B., Darondeau, P.: Concurrent secrets. Discrete Event Dyn. Syst. 17(4), 425\u2013446 (2007)","journal-title":"Discrete Event Dyn. Syst."},{"issue":"6","key":"13_CR2","doi-asserted-by":"publisher","first-page":"421","DOI":"10.1007\/s10207-008-0058-x","volume":"7","author":"J Bryans","year":"2008","unstructured":"Bryans, J., Koutny, M., Mazar\u00e9, L., Ryan, P.Y.A.: Opacity generalised to transition systems. Int. J. Inf. Secur. 7(6), 421\u2013435 (2008)","journal-title":"Int. J. Inf. Secur."},{"issue":"12","key":"13_CR3","doi-asserted-by":"publisher","first-page":"3104","DOI":"10.1109\/TAC.2012.2200372","volume":"57","author":"MP Cabasino","year":"2012","unstructured":"Cabasino, M.P., Giua, A., Lafortune, S., Seatzu, C.: A new approach for diagnosability analysis of Petri nets using verifier nets. IEEE Trans. Autom. Control 57(12), 3104\u20133117 (2012)","journal-title":"IEEE Trans. Autom. Control"},{"key":"13_CR4","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). doi: 10.1007\/978-3-642-04761-9_26"},{"key":"13_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"374","DOI":"10.1007\/3-540-65306-6_20","volume-title":"Lectures on Petri Nets I: Basic Models","author":"J Esparza","year":"1998","unstructured":"Esparza, J.: Decidability and complexity of Petri net problems \u2014 an introduction. In: Reisig, W., Rozenberg, G. (eds.) ACPN 1996. LNCS, vol. 1491, pp. 374\u2013428. Springer, Heidelberg (1998). doi: 10.1007\/3-540-65306-6_20"},{"key":"13_CR6","doi-asserted-by":"publisher","unstructured":"Even, S.: On information lossless automata of finite order. IEEE Trans. Elec. Comput. EC-14(4), 561\u2013569 (1965)","DOI":"10.1109\/PGEC.1965.263996"},{"key":"13_CR7","doi-asserted-by":"crossref","unstructured":"Germanos, V., Haar, S., Khomenko, V., Schwoon, S.: Diagnosability under weak fairness. ACM Trans. Embed. Comput. Syst. 14(4:69), 132\u2013141 (2015)","DOI":"10.1145\/2832910"},{"key":"13_CR8","doi-asserted-by":"publisher","unstructured":"Haar, S.: Qualitative diagnosability of labeled Petri nets revisited. In: Proceedings of CDC 2009 and CCC 2009, pp. 1248\u20131253. IEEE (2009)","DOI":"10.1109\/CDC.2009.5400917"},{"issue":"10","key":"13_CR9","doi-asserted-by":"publisher","first-page":"2310","DOI":"10.1109\/TAC.2010.2063490","volume":"55","author":"S Haar","year":"2010","unstructured":"Haar, S.: Types of asynchronous diagnosability and the reveals-relation in occurrence nets. IEEE Trans. Autom. Control 55(10), 2310\u20132320 (2010)","journal-title":"IEEE Trans. Autom. Control"},{"issue":"4","key":"13_CR10","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1007\/s10626-011-0121-z","volume":"22","author":"S Haar","year":"2012","unstructured":"Haar, S.: What topology tells us about diagnosability in partial order semantics. Discrete Event Dyn. Syst. 22(4), 383\u2013402 (2012)","journal-title":"Discrete Event Dyn. Syst."},{"key":"13_CR11","doi-asserted-by":"publisher","unstructured":"Haar, S., Rodr\u00edguez, C., Schwoon, S.: Reveal your faults: it\u2019s only fair! In: Proceedings of ACSD 2013, pp. 120\u2013129. IEEE (2013)","DOI":"10.1109\/ACSD.2013.15"},{"key":"13_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/3-540-63139-9_32","volume-title":"Application and Theory of Petri Nets 1997","author":"P Habermehl","year":"1997","unstructured":"Habermehl, P.: On the complexity of the linear-time $$\\mu $$ \u03bc -calculus for Petri Nets. In: Az\u00e9ma, P., Balbo, G. (eds.) ICATPN 1997. LNCS, vol. 1248, pp. 102\u2013116. Springer, Heidelberg (1997). doi: 10.1007\/3-540-63139-9_32"},{"issue":"2","key":"13_CR13","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1016\/0304-3975(91)90228-T","volume":"82","author":"RR Howell","year":"1991","unstructured":"Howell, R.R., Rosier, L.E., Yen, H.C.: A taxonomy of fairness and temporal logic problems for Petri nets. Theor. Comput. Sci. 82(2), 341\u2013372 (1991)","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"13_CR14","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1016\/0304-3975(90)90006-4","volume":"74","author":"P Jan\u010dar","year":"1990","unstructured":"Jan\u010dar, P.: Decidability of a temporal logic problem for Petri nets. Theor. Comput. Sci. 74(1), 71\u201393 (1990)","journal-title":"Theor. Comput. Sci."},{"issue":"1\u20132","key":"13_CR15","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1016\/S0304-3975(00)00100-6","volume":"256","author":"P Jan\u010dar","year":"2001","unstructured":"Jan\u010dar, P.: Nonprimitive recursive complexity and undecidability for Petri net equivalences. Theor. Comput. Sci. 256(1\u20132), 23\u201330 (2001)","journal-title":"Theor. Comput. Sci."},{"issue":"8","key":"13_CR16","doi-asserted-by":"publisher","first-page":"1318","DOI":"10.1109\/9.940942","volume":"46","author":"S Jiang","year":"2001","unstructured":"Jiang, S., Huang, Z., Chandra, V., Kumar, R.: A polynomial algorithm for testing diagnosability of discrete event systems. IEEE Trans. Autom. Control 46(8), 1318\u20131321 (2001)","journal-title":"IEEE Trans. Autom. Control"},{"issue":"3","key":"13_CR17","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1016\/0304-3975(77)90014-7","volume":"4","author":"ND Jones","year":"1977","unstructured":"Jones, N.D., Landweber, L.H., Lien, Y.E.: Complexity of some problems in Petri nets. Theor. Comput. Sci. 4(3), 277\u2013299 (1977)","journal-title":"Theor. Comput. Sci."},{"key":"13_CR18","doi-asserted-by":"publisher","unstructured":"Leroux, J., Schmitz, S.: Demystifying reachability in vector addition systems. In: Proceedings of LICS 2015, pp. 56\u201367. IEEE (2015)","DOI":"10.1109\/LICS.2015.16"},{"issue":"3","key":"13_CR19","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)","journal-title":"Automatica"},{"key":"13_CR20","unstructured":"Lipton, R.: The reachability problem requires exponential space. Technical report 62. Yale University (1976)"},{"key":"13_CR21","doi-asserted-by":"publisher","unstructured":"Madalinski, A., Khomenko, V.: Diagnosability verification with parallel LTL-X model checking based on Petri net unfoldings. In: Proceedings of SysTol 2010, pp. 398\u2013403. IEEE (2010)","DOI":"10.1109\/SYSTOL.2010.5676089"},{"issue":"2","key":"13_CR22","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1006\/inco.1994.1098","volume":"115","author":"AJ Mayer","year":"1994","unstructured":"Mayer, A.J., Stockmeyer, L.J.: The complexity of word problems\u2013this time with interleaving. Inf. Comput. 115(2), 293\u2013311 (1994)","journal-title":"Inf. Comput."},{"issue":"9","key":"13_CR23","doi-asserted-by":"publisher","first-page":"1555","DOI":"10.1109\/9.412626","volume":"40","author":"M Sampath","year":"1995","unstructured":"Sampath, M., Sengupta, R., Lafortune, S., Sinnamohideen, K., Teneketzis, D.: Diagnosability of discrete-event systems. IEEE Trans. Autom. Control 40(9), 1555\u20131575 (1995)","journal-title":"IEEE Trans. Autom. Control"},{"issue":"1","key":"13_CR24","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1145\/2893582.2893585","volume":"3","author":"S Schmitz","year":"2016","unstructured":"Schmitz, S.: Automata column: the complexity of reachability in vector addition systems. ACM SIGLOG News 3(1), 3\u201321 (2016)","journal-title":"ACM SIGLOG News"},{"key":"13_CR25","doi-asserted-by":"publisher","unstructured":"Tong, Y., Li, Z., Seatzu, C., Giua, A.: Verification of initial-state opacity in Petri nets. In: Proceedings of CDC 2015, pp. 344\u2013349. IEEE (2015)","DOI":"10.1109\/CDC.2015.7402224"},{"issue":"1","key":"13_CR26","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1016\/0020-0190(95)00049-I","volume":"55","author":"W Vogler","year":"1995","unstructured":"Vogler, W.: Fairness and partial order semantics. Inf. Process. Lett. 55(1), 33\u201339 (1995)","journal-title":"Inf. Process. Lett."},{"issue":"9","key":"13_CR27","doi-asserted-by":"publisher","first-page":"1491","DOI":"10.1109\/TAC.2002.802763","volume":"47","author":"TS Yoo","year":"2002","unstructured":"Yoo, T.S., Lafortune, S.: Polynomial-time verification of diagnosability of partially observed discrete event systems. IEEE Trans. Autom. Control 47(9), 1491\u20131495 (2002)","journal-title":"IEEE Trans. Autom. Control"}],"container-title":["Lecture Notes in Computer Science","Application and Theory of Petri Nets and Concurrency"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-57861-3_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,10,6]],"date-time":"2020-10-06T22:08:55Z","timestamp":1602022135000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-57861-3_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319578606","9783319578613"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-57861-3_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}