{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,7]],"date-time":"2025-06-07T17:40:09Z","timestamp":1749318009073,"version":"3.41.0"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031937057","type":"print"},{"value":"9783031937064","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"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":[[2025]]},"DOI":"10.1007\/978-3-031-93706-4_24","type":"book-chapter","created":{"date-parts":[[2025,6,7]],"date-time":"2025-06-07T17:22:45Z","timestamp":1749316965000},"page":"421-440","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Automata Size Reduction by\u00a0Procedure Finding"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0004-0091-0546","authenticated-orcid":false,"given":"Michal","family":"\u0160ed\u00fd","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6957-1651","authenticated-orcid":false,"given":"Luk\u00e1\u0161","family":"Hol\u00edk","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,6,8]]},"reference":[{"key":"24_CR1","doi-asserted-by":"publisher","unstructured":"Aziz, A., Singhal, V., Brayton, R., Swamy, G.: Minimizing interacting finite state machines: a compositional approach to language containment. In: Proceedings 1994 IEEE International Conference on Computer Design: VLSI in Computers and Processors, pp. 255\u2013261 (1994). https:\/\/doi.org\/10.1109\/ICCD.1994.331900","DOI":"10.1109\/ICCD.1994.331900"},{"key":"24_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/978-3-662-48899-7_6","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"S Baarir","year":"2015","unstructured":"Baarir, S., Duret-Lutz, A.: SAT-based minimization of deterministic $$\\omega $$-automata. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) LPAR 2015. LNCS, vol. 9450, pp. 79\u201387. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-48899-7_6"},{"issue":"2","key":"24_CR3","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). https:\/\/doi.org\/10.1007\/s10009-011-0205-y","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"24_CR4","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/10721959_20","volume-title":"Automated Deduction - CADE-17","author":"D Bustan","year":"2000","unstructured":"Bustan, D., Grumberg, O.: Simulation based minimization. In: McAllester, D. (ed.) CADE 2000. LNCS (LNAI), vol. 1831, pp. 255\u2013270. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/10721959_20"},{"key":"24_CR5","doi-asserted-by":"crossref","unstructured":"\u010ce\u0161ka, M., et al.: Deep packet inspection in FPGAs via approximate nondeterministic automata. CoRR abs\/1904.10786 (2019)","DOI":"10.1109\/FCCM.2019.00025"},{"key":"24_CR6","unstructured":"\u010ce\u0161ka, M., Havlena, V., Hol\u00edk, L., Leng\u00e1l, O., Vojnar, T.: AppReAL - approximate reduction of automata and languages. https:\/\/github.com\/ondrik-network-hw\/appreal"},{"key":"24_CR7","doi-asserted-by":"publisher","unstructured":"Chocholat\u00fd, D., Fiedor, T., Havlena, V., Holik, L., Hru\u0161ka, M., Leng\u00e1l, O., S\u00ed?, J.: 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","DOI":"10.1007\/978-3-031-57249-4_7"},{"key":"24_CR8","unstructured":"Clemente, L., Mayr, R.: Advanced automata minimization. Computing Research Repository (CoRR) abs\/1210.6624 (2012)"},{"key":"24_CR9","unstructured":"Clemente, L., Mayr, R.: Efficient reduction of nondeterministic automata with application to language inclusion testing. CoRR abs\/1711.09946 (2017)"},{"key":"24_CR10","unstructured":"Clemente, L., Mayr, R., et\u00a0al.: RABIT\/reduce. https:\/\/languageinclusion.org"},{"key":"24_CR11","unstructured":"D\u2019Antoni, L., Kincaid, Z., Wang, F.: A symbolic decision procedure for symbolic alternating finite automata. CoRR abs\/1610.01722 (2016)"},{"key":"24_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/978-3-642-36742-7_20","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Gange","year":"2013","unstructured":"Gange, G., Navas, J.A., Stuckey, P.J., S\u00f8ndergaard, H., Schachte, P.: Unbounded model-checking with interpolation for regular language constraints. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 277\u2013291. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_20"},{"key":"24_CR13","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/978-3-642-14684-8_9","volume-title":"Finite-State Methods and Natural Language Processing","author":"J Geldenhuys","year":"2010","unstructured":"Geldenhuys, J., van der Merwe, B., van Zijl, L.: Reducing nondeterministic finite automata with SAT solvers. In: Yli-Jyr\u00e4, A., Kornai, A., Sakarovitch, J., Watson, B. (eds.) FSMNLP 2009. LNCS (LNAI), vol. 6062, pp. 81\u201392. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14684-8_9"},{"key":"24_CR14","unstructured":"Havlena, V., S\u00ed\u010d, J., Chen, Y.F., Chocholat\u00fd, D., Hol\u00edk, L., Leng\u00e1l, O.: Z3-Noodler. https:\/\/github.com\/VeriFIT\/z3-noodler"},{"key":"24_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/978-3-540-27812-2_11","volume-title":"Theory Is Forever","author":"L Ilie","year":"2004","unstructured":"Ilie, L., Navarro, G., Yu, S.: On NFA reductions. In: Karhum\u00e4ki, J., Maurer, H., P\u0103un, G., Rozenberg, G. (eds.) Theory Is Forever. LNCS, vol. 3113, pp. 112\u2013124. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-27812-2_11"},{"key":"24_CR16","doi-asserted-by":"publisher","first-page":"617","DOI":"10.1109\/T-C.1970.222994","volume":"100","author":"T Kameda","year":"1970","unstructured":"Kameda, T., Weiner, P.: On the state minimization of nondeterministic finite automata. IEEE Trans. Comput. 100, 617\u2013627 (1970). https:\/\/doi.org\/10.1109\/T-C.1970.222994","journal-title":"IEEE Trans. Comput."},{"key":"24_CR17","doi-asserted-by":"publisher","unstructured":"Ko\u0161ar, V., Ka\u0161til, J., Tobola, J., Korenek, J., Pu\u0161, V.: NetBench: framework for evaluation of packet processing algorithms. In: Architectures for Networking and Communications Systems, pp. 95\u201396. IEEE Computer Society, Los Alamitos (2011). https:\/\/doi.org\/10.1109\/ANCS.2011.25","DOI":"10.1109\/ANCS.2011.25"},{"key":"24_CR18","unstructured":"M\u00f8ller, A.: dk.brics.automaton \u2013 finite-state automata and regular expressions for Java (2021). http:\/\/www.brics.dk\/automaton\/"},{"key":"24_CR19","unstructured":"Moln\u00e1rov\u00e1, V.: Efficient reduction of finite automata. Brno University of Technology (2023). https:\/\/www.vut.cz\/en\/students\/final-thesis\/detail\/145522. Bachelor\u2019s thesis, Supervisor: Leng\u00e1l, O"},{"key":"24_CR20","unstructured":"RegexLib Team: Regular Expression Library. https:\/\/regexlib.com\/"},{"key":"24_CR21","doi-asserted-by":"publisher","unstructured":"Sistla, M.A., Chaudhuri, S., Reps, T.: CFLOBDDs: context-free-language ordered binary decision diagrams. ACM Trans. Program. Lang. Syst. 46(2) (2024). https:\/\/doi.org\/10.1145\/3651157","DOI":"10.1145\/3651157"},{"key":"24_CR22","doi-asserted-by":"publisher","unstructured":"Smith, R., Estan, C., Jha, S.: XFA: faster signature matching with extended automata. In: 2008 IEEE Symposium on Security and Privacy (SP 2008), pp. 187\u2013201 (2008). https:\/\/doi.org\/10.1109\/SP.2008.14","DOI":"10.1109\/SP.2008.14"},{"key":"24_CR23","unstructured":"Snort Team: Snort: Network Intrusion Detection & Prevention System. https:\/\/www.snort.org\/"},{"key":"24_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"880","DOI":"10.1007\/978-3-540-45234-8_85","volume-title":"Field Programmable Logic and Application","author":"I Sourdis","year":"2003","unstructured":"Sourdis, I., Pnevmatikatos, D.: Fast, large-scale string match for a 10Gbps FPGA-based network intrusion detection system. In: Y. K. Cheung, P., Constantinides, G.A. (eds.) FPL 2003. LNCS, vol. 2778, pp. 880\u2013889. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45234-8_85"},{"key":"24_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-030-89051-3_14","volume-title":"Programming Languages and Systems","author":"P Vargov\u010d\u00edk","year":"2021","unstructured":"Vargov\u010d\u00edk, P., Hol\u00edk, L.: Simplifying alternating automata for\u00a0emptiness testing. In: Oh, H. (ed.) APLAS 2021. LNCS, vol. 13008, pp. 243\u2013264. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-89051-3_14"},{"key":"24_CR26","unstructured":"\u0160ed\u00fd, M.: Reducing size of nondeterministic automata with SAT solvers. Brno University of Technology, Faculty of Information Technology (2021). https:\/\/www.fit.vut.cz\/ study\/thesis\/23436\/, Bachelor\u2019s thesis, Supervisor: Hol\u00edk, L"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-93706-4_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,7]],"date-time":"2025-06-07T17:22:48Z","timestamp":1749316968000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-93706-4_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031937057","9783031937064"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-93706-4_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"8 June 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"NFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"NASA Formal Methods Symposium","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hampton Roads, VA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","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":"11 June 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 June 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"nfm2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/shemesh.larc.nasa.gov\/nfm2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}