{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,23]],"date-time":"2025-09-23T00:10:14Z","timestamp":1758586214415,"version":"3.44.0"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032046994","type":"print"},{"value":"9783032047007","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,9,11]],"date-time":"2025-09-11T00:00:00Z","timestamp":1757548800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,9,11]],"date-time":"2025-09-11T00:00:00Z","timestamp":1757548800000},"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-3-032-04700-7_17","type":"book-chapter","created":{"date-parts":[[2025,9,21]],"date-time":"2025-09-21T23:45:47Z","timestamp":1758498347000},"page":"221-237","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["On Complementation of\u00a0Nondeterministic Finite Automata Without Full Determinization"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6957-1651","authenticated-orcid":false,"given":"Luk\u00e1\u0161","family":"Hol\u00edk","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3038-5875","authenticated-orcid":false,"given":"Ond\u0159ej","family":"Leng\u00e1l","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0007-1871-9047","authenticated-orcid":false,"given":"Juraj","family":"Major","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0004-4639-1673","authenticated-orcid":false,"given":"Ad\u00e9la","family":"\u0160t\u011bpkov\u00e1","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5873-403X","authenticated-orcid":false,"given":"Jan","family":"Strej\u010dek","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,9,11]]},"reference":[{"key":"17_CR1","doi-asserted-by":"crossref","unstructured":"Allred, J.D., Ultes-Nitsche, U.: A simple and optimal complementation algorithm for B\u00fcchi automata. In: LICS 2018, pp. 46\u201355. ACM (2018)","DOI":"10.1145\/3209108.3209138"},{"key":"17_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/10722167_11","volume-title":"Computer Aided Verification","author":"A Ayari","year":"2000","unstructured":"Ayari, A., Basin, D.: Bounded model construction for monadic second-order logics. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 99\u2013112. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/10722167_11"},{"issue":"2","key":"17_CR3","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1016\/0304-3975(93)90160-U","volume":"119","author":"J Birget","year":"1993","unstructured":"Birget, J.: Partial orders on words, minimal elements of regular languages and state complexity. Theor. Comput. Sci. 119(2), 267\u2013291 (1993)","journal-title":"Theor. Comput. Sci."},{"key":"17_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-030-53291-8_2","volume-title":"Computer Aided Verification","author":"F Blahoudek","year":"2020","unstructured":"Blahoudek, F., Duret-Lutz, A., Strej\u010dek, J.: Seminator 2 can complement generalized B\u00fcchi automata via improved semi-determinization. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 15\u201327. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_2"},{"issue":"2","key":"17_CR5","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/s10009-011-0205-y","volume":"14","author":"A Bouajjani","year":"2012","unstructured":"Bouajjani, A., Habermehl, P., Rogalewicz, A., Vojnar, T.: Abstract regular (tree) model checking. Int. J. Softw. Tools Technol. Transf. 14(2), 167\u2013191 (2012)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"17_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1007\/10722167_31","volume-title":"Computer Aided Verification","author":"A Bouajjani","year":"2000","unstructured":"Bouajjani, A., Jonsson, B., Nilsson, M., Touili, T.: Regular model checking. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 403\u2013418. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/10722167_31"},{"key":"17_CR7","unstructured":"B\u00fcchi, J.R.: On a decision method in restricted second-order arithmetic. In: International Congress on Logic, Methodology, and Philosophy of Science, pp. 1\u201311. Stanford University Press (1962)"},{"issue":"2","key":"17_CR8","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1145\/635499.635502","volume":"4","author":"D Bustan","year":"2003","unstructured":"Bustan, D., Grumberg, O.: Simulation-based minimization. ACM Trans. Comput. Log. 4(2), 181\u2013206 (2003)","journal-title":"ACM Trans. Comput. Log."},{"key":"17_CR9","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/978-3-031-57249-4_7","volume-title":"TACAS 2024","author":"D Chocholat\u00fd","year":"2024","unstructured":"Chocholat\u00fd, D., et al.: Mata: a fast and simple finite automata library. In: Finkbeiner, B., Kov\u00e1cs, L. (eds.) TACAS 2024. LNCS, vol. 14571, pp. 130\u2013151. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-57249-4_7"},{"key":"17_CR10","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-031-90653-4_2","volume-title":"TACAS 2025","author":"D Chocholat\u00fd","year":"2025","unstructured":"Chocholat\u00fd, D., Havlena, V., Hol\u00edk, L., Hrani\u010dka, J., Leng\u00e1l, O., S\u00ed\u010d, J.: Z3-noodler 1.3: shepherding decision procedures for strings with model generation. In: Gurfinkel, A., Heule, M. (eds.) TACAS 2025. LNCS, vol. 15697, pp. 23\u201344. Springer, Cham (2025). https:\/\/doi.org\/10.1007\/978-3-031-90653-4_2"},{"key":"17_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"516","DOI":"10.1007\/BFb0028773","volume-title":"Computer Aided Verification","author":"J Elgaard","year":"1998","unstructured":"Elgaard, J., Klarlund, N., M\u00f8ller, A.: MONA 1.x: new techniques for WS1S and WS2S. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 516\u2013520. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0028773"},{"key":"17_CR12","unstructured":"Evans, C.: CALEB531\/automata: a Python library for simulating finite automata, pushdown automata, and Turing machines (2025)"},{"key":"17_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"407","DOI":"10.1007\/978-3-662-54577-5_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Fiedor","year":"2017","unstructured":"Fiedor, T., Hol\u00edk, L., Jank\u016f, P., Leng\u00e1l, O., Vojnar, T.: Lazy automata techniques for WS1S. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 407\u2013425. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54577-5_24"},{"issue":"3","key":"17_CR14","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1007\/s00236-018-0331-z","volume":"56","author":"T Fiedor","year":"2019","unstructured":"Fiedor, T., Hol\u00edk, L., Leng\u00e1l, O., Vojnar, T.: Nested antichains for WS1S. Acta Informatica 56(3), 205\u2013228 (2019). https:\/\/doi.org\/10.1007\/s00236-018-0331-z","journal-title":"Acta Informatica"},{"key":"17_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/978-3-540-70844-5_17","volume-title":"Implementation and Applications of Automata","author":"R van Glabbeek","year":"2008","unstructured":"van Glabbeek, R., Ploeger, B.: Five determinisation algorithms. In: Ibarra, O.H., Ravikumar, B. (eds.) CIAA 2008. LNCS, vol. 5148, pp. 161\u2013170. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-70844-5_17"},{"key":"17_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/3-540-63174-7_5","volume-title":"Automata Implementation","author":"J Glenn","year":"1997","unstructured":"Glenn, J., Gasarch, W.: Implementing WS1S via finite automata. In: Raymond, D., Wood, D., Yu, S. (eds.) WIA 1996. LNCS, vol. 1260, pp. 50\u201363. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/3-540-63174-7_5"},{"key":"17_CR17","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1007\/978-3-031-65627-9_3","volume-title":"CAV 2024","author":"P Habermehl","year":"2024","unstructured":"Habermehl, P., Havlena, V., He\u010dko, M., Hol\u00edk, L., Leng\u00e1l, O.: Algebraic reasoning meets automata in solving linear integer arithmetic. In: Gurfinkel, A., Ganesh, V. (eds.) CAV 2024. LNCS, vol. 14681, pp. 42\u201367. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-65627-9_3"},{"key":"17_CR18","doi-asserted-by":"crossref","unstructured":"Hagberg, A.A., Schult, D.A., Swart, P.J.: Exploring network structure, dynamics, and function using networkx. In: SciPy 2008, pp. 11 \u2013 15. Pasadena, CA, USA (2008)","DOI":"10.25080\/TCWV9851"},{"key":"17_CR19","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/978-3-031-90897-2_5","volume-title":"FoSSaCS 2025","author":"V Havlena","year":"2025","unstructured":"Havlena, V., Leng\u00e1l, O., \u0160mahl\u00edkov\u00e1, B.: Complementation of Emerson-Lei automata. In: Abdulla, P.A., Kesner, D. (eds.) FoSSaCS 2025. LNCS, vol. 15691, pp. 88\u2013110. Springer, Cham (2025). https:\/\/doi.org\/10.1007\/978-3-031-90897-2_5"},{"key":"17_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/3-540-44977-9_14","volume-title":"Implementation and Application of Automata","author":"M Holzer","year":"2003","unstructured":"Holzer, M., Kutrib, M.: State complexity of basic operations on nondeterministic finite automata. In: Champarnaud, J.-M., Maurel, D. (eds.) CIAA 2002. LNCS, vol. 2608, pp. 148\u2013157. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-44977-9_14"},{"key":"17_CR21","unstructured":"Hol\u00edk, L., Leng\u00e1l, O., Major, J., \u0160t\u011bpkov\u00e1, A., Strej\u010dek, J.: On complementation of nondeterministic finite automata without full determinization (technical report). CoRR abs\/2507.03439 (2025). https:\/\/arxiv.org\/abs\/2507.03439"},{"key":"17_CR22","doi-asserted-by":"crossref","unstructured":"Hopcroft, J.: An $$n \\log n$$ algorithm for minimizing states in a finite automaton. In: Kohavi, Z., Paz, A. (eds.) Theory of Machines and Computations, pp. 189\u2013196. Academic Press (1971)","DOI":"10.1016\/B978-0-12-417750-5.50022-1"},{"issue":"2","key":"17_CR23","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1016\/j.tcs.2004.04.011","volume":"330","author":"G Jir\u00e1skov\u00e1","year":"2005","unstructured":"Jir\u00e1skov\u00e1, G.: State complexity of some operations on binary regular languages. Theor. Comput. Sci. 330(2), 287\u2013298 (2005)","journal-title":"Theor. Comput. Sci."},{"key":"17_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"448","DOI":"10.1007\/3-540-63166-6_45","volume-title":"Computer Aided Verification","author":"P Kelb","year":"1997","unstructured":"Kelb, P., Margaria, T., Mendier, M., Gsottberger, C.: Mosel: a sound and efficient tool for M2L(Str). In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 448\u2013451. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/3-540-63166-6_45"},{"issue":"1\u20132","key":"17_CR25","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1016\/S0304-3975(00)00103-1","volume":"256","author":"Y Kesten","year":"2001","unstructured":"Kesten, Y., Maler, O., Marcus, M., Pnueli, A., Shahar, E.: Symbolic model checking with rich assertional languages. Theor. Comput. Sci. 256(1\u20132), 93\u2013112 (2001)","journal-title":"Theor. Comput. Sci."},{"key":"17_CR26","doi-asserted-by":"crossref","unstructured":"Mayr, R., Clemente, L.: Advanced automata minimization. In: POPL 2013. ACM (2013)","DOI":"10.1145\/2429069.2429079"},{"key":"17_CR27","series-title":"LNM","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1007\/BFb0064872","volume-title":"Logic Colloquium","author":"AR Meyer","year":"1975","unstructured":"Meyer, A.R.: Weak monadic second order theory of succesor is not elementary-recursive. In: Parikh, R. (ed.) Logic Colloquium. LNM, vol. 453, pp. 132\u2013154. Springer, Heidelberg (1975). https:\/\/doi.org\/10.1007\/BFb0064872"},{"key":"17_CR28","doi-asserted-by":"crossref","unstructured":"Rabin, M.O., Scott, D.S.: Finite automata and their decision problems. IBM J. Res. Dev. 3(2) (1959)","DOI":"10.1147\/rd.32.0114"},{"key":"17_CR29","doi-asserted-by":"crossref","unstructured":"Sakoda, W.J., Sipser, M.: Nondeterminism and the size of two way finite automata. In: STOC 1978, pp. 275\u2013286. ACM (1978)","DOI":"10.1145\/800133.804357"},{"key":"17_CR30","unstructured":"Valmari, A., Lehtinen, P.: Efficient minimization of DFAs with partial transition functions. In: STACS 2008. LIPIcs, vol.\u00a01, pp. 645\u2013656. Dagstuhl (2008)"},{"key":"17_CR31","doi-asserted-by":"crossref","unstructured":"Varatalu, I.E., Veanes, M., Ernits, J.P.: RE#: high performance derivative-based regex matching with intersection, complement, and restricted lookarounds. PACMPL 9(POPL), 1\u201332 (2025)","DOI":"10.1145\/3704837"},{"key":"17_CR32","unstructured":"VeriFIT: nfa-bench Extensive benchmark for reasoning about regular properties (2025). https:\/\/github.com\/VeriFIT\/nfa-bench"},{"key":"17_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/3-540-60360-3_30","volume-title":"Static Analysis","author":"P Wolper","year":"1995","unstructured":"Wolper, P., Boigelot, B.: An automata-theoretic approach to Presburger arithmetic constraints. In: Mycroft, A. (ed.) SAS 1995. LNCS, vol. 983, pp. 21\u201332. Springer, Heidelberg (1995). https:\/\/doi.org\/10.1007\/3-540-60360-3_30"},{"key":"17_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/11817963_5","volume-title":"Computer Aided Verification","author":"M De Wulf","year":"2006","unstructured":"De Wulf, M., Doyen, L., Henzinger, T.A., Raskin, J.-F.: Antichains: a new algorithm for checking universality of finite automata. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 17\u201330. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11817963_5"}],"container-title":["Lecture Notes in Computer Science","Fundamentals of Computation Theory"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-04700-7_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,21]],"date-time":"2025-09-21T23:45:50Z","timestamp":1758498350000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-04700-7_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,11]]},"ISBN":["9783032046994","9783032047007"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-04700-7_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,9,11]]},"assertion":[{"value":"11 September 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FCT","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Fundamentals of Computation Theory","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Wroc\u0142aw","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Poland","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":"15 September 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 September 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fct2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/fct.ii.uni.wroc.pl","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}