{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:12:51Z","timestamp":1742911971721,"version":"3.40.3"},"publisher-location":"Cham","reference-count":82,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031384981"},{"type":"electronic","value":"9783031384998"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,9,2]],"date-time":"2023-09-02T00:00:00Z","timestamp":1693612800000},"content-version":"vor","delay-in-days":244,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Several new algorithms for deciding emptiness of Boolean combinations of regular languages and of languages of alternating automata have been proposed recently, especially in the context of analysing regular expressions and in string constraint solving. The new algorithms demonstrated a significant potential, but they have never been systematically compared, neither among each other nor with the state-of-the art implementations of existing (non)deterministic automata-based methods. In this paper, we provide such comparison as well as an overview of the existing algorithms and their implementations. We collect a diverse benchmark mostly originating in or related to practical problems from string constraint solving, analysing LTL properties, and regular model checking, and evaluate collected implementations on it. The results reveal the best tools and hint on what the best algorithms and implementation techniques are. Roughly, although some advanced algorithms are fast, such as antichain algorithms and reductions to IC3\/PDR, they are not as overwhelmingly dominant as sometimes presented and there is no clear winner. The simplest NFA-based technology may sometimes be a better choice, depending on the problem source and the implementation style. We believe that our findings are relevant for development of automata techniques as well as for related fields such as string constraint solving.<\/jats:p>","DOI":"10.1007\/978-3-031-38499-8_17","type":"book-chapter","created":{"date-parts":[[2023,9,1]],"date-time":"2023-09-01T23:03:25Z","timestamp":1693609405000},"page":"286-306","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Reasoning About Regular Properties: A Comparative Study"],"prefix":"10.1007","author":[{"given":"Tom\u00e1\u0161","family":"Fiedor","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luk\u00e1\u0161","family":"Hol\u00edk","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martin","family":"Hru\u0161ka","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Adam","family":"Rogalewicz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Juraj","family":"S\u00ed\u010d","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pavol","family":"Vargov\u010d\u00edk","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,9,2]]},"reference":[{"key":"17_CR1","unstructured":"The benchmark used in the paper. https:\/\/github.com\/VeriFIT\/automata-bench"},{"key":"17_CR2","unstructured":"Experiment replication package and additional material. https:\/\/www.fit.vutbr.cz\/research\/groups\/verifit\/tools\/afa-comparison\/"},{"key":"17_CR3","unstructured":"Jaltimpact. https:\/\/github.com\/cathiec\/JAltImpact"},{"key":"17_CR4","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., et al.: TRAU: SMT solver for string constraints. In: Proceedings of the FMCAD\u201918. IEEE (2018)","DOI":"10.23919\/FMCAD.2018.8602997"},{"key":"17_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/978-3-030-31784-3_16","volume-title":"Automated Technology for Verification and Analysis","author":"PA Abdulla","year":"2019","unstructured":"Abdulla, P.A., Atig, M.F., Diep, B.P., Hol\u00edk, L., Jank\u016f, P.: Chain-free string constraints. In: Chen, Y.-F., Cheng, C.-H., Esparza, J. (eds.) ATVA 2019. LNCS, vol. 11781, pp. 277\u2013293. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-31784-3_16"},{"key":"17_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/978-3-642-12002-2_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"PA Abdulla","year":"2010","unstructured":"Abdulla, P.A., Chen, Y.-F., Hol\u00edk, L., Mayr, R., Vojnar, T.: When simulation meets antichains. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 158\u2013174. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-12002-2_14"},{"key":"17_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/978-3-030-99524-9_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H Barbosa","year":"2022","unstructured":"Barbosa, H., et al.: cvc5: a versatile and industrial-strength SMT solver. In: TACAS 2022. LNCS, vol. 13243, pp. 415\u2013442. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24"},{"key":"17_CR8","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2016). https:\/\/www.smt-lib.org\/"},{"key":"17_CR9","unstructured":"Berzish, M.: Z3str4: a solver for theories over strings. Ph.D. thesis (2021). http:\/\/hdl.handle.net\/10012\/17102"},{"key":"17_CR10","doi-asserted-by":"publisher","unstructured":"Blahoudek, F., et al.: Word equations in synergy with regular constraints. In: Chechik, M., Katoen, J.P., Leucker, M. (eds.) Formal Methods. FM 2023. LNCS, vol. 14000, pp. 403\u2013423. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-27481-7_23","DOI":"10.1007\/978-3-031-27481-7_23"},{"key":"17_CR11","doi-asserted-by":"crossref","unstructured":"Bonchi, F., Pous, D.: Checking NFA equivalence with bisimulations up to congruence. In: Proceedings of the POPL\u201913. ACM (2013)","DOI":"10.1145\/2429069.2429124"},{"key":"17_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/978-3-540-70844-5_7","volume-title":"Implementation and Applications of Automata","author":"A Bouajjani","year":"2008","unstructured":"Bouajjani, A., Habermehl, P., Hol\u00edk, L., Touili, T., Vojnar, T.: Antichain-based universality and inclusion testing over nondeterministic finite tree automata. In: Ibarra, O.H., Ravikumar, B. (eds.) CIAA 2008. LNCS, vol. 5148, pp. 57\u201367. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-70844-5_7"},{"key":"17_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1007\/3-540-61064-2_27","volume-title":"Trees in Algebra and Programming \u2014 CAAP \u201996","author":"A Boudet","year":"1996","unstructured":"Boudet, A., Comon, H.: Diophantine equations, presburger arithmetic and finite automata. In: Kirchner, H. (ed.) CAAP 1996. LNCS, vol. 1059, pp. 30\u201343. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61064-2_27"},{"key":"17_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"518","DOI":"10.1007\/978-3-319-21690-4_36","volume-title":"Computer Aided Verification","author":"M Bozzano","year":"2015","unstructured":"Bozzano, M., et al.: Formal design and safety analysis of AIR6110 wheel brake system. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 518\u2013535. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_36"},{"key":"17_CR15","doi-asserted-by":"crossref","unstructured":"Bradley, A.R., Manna, Z.: Checking safety by inductive generalization of counterexamples to induction. In: Proceedings of the FMCAD\u201907. IEEE (2007)","DOI":"10.1109\/FAMCAD.2007.15"},{"key":"17_CR16","unstructured":"Bradley, A.: IC3 reference implementation: a short, simple, fairly competitive implementation of IC3 (2015). https:\/\/github.com\/arbrad\/IC3ref"},{"key":"17_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/978-3-642-14295-6_5","volume-title":"Computer Aided Verification","author":"R Brayton","year":"2010","unstructured":"Brayton, R., Mishchenko, A.: ABC: an academic industrial-strength verification tool. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 24\u201340. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_5"},{"key":"17_CR18","doi-asserted-by":"crossref","unstructured":"Brzozowski, J., Leiss, E.: On equations for regular languages, finite automata, and sequential networks. Theor. Comput. Sci. 10(1) (1980)","DOI":"10.1016\/0304-3975(80)90069-9"},{"key":"17_CR19","unstructured":"Brzozowski, J.A.: Canonical regular expressions and minimal state graphs for definite events. In: Proceedings of the Symposium on Mathematical Theory of Automata (1962)"},{"key":"17_CR20","doi-asserted-by":"publisher","unstructured":"B\u00fcchi, J.R.: Weak Second-Order Arithmetic and Finite Automata, pp. 398\u2013424. Springer, New York, NY (1990). https:\/\/doi.org\/10.1007\/978-1-4613-8928-6_22","DOI":"10.1007\/978-1-4613-8928-6_22"},{"key":"17_CR21","unstructured":"B\u00fcchi, J.R.: On a decision method in restricted second order arithmetic. In: Proceedings of the International Congress on Logic, Method, and Philosophy of Science. SUP (1962)"},{"key":"17_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/978-3-319-08867-9_22","volume-title":"Computer Aided Verification","author":"R Cavada","year":"2014","unstructured":"Cavada, R., et al.: The nuXmv symbolic model checker. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 334\u2013342. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_22"},{"key":"17_CR23","doi-asserted-by":"crossref","unstructured":"C\u00e9c\u00e9, G.: Foundation for a series of efficient simulation algorithms. In: Proceedings of the LICS\u201917. IEEE (2017)","DOI":"10.1109\/LICS.2017.8005069"},{"key":"17_CR24","doi-asserted-by":"crossref","unstructured":"Chandra, A.K., Kozen, D.C., Stockmeyer, L.J.: Alternation. J. ACM 28(1) (1981)","DOI":"10.1145\/322234.322243"},{"key":"17_CR25","doi-asserted-by":"crossref","unstructured":"Chen, T., Chen, Y., Hague, M., Lin, A.W., Wu, Z.: What is decidable about string constraints with the replaceall function. In: Proceedings of the POPL\u201918 (2018)","DOI":"10.1145\/3158091"},{"key":"17_CR26","doi-asserted-by":"crossref","unstructured":"Chen, T., Hague, M., Lin, A.W., R\u00fcmmer, P., Wu, Z.: Decision procedures for path feasibility of string-manipulating programs with complex operations. In: Proceedings of the POPL\u201919 (2019)","DOI":"10.1145\/3290362"},{"key":"17_CR27","unstructured":"Cox, A.: Model Checking Regular Expressions (2019). presented at MOSCA\u201919. https:\/\/mosca19.github.io\/slides\/cox.pdf"},{"key":"17_CR28","unstructured":"Cox, A., Leasure, J.: Model checking regular language constraints. CoRR abs\/1708.09073 (2017)"},{"key":"17_CR29","unstructured":"D\u2019Anthoni, L.: A symbolic automata library. https:\/\/github.com\/lorisdanto\/symbolicautomata"},{"key":"17_CR30","doi-asserted-by":"crossref","unstructured":"D\u2019Antoni, L., Kincaid, Z., Wang, F.: A symbolic decision procedure for symbolic alternating finite automata. Electron. Notes Theor. Comput. Sci. 336 (2018)","DOI":"10.1016\/j.entcs.2018.03.017"},{"key":"17_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/978-3-319-63387-9_3","volume-title":"Computer Aided Verification","author":"L D\u2019Antoni","year":"2017","unstructured":"D\u2019Antoni, L., Veanes, M.: The power of symbolic automata and transducers. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 47\u201367. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_3"},{"key":"17_CR32","doi-asserted-by":"crossref","unstructured":"D\u2019Antoni, L., Veanes, M.: Minimization of symbolic automata. In: Proceedings of the POPL\u201914. ACM (2014)","DOI":"10.1145\/2535838.2535849"},{"key":"17_CR33","doi-asserted-by":"crossref","unstructured":"D\u2019Antoni, L., Veanes, M.: Minimization of symbolic tree automata. In: Proceedings of the LICS\u201916. ACM (2016)","DOI":"10.1145\/2933575.2933578"},{"key":"17_CR34","unstructured":"De Giacomo, G., Vardi, M.Y.: Linear temporal logic and linear dynamic logic on finite traces. In: Proceedings of the IJCAI\u201913. ACM (2013)"},{"key":"17_CR35","doi-asserted-by":"publisher","unstructured":"De Wulf, M., Doyen, L., Maquet, N., Raskin, J.F.: Alaska. In: Cha, S., Choi, J.Y., Kim, M., Lee, I., Viswanathan, M. (eds.) Automated Technology for Verification and Analysis. ATVA 2008. LNCS, vol. 5311, pp. 240\u2013245. Springer, Berlin, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-88387-6_21","DOI":"10.1007\/978-3-540-88387-6_21"},{"key":"17_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-642-12002-2_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Doyen","year":"2010","unstructured":"Doyen, L., Raskin, J.-F.: Antichain algorithms for finite automata. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 2\u201322. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-12002-2_2"},{"key":"17_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502\u2013518. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24605-3_37"},{"key":"17_CR38","doi-asserted-by":"crossref","unstructured":"Fellah, A., J\u00fcrgensen, H., Yu, S.: Constructions for alternating finite automata. Int. J. Comput. Math. 35 (1990)","DOI":"10.1080\/00207169008803893"},{"key":"17_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/978-3-319-69483-2_13","volume-title":"Dependable Software Engineering. Theories, Tools, and Applications","author":"C Fu","year":"2017","unstructured":"Fu, C., Deng, Y., Jansen, D.N., Zhang, L.: On equivalence checking of nondeterministic finite automata. In: Larsen, K.G., Sokolsky, O., Wang, J. (eds.) SETTA 2017. LNCS, vol. 10606, pp. 216\u2013231. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-69483-2_13"},{"key":"17_CR40","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":"17_CR41","doi-asserted-by":"crossref","unstructured":"Ganty, P., Maquet, N., Raskin, J.: Fixed point guided abstraction refinement for alternating automata. Theor. Comput. Sci. 411(38\u201339) (2010)","DOI":"10.1016\/j.tcs.2010.05.037"},{"key":"17_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-41540-6_1","volume-title":"Computer Aided Verification","author":"M Gario","year":"2016","unstructured":"Gario, M., Cimatti, A., Mattarei, C., Tonetta, S., Rozier, K.Y.: Model checking at scale: automated air traffic control design space exploration. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 3\u201322. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_1"},{"key":"17_CR43","unstructured":"Harding, A.: Symbolic strategy synthesis for games with LTL winning conditions. Ph.D. thesis, University of Birmingham (2005)"},{"key":"17_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/3-540-60630-0_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"JG Henriksen","year":"1995","unstructured":"Henriksen, J.G., et al.: Mona: monadic second-order logic in practice. In: Brinksma, E., Cleaveland, W.R., Larsen, K.G., Margaria, T., Steffen, B. (eds.) TACAS 1995. LNCS, vol. 1019, pp. 89\u2013110. Springer, Heidelberg (1995). https:\/\/doi.org\/10.1007\/3-540-60630-0_5"},{"key":"17_CR45","unstructured":"Henzinger, M.R., Henzinger, T.A., Kopke, P.W.: Computing simulations on finite and infinite graphs. In: Proceedings of the FOCS. IEEE (1995)"},{"key":"17_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-642-31612-8_13","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"K Hoder","year":"2012","unstructured":"Hoder, K., Bj\u00f8rner, N.: Generalized property directed reachability. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 157\u2013171. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31612-8_13"},{"key":"17_CR47","doi-asserted-by":"crossref","unstructured":"Hol\u00edk, L., Jank\u016f, P., Lin, A.W., R\u00fcmmer, P., Vojnar, T.: String constraints with concatenation and transducers solved efficiently. In: Proceedings of the POPL\u201918, vol. 2 (2018)","DOI":"10.1145\/3158092"},{"key":"17_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/978-3-030-01090-4_7","volume-title":"Automated Technology for Verification and Analysis","author":"L Hol\u00edk","year":"2018","unstructured":"Hol\u00edk, L., Leng\u00e1l, O., S\u00ed\u010d, J., Veanes, M., Vojnar, T.: Simulation algorithms for symbolic automata. In: Lahiri, S.K., Wang, C. (eds.) ATVA 2018. LNCS, vol. 11138, pp. 109\u2013125. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-01090-4_7"},{"key":"17_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-642-24372-1_18","volume-title":"Automated Technology for Verification and Analysis","author":"L Hol\u00edk","year":"2011","unstructured":"Hol\u00edk, L., Leng\u00e1l, O., \u0160im\u00e1\u010dek, J., Vojnar, T.: Efficient inclusion checking on explicit and semi-symbolic tree automata. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 243\u2013258. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-24372-1_18"},{"key":"17_CR50","first-page":"1337","volume":"7","author":"L Hol\u00edk","year":"2010","unstructured":"Hol\u00edk, L., \u0160im\u00e1\u010dek, J.: Optimizing an LTS-simulation algorithm. Comput. Inform. 7, 1337\u20131348 (2010)","journal-title":"Comput. Inform."},{"key":"17_CR51","doi-asserted-by":"crossref","unstructured":"Hooimeijer, P., Weimer, W.: A decision procedure for subset constraints over regular languages. In: PLDI\u201909. ACM (2009)","DOI":"10.1145\/1542476.1542498"},{"key":"17_CR52","doi-asserted-by":"crossref","unstructured":"Hopcroft, J.E.: An n log n algorithm for minimizing states in a finite automaton. Technical report, Stanford, CA, USA (1971)","DOI":"10.1016\/B978-0-12-417750-5.50022-1"},{"key":"17_CR53","doi-asserted-by":"crossref","unstructured":"Hromkovi\u010d, J.: On the power of alternation in automata theory. J. Comput. Syst. Sci. 31(1) (1985)","DOI":"10.1016\/0022-0000(85)90063-7"},{"key":"17_CR54","doi-asserted-by":"crossref","unstructured":"Huffman, D.: The synthesis of sequential switching circuits. J. Franklin Inst. 257(3) (1954)","DOI":"10.1016\/0016-0032(54)90574-8"},{"key":"17_CR55","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":"17_CR56","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-319-89963-3_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Iosif","year":"2018","unstructured":"Iosif, R., Xu, X.: Abstraction refinement for emptiness checking of alternating data automata. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10806, pp. 93\u2013111. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89963-3_6"},{"key":"17_CR57","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Vardi, M.Y.: Weak alternating automata are not that weak. ACM Trans. Comput. Logic 2(3) (2001)","DOI":"10.1145\/377978.377993"},{"key":"17_CR58","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Vardi, M.Y., Wolper, P.: An automata-theoretic approach to branching-time model checking. J. ACM 47(2) (2000)","DOI":"10.1145\/333979.333987"},{"key":"17_CR59","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/978-3-642-28756-5_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"O Leng\u00e1l","year":"2012","unstructured":"Leng\u00e1l, O., \u0160im\u00e1\u010dek, J., Vojnar, T.: VATA: a library for efficient manipulation of non-deterministic tree automata. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 79\u201394. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28756-5_7"},{"key":"17_CR60","doi-asserted-by":"crossref","unstructured":"Li, J., Pu, G., Zhang, Y., Vardi, M.Y., Rozier, K.Y.: SAT-based explicit LTLf satisfiability checking. Artif. Intell. 289 (2020)","DOI":"10.1016\/j.artint.2020.103369"},{"key":"17_CR61","unstructured":"Lutterkort, D.: libfa. https:\/\/augeas.net\/libfa\/"},{"key":"17_CR62","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-45069-6_1","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"2003","unstructured":"McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1\u201313. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45069-6_1"},{"key":"17_CR63","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/11817963_14","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"2006","unstructured":"McMillan, K.L.: Lazy abstraction with interpolants. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 123\u2013136. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11817963_14"},{"key":"17_CR64","doi-asserted-by":"crossref","unstructured":"Moore, E.F.: Gedanken-experiments on sequential machines. In: Automata Studies, vol. 34. Princeton University Press, Princeton (1956)","DOI":"10.1515\/9781400882618-006"},{"key":"17_CR65","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"17_CR66","unstructured":"Muller, D., Saoudi, A., Schupp, P.: Weak alternating automata give a simple explanation of why most temporal and dynamic logics are decidable in exponential time. In: Proceedings of the LICS. IEEE (1988)"},{"key":"17_CR67","unstructured":"M\u00f8ller, A., et al.: Brics automata library. https:\/\/www.brics.dk\/automaton\/"},{"key":"17_CR68","doi-asserted-by":"publisher","unstructured":"N\u00f6tzli, A., Reynolds, A., Barbosa, H., Barrett, C., Tinelli, C.: Even faster conflicts and lazier reductions for string solvers. In: Shoham, S., Vizel, Y. (eds.) Computer Aided Verification. CAV 2022. LNCS, vol. 13372, pp. 205\u2013226. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-13188-2_11","DOI":"10.1007\/978-3-031-13188-2_11"},{"key":"17_CR69","doi-asserted-by":"crossref","unstructured":"Paige, R., Tarjan, R.E.: Three partition refinement algorithms. SIAM J. Comput. 16(6) (1987)","DOI":"10.1137\/0216062"},{"key":"17_CR70","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.ic.2009.06.002","volume":"208","author":"F Ranzato","year":"2010","unstructured":"Ranzato, F., Tapparo, F.: An efficient simulation algorithm based on abstract interpretation. Inf. Comput. 208, 1\u201322 (2010)","journal-title":"Inf. Comput."},{"key":"17_CR71","unstructured":"RegExLib.com: The Internet\u2019s first Regular Expression Library. http:\/\/regexlib.com\/"},{"key":"17_CR72","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-3-540-73370-6_11","volume-title":"Model Checking Software","author":"KY Rozier","year":"2007","unstructured":"Rozier, K.Y., Vardi, M.Y.: LTL satisfiability checking. In: Bo\u0161na\u010dki, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol. 4595, pp. 149\u2013167. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73370-6_11"},{"key":"17_CR73","doi-asserted-by":"crossref","unstructured":"Stanford, C., Veanes, M., Bj\u00f8rner, N.S.: Symbolic boolean derivatives for efficiently solving extended regular expression constraints. In: Proceedings of the PLDI\u201921. ACM (2021)","DOI":"10.1145\/3453483.3454066"},{"key":"17_CR74","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"396","DOI":"10.1007\/11591191_28","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"D Tabakov","year":"2005","unstructured":"Tabakov, D., Vardi, M.Y.: Experimental evaluation of classical automata constructions. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol. 3835, pp. 396\u2013411. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11591191_28"},{"key":"17_CR75","doi-asserted-by":"crossref","unstructured":"Valmari, A.: Simple bisimilarity minimization in O(m log n) time. Fundam. Inform. 105(3) (2010)","DOI":"10.3233\/FI-2010-369"},{"key":"17_CR76","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"575","DOI":"10.1007\/3-540-57887-0_116","volume-title":"Theoretical Aspects of Computer Software","author":"MY Vardi","year":"1994","unstructured":"Vardi, M.Y.: Nontraditional applications of automata theory. In: Hagiya, M., Mitchell, J.C. (eds.) TACS 1994. LNCS, vol. 789, pp. 575\u2013597. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/3-540-57887-0_116"},{"key":"17_CR77","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":"17_CR78","unstructured":"Veanes, M.: A.NET automata library. https:\/\/github.com\/AutomataDotNet\/Automata"},{"key":"17_CR79","doi-asserted-by":"crossref","unstructured":"Veanes, M., de Halleux, P., Tillmann, N.: Rex: symbolic regular expression explorer. In: Proceedings of the ICST\u201910. IEEE (2010)","DOI":"10.1109\/ICST.2010.15"},{"key":"17_CR80","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1007\/978-3-319-41528-4_13","volume-title":"Computer Aided Verification","author":"H-E Wang","year":"2016","unstructured":"Wang, H.-E., Tsai, T.-L., Lin, C.-H., Yu, F., Jiang, J.-H.R.: String analysis via automata manipulation with logic circuit representation. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 241\u2013260. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_13"},{"key":"17_CR81","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_CR82","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","Automated Deduction \u2013 CADE 29"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-38499-8_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,1]],"date-time":"2023-09-01T23:05:47Z","timestamp":1693609547000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-38499-8_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031384981","9783031384998"],"references-count":82,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-38499-8_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"2 September 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CADE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Deduction","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Rome","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 July 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 July 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cade2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/easyconferences.eu\/cade2023\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"77","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"28","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"36% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}