{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T03:42:54Z","timestamp":1740109374431,"version":"3.37.3"},"reference-count":39,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2022,6,22]],"date-time":"2022-06-22T00:00:00Z","timestamp":1655856000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,6,22]],"date-time":"2022-06-22T00:00:00Z","timestamp":1655856000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100005416","name":"Research Council of Norway","doi-asserted-by":"crossref","award":["288761"],"award-info":[{"award-number":["288761"]}],"id":[{"id":"10.13039\/501100005416","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100003593","name":"Conselho Nacional de Desenvolvimento Cient\u00edfico e Tecnol\u00f3gico","doi-asserted-by":"publisher","award":["CNPQ 140399\/2017-8"],"award-info":[{"award-number":["CNPQ 140399\/2017-8"]}],"id":[{"id":"10.13039\/501100003593","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002322","name":"Coordena\u00e7\u00e3o de Aperfei\u00e7oamento de Pessoal de N\u00edvel Superior","doi-asserted-by":"publisher","award":["CAPES 88881.187636\/2018-01"],"award-info":[{"award-number":["CAPES 88881.187636\/2018-01"]}],"id":[{"id":"10.13039\/501100002322","id-type":"DOI","asserted-by":"publisher"}]},{"name":"University of Bergen"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Theory Comput Syst"],"published-print":{"date-parts":[[2022,8]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Traditionally, finite automata theory has been used as a framework for the representation of possibly infinite sets of strings. In this work, we introduce the notion of second-order finite automata, a formalism that combines finite automata with ordered decision diagrams, with the aim of representing possibly infinite<jats:italic>sets of sets<\/jats:italic>of strings. Our main result states that second-order finite automata can be canonized with respect to the second-order languages they represent. Using this canonization result, we show that sets of sets of strings represented by second-order finite automata are closed under the usual Boolean operations, such as union, intersection, difference and even under a suitable notion of complementation. Additionally, emptiness of intersection and inclusion are decidable. We provide two algorithmic applications for second-order automata. First, we show that several width\/size minimization problems for deterministic and nondeterministic ODDs are solvable in fixed-parameter tractable time when parameterized by the width of the input ODD. In particular, our results imply FPT algorithms for corresponding width\/size minimization problems for ordered binary decision diagrams (OBDDs) with a fixed variable ordering. Previously, only algorithms that take exponential time in the size of the input OBDD were known for width minimization, even for OBDDs of constant width. Second, we show that for each<jats:italic>k<\/jats:italic>and<jats:italic>w<\/jats:italic>one can count the number of distinct functions computable by ODDs of width at most<jats:italic>w<\/jats:italic>and length<jats:italic>k<\/jats:italic>in time<jats:italic>h<\/jats:italic>(|\u03a3|,<jats:italic>w<\/jats:italic>) \u22c5<jats:italic>k<\/jats:italic><jats:sup><jats:italic>O<\/jats:italic>(1)<\/jats:sup>, for a suitable<jats:inline-formula><jats:alternatives><jats:tex-math>$h:\\mathbb {N}\\times \\mathbb {N}\\rightarrow \\mathbb {N}$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mi>h<\/mml:mi><mml:mo>:<\/mml:mo><mml:mi>\u2115<\/mml:mi><mml:mo>\u00d7<\/mml:mo><mml:mi>\u2115<\/mml:mi><mml:mo>\u2192<\/mml:mo><mml:mi>\u2115<\/mml:mi><\/mml:math><\/jats:alternatives><\/jats:inline-formula>. This improves exponentially on the time necessary to explicitly enumerate all such functions, which is exponential in both the width parameter<jats:italic>w<\/jats:italic>and in the length<jats:italic>k<\/jats:italic>of the ODDs.<\/jats:p>","DOI":"10.1007\/s00224-022-10085-w","type":"journal-article","created":{"date-parts":[[2022,6,22]],"date-time":"2022-06-22T11:03:03Z","timestamp":1655895783000},"page":"861-909","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Second-Order Finite Automata"],"prefix":"10.1007","volume":"66","author":[{"given":"Alexsander Andrade","family":"de Melo","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7798-7446","authenticated-orcid":false,"given":"Mateus","family":"de Oliveira Oliveira","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,6,22]]},"reference":[{"key":"10085_CR1","first-page":"1","volume":"379","author":"V Baranyi","year":"2011","unstructured":"Baranyi, V., Gr\u00e4del, E., Rubin, S.: Automata-based presentations of infinite structures. Finite and Algorithmic Model Theory 379, 1 (2011)","journal-title":"Finite and Algorithmic Model Theory"},{"key":"10085_CR2","doi-asserted-by":"crossref","unstructured":"Blumensath, A., Gr\u00e4del, E.: Automatic structures. In: Proc. of the 15th Annual IEEE Symposium on Logic in Computer Science (LICS 2000), pp. 51\u201362. IEEE Computer Society (2000)","DOI":"10.1109\/LICS.2000.855755"},{"key":"10085_CR3","doi-asserted-by":"crossref","unstructured":"Bollig, B.: On the width of ordered binary decision diagrams. In: Zhang, Z., Wu, L., Xu, W., Du, D. (eds.) Proc. of the 8th International Conference on Combinatorial Optimization and Applications (COCOA 2014) volume 8881 of Lecture Notes in Computer Science, pp. 444\u2013458. Springer (2014)","DOI":"10.1007\/978-3-319-12691-3_33"},{"issue":"3","key":"10085_CR4","doi-asserted-by":"publisher","first-page":"532","DOI":"10.1007\/s00224-015-9657-x","volume":"59","author":"B Bollig","year":"2016","unstructured":"Bollig, B.: On the minimization of (complete) ordered binary decision diagrams. Theory Comput. Syst. 59(3), 532\u2013559 (2016)","journal-title":"Theory Comput. Syst."},{"issue":"1","key":"10085_CR5","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1016\/j.entcs.2005.11.015","volume":"149","author":"A Bouajjani","year":"2006","unstructured":"Bouajjani, A., Habermehl, P., Rogalewicz, A., Vojnar, T.: Abstract regular tree model checking. Electron. Notes Theor. Comput. Sci. 149 (1), 37\u201348 (2006)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"1\u20133","key":"10085_CR6","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1016\/j.tcs.2007.11.022","volume":"393","author":"S Bozapalidis","year":"2008","unstructured":"Bozapalidis, S., Kalampakas, A.: Graph automata. Theor. Comput. Sci. 393(1\u20133), 147\u2013165 (2008)","journal-title":"Theor. Comput. Sci."},{"issue":"4","key":"10085_CR7","doi-asserted-by":"publisher","first-page":"806","DOI":"10.1016\/j.jcss.2013.12.001","volume":"80","author":"J Case","year":"2014","unstructured":"Case, J., Jain, S., Ong, Y.S., Semukhin, P., Stephan, F.: Automatic learners with feedback queries. J. Comput. Syst. Sci. 80(4), 806\u2013820 (2014)","journal-title":"J. Comput. Syst. Sci."},{"key":"10085_CR8","doi-asserted-by":"crossref","unstructured":"Case, J., Jain, S., Stephan, F., Stephan, F.: Automatic functions, linear time and learning. Log. Methods Comput. Sci. (2013)","DOI":"10.2168\/LMCS-9(3:19)2013"},{"issue":"2","key":"10085_CR9","doi-asserted-by":"publisher","first-page":"4","DOI":"10.2168\/LMCS-3(2:4)2007","volume":"3","author":"T Colcombet","year":"2007","unstructured":"Colcombet, T., L\u00f6ding, C.: Transforming structures by set interpretations. Log. Methods Comput. Sci. 3(2), 4 (2007)","journal-title":"Log. Methods Comput. Sci."},{"key":"10085_CR10","doi-asserted-by":"crossref","unstructured":"Courcelle, B.: On recognizable sets and tree automata. In: Algebraic Techniques, pp. 93\u2013126. Elsevier (1989)","DOI":"10.1016\/B978-0-12-046370-1.50009-7"},{"issue":"1","key":"10085_CR11","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1016\/0890-5401(90)90043-H","volume":"85","author":"B Courcelle","year":"1990","unstructured":"Courcelle, B.: The monadic second-order logic of graphs. I. Recognizable sets of finite graphs. Inf. Comput. 85(1), 12\u201375 (1990)","journal-title":"Inf. Comput."},{"key":"10085_CR12","unstructured":"Courcelle, B., Durand, I.: Verifying monadic second order graph properties with tree automata. In: Rhodes, C. (ed.) Proc. of the 3rd European Lisp Symposium (ELS 2010), pp. 7\u201321. ELSAA (2010)"},{"key":"10085_CR13","doi-asserted-by":"crossref","unstructured":"De Melo, A.A., De Oliveira Oliveira, M.: On the width of regular classes of finite structures. In: Fontaine, P. (ed.) Proc. of the 27th International Conference on Automated Deduction (CADE 2019), volume 11716 of Lecture Notes in Computer Science, pp. 18\u201334. Springer (2019)","DOI":"10.1007\/978-3-030-29436-6_2"},{"key":"10085_CR14","doi-asserted-by":"crossref","unstructured":"De Melo, A.A., De Oliveira Oliveira, M.: Second-order finite automata. In: Fernau, H. (ed.) Proc. of the 15th International Computer Science Symposium in Russia (CSR 2020), volume 12159 of Lecture Notes in Computer Science, pp. 46\u201363 (2020)","DOI":"10.1007\/978-3-030-50026-9_4"},{"key":"10085_CR15","doi-asserted-by":"crossref","unstructured":"De Melo, A.A., De Oliveira Oliveira, M.: Symbolic solutions for symbolic constraint satisfaction problems. In: Calvanese, D., Erdem, E., Thielscher, M. (eds.) Proc. of the 17th International Conference on Principles of Knowledge Representation and Reasoning (KR 2020), pp. 49\u201358 (2020)","DOI":"10.24963\/kr.2020\/6"},{"key":"10085_CR16","doi-asserted-by":"crossref","unstructured":"Ebbinghaus, H.-D., Flum, J.: Finite automata and logic: A microcosm of finite model theory. In: Finite Model Theory, pp. 107\u2013118. Springer (1995)","DOI":"10.1007\/978-3-662-03182-7_6"},{"key":"10085_CR17","doi-asserted-by":"crossref","unstructured":"Erg\u00fcn, F., Kumar, R., Rubinfeld, R.: On learning bounded-width branching programs. In: Maass, W. (ed.) Proc. of the Eigth Annual Conference on Computational Learning Theory (COLT 1995), pp. 361\u2013368. ACM (1995)","DOI":"10.1145\/225298.225342"},{"key":"10085_CR18","doi-asserted-by":"crossref","unstructured":"Forbes, M.A., Kelley, Z.: Pseudorandom generators for read-once branching programs, in any order. In: Thorup, M. (ed.) Proc. of the 59th IEEE Annual Symposium on Foundations of Computer Science (FOCS 2018), pp. 946\u2013955. IEEE Computer Society (2018)","DOI":"10.1109\/FOCS.2018.00093"},{"issue":"2&3","key":"10085_CR19","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1142\/S021800149200014X","volume":"6","author":"D Giammarresi","year":"1992","unstructured":"Giammarresi, D., Restivo, A.: Recognizable picture languages. Int. J. Pattern Recognit. Artif. Intell. 6(2&3), 241\u2013256 (1992)","journal-title":"Int. J. Pattern Recognit. Artif. Intell."},{"key":"10085_CR20","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Using partial orders to improve automatic verification methods. In: Clarke, E.M., Kurshan, R.P. (eds.) 2nd International Workshop on Computer Aided Verification (CAV 1990), volume 531 of Lecture Notes in Computer Science, pp. 176\u2013185. Springer (1990)","DOI":"10.1007\/BFb0023731"},{"key":"10085_CR21","unstructured":"Goldreich, O.: On testing computability by small width obdds. In: Serna, M.J., Shaltiel, R., Jansen, K., Rolim, J.D.P. (eds.) Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques, Proc. of the 13th International Workshop, APPROX 2010, and 14th International Workshop, RANDOM 2010, volume 6302 of Lecture Notes in Computer Science, pp. 574\u2013587. Springer (2010)"},{"key":"10085_CR22","doi-asserted-by":"crossref","unstructured":"Gr\u00e4del, E.: Automatic structures: twenty years later. In: Inproceedings of the 35Th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS \u201920, pp. 21\u201334. New York, NY,USA, Association for Computing Machinery (2020)","DOI":"10.1145\/3373718.3394734"},{"issue":"1","key":"10085_CR23","first-page":"39","volume":"7","author":"BR Hodgsonl","year":"1983","unstructured":"Hodgsonl, B.R.: D\u00e9cidabilit\u00e9 par automate fini. Annales des sciences math\u00e9matiques du Qu\u00e9bec 7(1), 39\u201357 (1983)","journal-title":"Annales des sciences math\u00e9matiques du Qu\u00e9bec"},{"key":"10085_CR24","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1016\/j.tcs.2017.12.031","volume":"742","author":"R H\u00f6lzl","year":"2018","unstructured":"H\u00f6lzl, R., Jain, S., Stephan, F.: Learning pattern languages over groups. Theor. Comput. Sci. 742, 66\u201381 (2018)","journal-title":"Theor. Comput. Sci."},{"key":"10085_CR25","doi-asserted-by":"crossref","unstructured":"Hopcroft, J.: An n log n algorithm for minimizing states in a finite automaton. In: Theory of machines and computations, pp. 189\u2013196. Elsevier (1971)","DOI":"10.1016\/B978-0-12-417750-5.50022-1"},{"key":"10085_CR26","unstructured":"Hopcroft, J., Motwani, R., Ullman, J.: Introduction to Automata Theory Languages, and Computation. Pearson\/Addison Wesley (2007)"},{"key":"10085_CR27","doi-asserted-by":"crossref","unstructured":"Howar, F., Steffen, B.: Active automata learning in practice - an annotated bibliography of the years 2011 to 2016. In: Bennaceur, A., H\u00e4hnle, R., Meinke, K. (eds.) Machine Learning for Dynamic Software Analysis: Potentials and Limits - International Dagstuhl Seminar 16172, volume 11026 of Lecture Notes in Computer Science, pp. 123\u2013148. Springer (2018)","DOI":"10.1007\/978-3-319-96562-8_5"},{"key":"10085_CR28","unstructured":"Jain, S., Kinber, E.B.: Automatic learning from positive data and negative counterexamples. In: Stoltz, G., Vayatis, N., Zeugmann, T. (eds.) Algorithmic Learning Theory - 23rd International Conference, ALT 2012, Lyon, France, October 29-31 Proceedings, volume 7568 of Lecture Notes in Computer Science, pp. 66\u201380. Springer (2012)"},{"issue":"6","key":"10085_CR29","doi-asserted-by":"publisher","first-page":"1910","DOI":"10.1016\/j.jcss.2011.12.011","volume":"78","author":"S Jain","year":"2012","unstructured":"Jain, S., Luo, Q., Stephan, F.: Learnability of automatic classes. J. Comput. Syst. Sci. 78(6), 1910\u20131927 (2012)","journal-title":"J. Comput. Syst. Sci."},{"key":"10085_CR30","doi-asserted-by":"crossref","unstructured":"Kartzow, A., Schlicht, P.: Structures without scattered-automatic presentation. In: Bonizzoni, P., Brattka, V., L\u00f6we, B. (eds.) Proc. of the 9th Conference on Computability in Europe (CiE 2013), volume 7921 of Lecture Notes in Computer Science, pp. 273\u2013283. Springer (2013)","DOI":"10.1007\/978-3-642-39053-1_32"},{"key":"10085_CR31","doi-asserted-by":"crossref","unstructured":"Khoussainov, B., Nerode, A.: Automatic presentations of structures. In: International Workshop on Logical and Computational Complexity (LCC 1994), volume 960 of Lecture Notes in Computer Science, pp. 367\u2013392. Springer (1995)","DOI":"10.1007\/3-540-60178-3_93"},{"key":"10085_CR32","doi-asserted-by":"crossref","unstructured":"Kuske, D.: Second-order finite automata: Expressive power and simple proofs using automatic structures. In: Moreira, N., Reis, R. (eds.) Proc. of the 25th International Conference on Developments in Language Theory (DLT 2021), volume 12811 of Lecture Notes in Computer Science, pp. 242\u2013254. Springer (2021)","DOI":"10.1007\/978-3-030-81508-0_20"},{"issue":"5","key":"10085_CR33","doi-asserted-by":"publisher","first-page":"1557","DOI":"10.1137\/S009753970038211X","volume":"31","author":"I Newman","year":"2002","unstructured":"Newman, I.: Testing membership in languages that have small width branching programs. SIAM J. Comput. 31(5), 1557\u20131570 (2002)","journal-title":"SIAM J. Comput."},{"issue":"3","key":"10085_CR34","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1016\/0304-3975(83)90113-5","volume":"25","author":"L Priese","year":"1983","unstructured":"Priese, L.: Automata and concurrency. Theor. Comput. Sci. 25 (3), 221\u2013265 (1983)","journal-title":"Theor. Comput. Sci."},{"key":"10085_CR35","doi-asserted-by":"crossref","unstructured":"Ron, D., Tsur, G.: Testing computability by width two obdds. In: Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques, pp. 686\u2013699. Springer (2009)","DOI":"10.1007\/978-3-642-03685-9_51"},{"key":"10085_CR36","doi-asserted-by":"crossref","unstructured":"Thomas, W.: Automata theory on trees and partial orders. In: Bidoit, M., Dauchet, M. (eds.) Proc. of the 7th International Joint Conference on Theory and Practice of Software Development (TAPSOFT 1997), volume 1214 of Lecture Notes in Computer Science, pp. 20\u201338. Springer (1997)","DOI":"10.1007\/BFb0030586"},{"key":"10085_CR37","doi-asserted-by":"crossref","unstructured":"Wegener, I.: Branching programs and binary decision diagrams. SIAM (2000)","DOI":"10.1137\/1.9780898719789"},{"key":"10085_CR38","unstructured":"Zaid, F.A.: Algorithmic solutions via model theoretic interpretations. Ph.D. Dissertation RWTH Aachen University (2016)"},{"key":"10085_CR39","unstructured":"Zaid, F.A., Gr\u00e4del, E., Reinhardt, F.: Advice automatic structures and uniformly automatic classes. In: Goranko, V., Dam, M. (eds.) Proc. of the 26th EACSL Annual Conference on Computer Science Logic (CSL 2017), volume 82 of LIPIcs, pp. 35:1\u201335:20. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2017)"}],"container-title":["Theory of Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00224-022-10085-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00224-022-10085-w\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00224-022-10085-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,27]],"date-time":"2024-09-27T12:10:26Z","timestamp":1727439026000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s00224-022-10085-w"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,6,22]]},"references-count":39,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2022,8]]}},"alternative-id":["10085"],"URL":"https:\/\/doi.org\/10.1007\/s00224-022-10085-w","relation":{},"ISSN":["1432-4350","1433-0490"],"issn-type":[{"type":"print","value":"1432-4350"},{"type":"electronic","value":"1433-0490"}],"subject":[],"published":{"date-parts":[[2022,6,22]]},"assertion":[{"value":"30 April 2022","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"22 June 2022","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"20 August 2022","order":3,"name":"change_date","label":"Change Date","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"Update","order":4,"name":"change_type","label":"Change Type","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"Funding information has been added in the Funding Note.","order":5,"name":"change_details","label":"Change Details","group":{"name":"ArticleHistory","label":"Article History"}}]}}