{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T09:05:48Z","timestamp":1784797548446,"version":"3.55.0"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032325259","type":"print"},{"value":"9783032325266","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,7,24]],"date-time":"2026-07-24T00:00:00Z","timestamp":1784851200000},"content-version":"vor","delay-in-days":204,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    We present an SMT-based active learning algorithm for nondeterministic weighted automata (WFAs) as a practical and robust alternative to Hankel\/\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$\\textsf{L}^\\star $$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:msup>\n                            <mml:mi>L<\/mml:mi>\n                            <mml:mo>\u22c6<\/mml:mo>\n                          <\/mml:msup>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    -style methods. Our algorithm is parametric in a given semiring and, if it terminates, guaranteed to produce\n                    <jats:italic>minimal<\/jats:italic>\n                    WFAs. We prove partial correctness and provide a sufficient termination condition, which in particular implies termination for all finite semirings. Our extensive experimental evaluation shows that our algorithm is capable of learning numerous minimal WFAs over both finite and infinite semirings, vastly outperforms a naive baseline, and is competitive with a state-of-the-art algorithm while producing significantly smaller automata and requiring less interaction with the teacher.\n                  <\/jats:p>","DOI":"10.1007\/978-3-032-32526-6_15","type":"book-chapter","created":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T08:44:25Z","timestamp":1784796265000},"page":"307-330","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["SMT-Based Active Learning of Weighted Automata"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6942-0228","authenticated-orcid":false,"given":"Tiago","family":"Ferreira","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8705-2564","authenticated-orcid":false,"given":"Kevin","family":"Batz","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5014-9784","authenticated-orcid":false,"given":"Alexandra","family":"Silva","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,7,24]]},"reference":[{"key":"15_CR1","doi-asserted-by":"publisher","unstructured":"Handbook of weighted automata (2009). https:\/\/doi.org\/10.1007\/978-3-642-01492-5. https:\/\/link.springer.com\/10.1007\/978-3-642-01492-5","DOI":"10.1007\/978-3-642-01492-5"},{"key":"15_CR2","doi-asserted-by":"publisher","unstructured":"Aarts, F., Ruiter, J.D., Poll, E.: Formal models of bank cards for free. In: 2013 IEEE Sixth International Conference on Software Testing, Verification and Validation Workshops, pp. 461\u2013468 (2013). https:\/\/doi.org\/10.1109\/ICSTW.2013.60","DOI":"10.1109\/ICSTW.2013.60"},{"key":"15_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"673","DOI":"10.1007\/978-3-642-16558-0_54","volume-title":"Leveraging applications of formal methods, verification, and validation","author":"F Aarts","year":"2010","unstructured":"Aarts, F., Schmaltz, J., Vaandrager, F.: Inference and Abstraction of the Biometric Passport. In: Margaria, T., Steffen, B. (eds.) ISoLA 2010. LNCS, vol. 6415, pp. 673\u2013686. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-16558-0_54"},{"key":"15_CR4","doi-asserted-by":"publisher","unstructured":"Almagor, S., Boker, U., Kupferman, O.: What\u2019s decidable about weighted automata? Inf. Comput. 282, 104651. https:\/\/doi.org\/10.1016\/j.ic.2020.104651. https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0890540120301395","DOI":"10.1016\/j.ic.2020.104651"},{"key":"15_CR5","doi-asserted-by":"publisher","unstructured":"Angluin, D.: Learning regular sets from queries and counterexamples. Inf. Comput. 75(2), 87\u2013106 (1987). https:\/\/doi.org\/10.1016\/0890-5401(87)90052-6. https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/0890540187900526","DOI":"10.1016\/0890-5401(87)90052-6"},{"key":"15_CR6","doi-asserted-by":"publisher","unstructured":"Aristote, Q., Van\u00a0Gool, S., Petri\u015fan, D., Shirmohammadi, M.: Learning weighted automata over number rings, concretely and categorically. In: 2025 40th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS), pp. 417\u2013430. IEEE (2025). https:\/\/doi.org\/10.1109\/LICS65433.2025.00038. https:\/\/ieeexplore.ieee.org\/document\/11186332\/","DOI":"10.1109\/LICS65433.2025.00038"},{"issue":"OOPSLA1","key":"15_CR7","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3527310","volume":"6","author":"K Batz","year":"2022","unstructured":"Batz, K., Gallus, A., Kaminski, B.L., Katoen, J.P., Winkler, T.: Weighted programming: a programming paradigm for specifying mathematical models. Proc. ACM Program. Lang. 6(OOPSLA1), 1\u201330 (2022). https:\/\/doi.org\/10.1145\/3527310","journal-title":"Proc. ACM Program. Lang."},{"key":"15_CR8","doi-asserted-by":"publisher","unstructured":"Bergadano, F., Varricchio, S.: Learning behaviors of automata from multiplicity and equivalence queries. SIAM J. Comput. 25(6), 1268\u20131280 (1996). https:\/\/doi.org\/10.1137\/S009753979326091X. http:\/\/epubs.siam.org\/doi\/10.1137\/S009753979326091X","DOI":"10.1137\/S009753979326091X"},{"key":"15_CR9","doi-asserted-by":"publisher","unstructured":"Biermann, A.W., Feldman, J.A.: On the synthesis of finite-state machines from samples of their behavior. IEEE Trans. Comput. C 21(6), 592\u2013597 (1972). https:\/\/doi.org\/10.1109\/TC.1972.5009015","DOI":"10.1109\/TC.1972.5009015"},{"key":"15_CR10","unstructured":"Bollig, B., Habermehl, P., Kern, C., Leucker, M.: Angluin-style learning of NFA. In: Proceedings of the 21st International Joint Conference on Artificial Intelligence, pp. 1004\u20131009. Morgan Kaufmann Publishers Inc IJCAI&apos;09"},{"key":"15_CR11","doi-asserted-by":"publisher","unstructured":"Bonsangue, M.M., Milius, S., Silva, A.: Sound and complete axiomatizations of coalgebraic language equivalence. ACM Trans. Comput. Log. 14(1), 1\u201352 (2013). https:\/\/doi.org\/10.1145\/2422085.2422092. https:\/\/dl.acm.org\/doi\/10.1145\/2422085.2422092","DOI":"10.1145\/2422085.2422092"},{"key":"15_CR12","doi-asserted-by":"publisher","unstructured":"Buna-Marginean, A., Cheval, V., Shirmohammadi, M., Worrell, J.: On learning polynomial recursive programs. Proc. ACM on Program. Lang. 8, 1001\u2013102. https:\/\/doi.org\/10.1145\/3632876. https:\/\/dl.acm.org\/doi\/10.1145\/3632876","DOI":"10.1145\/3632876"},{"key":"15_CR13","doi-asserted-by":"publisher","unstructured":"Chapman, M., Chockler, H., Kesseli, P., Kroening, D., Strichman, O., Tautschnig, M.: Learning the language of error. In: Finkbeiner, B., Pu, G., Zhang, L. (eds.) Automated Technology for Verification and Analysis, vol.\u00a09364, pp. 114\u2013130. Springer International Publishing (2015).https:\/\/doi.org\/10.1007\/978-3-319-24953-7_9. http:\/\/link.springer.com\/10.1007\/978-3-319-24953-7_9, series Title: Lecture Notes in Computer Science","DOI":"10.1007\/978-3-319-24953-7_9"},{"key":"15_CR14","doi-asserted-by":"publisher","unstructured":"Cimatti, A., Griggio, A., Irfan, A., Roveri, M., Sebastiani, R.: Incremental linearization for satisfiability and verification modulo nonlinear arithmetic and transcendental functions. ACM Trans. Comput. Logic 19(3), 1\u201352 (2018). https:\/\/doi.org\/10.1145\/3230639","DOI":"10.1145\/3230639"},{"key":"15_CR15","doi-asserted-by":"publisher","unstructured":"Daviaud, L., Johnson, M.: Feasability of learning weighted automata on a semiring. Logical Meth. Comput. Sci. 21(3), 13612. https:\/\/doi.org\/10.46298\/lmcs-21(3:15)2025. https:\/\/doi.org\/10.46298\/lmcs-21(3:15)2025","DOI":"10.46298\/lmcs-21(3:15)2025"},{"key":"15_CR16","doi-asserted-by":"publisher","unstructured":"Denis, F., Lemay, A., Terlutte, A.: Residual finite state automata. In: Ferreira, A., Reichel, H. (eds.) STACS 2001, vol. 2010, pp. 144\u2013157. Springer Berlin Heidelberg. https:\/\/doi.org\/10.1007\/3-540-44693-1_13. http:\/\/link.springer.com\/10.1007\/3-540-44693-1_13, series Title: Lecture Notes in Computer Science","DOI":"10.1007\/3-540-44693-1_13"},{"key":"15_CR17","doi-asserted-by":"publisher","unstructured":"Dierl, S., Fiterau-Brostean, P., Howar, F., Jonsson, B., Sagonas, K., T\u00e5quist, F.: Scalable tree-based register automata learning. In: Finkbeiner, B., Kov\u00e1cs, L. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, vol. 14571, pp. 87\u2013108. Springer Nature Switzerlandhttps:\/\/doi.org\/10.1007\/978-3-031-57249-4_5. https:\/\/link.springer.com\/10.1007\/978-3-031-57249-4_5, series Title: Lecture Notes in Computer Science","DOI":"10.1007\/978-3-031-57249-4_5"},{"key":"15_CR18","doi-asserted-by":"publisher","unstructured":"Ferreira, T., Batz, K., Silva, A.: SMT-based active learning of weighted automata (artifact). Zenodo (2026). https:\/\/doi.org\/10.5281\/ZENODO.19701329","DOI":"10.5281\/ZENODO.19701329"},{"key":"15_CR19","doi-asserted-by":"publisher","unstructured":"Ferreira, T., Brewton, H., D\u2019Antoni, L., Silva, A.: Prognosis: closed-box analysis of network protocol implementations. In: SIGCOMM, pp. 762\u2013774 ACM. https:\/\/doi.org\/10.1145\/3452296.3472938","DOI":"10.1145\/3452296.3472938"},{"key":"15_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"454","DOI":"10.1007\/978-3-319-41540-6_25","volume-title":"Computer Aided Verification","author":"P Fiter\u0103u-Bro\u015ftean","year":"2016","unstructured":"Fiter\u0103u-Bro\u015ftean, P., Janssen, R., Vaandrager, F.: Combining model learning and model checking to analyze TCP implementations. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 454\u2013471. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_25"},{"key":"15_CR21","doi-asserted-by":"publisher","unstructured":"Fujiwara, S., Bochmann, V., G., Khendek, F., Amalou, M., Ghedamsi, A.: Test selection based on finite state models 17(6), 591\u2013603. https:\/\/doi.org\/10.1109\/32.87284","DOI":"10.1109\/32.87284"},{"key":"15_CR22","doi-asserted-by":"publisher","unstructured":"Gao, S., Avigad, J., Clarke, E.M.: $$\\delta $$-complete decision procedures for satisfiability over the reals. In: Gramlich, B., Miller, D., Sattler, U. (eds.) Automated Reasoning, vol.\u00a07364, pp. 286\u2013300. Springer Berlin Heidelber. https:\/\/doi.org\/10.1007\/978-3-642-31365-3_23","DOI":"10.1007\/978-3-642-31365-3_23"},{"key":"15_CR23","unstructured":"van Heerdt, G.: Efficient inference of mealy machines (2014)"},{"key":"15_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"602","DOI":"10.1007\/978-3-030-45231-5_31","volume-title":"Computer Aided Verification","author":"G van Heerdt","year":"2020","unstructured":"van Heerdt, G., Kupke, C., Rot, J., Silva, A.: Learning weighted automata over principal ideal domains. In: CAV 2016. LNCS, vol. 9780, pp. 602\u2013621. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45231-5_31"},{"key":"15_CR25","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/978-3-642-15488-1_7","volume-title":"Grammatical Inference: Theoretical Results and Applications","author":"MJH Heule","year":"2010","unstructured":"Heule, M.J.H., Verwer, S.: Exact DFA identification using SAT solvers. In: Sempere, J.M., Garc\u00eda, P. (eds.) ICGI 2010. LNCS (LNAI), vol. 6339, pp. 66\u201379. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15488-1_7"},{"key":"15_CR26","doi-asserted-by":"publisher","unstructured":"Marksteiner, S., Sirjani, M., Sj\u00f6din, M.: Automated passport control: mining and checking models of machine readable travel documents. In: Proceedings of the 19th International Conference on Availability, Reliability and Security, pp.\u00a01\u20138. ARES \u201924, Association for Computing Machinery (2024). https:\/\/doi.org\/10.1145\/3664476.3670454. https:\/\/dl.acm.org\/doi\/10.1145\/3664476.3670454","DOI":"10.1145\/3664476.3670454"},{"key":"15_CR27","doi-asserted-by":"publisher","unstructured":"Moeller, M., Wiener, T., Solko-Breslin, A., Koch, C., Foster, N., Silva, A.: Automata learning with an incomplete teacher. In: Ali, K., Salvaneschi, G. (eds.) 37th European Conference on Object-Oriented Programming, ECOOP 2023, Seattle, Washington, United States, 17\u201321 July 2023. LIPIcs, vol.\u00a0263, pp. 21:1\u201321:30. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2023). https:\/\/doi.org\/10.4230\/LIPICS.ECOOP.2023.21","DOI":"10.4230\/LIPICS.ECOOP.2023.21"},{"key":"15_CR28","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":"15_CR29","doi-asserted-by":"publisher","unstructured":"Neider, D., Smetsers, R., Vaandrager, F., Kuppens, H.: Benchmarks for automata learning and conformance testing. In: Margaria, T., Graf, S., Larsen, K.G. (eds.) Models, Mindsets, Meta: The What, the How, and the Why Not?, vol. 11200, pp. 390\u2013416. Springer International Publishi. https:\/\/doi.org\/10.1007\/978-3-030-22348-9_23","DOI":"10.1007\/978-3-030-22348-9_23"},{"key":"15_CR30","doi-asserted-by":"publisher","unstructured":"Oliveira, A.L., Silva, J.P.M.: Efficient algorithms for the inference of minimum size DFAS. Mach. Learn. 44(1\/2), 93\u2013119 (2001). https:\/\/doi.org\/10.1023\/A:1010828029885","DOI":"10.1023\/A:1010828029885"},{"key":"15_CR31","doi-asserted-by":"publisher","unstructured":"Pasti, C., Karag\u00f6z, T., Nowak, F., Svete, A., Boumasmoud, R., Cotterell, R.: An l* algorithm for deterministic weighted regular languages. In: Proceedings of the 2024 Conference on Empirical Methods in Natural Language Processing, pp. 8197\u20138210. Association for Computational Linguistics. https:\/\/doi.org\/10.18653\/v1\/2024.emnlp-main.468. https:\/\/aclanthology.org\/2024.emnlp-main.468","DOI":"10.18653\/v1\/2024.emnlp-main.468"},{"key":"15_CR32","doi-asserted-by":"publisher","unstructured":"Peled, D., Vardi, M.Y., Yannakakis, M.: Black box checking. In: Wu, J., Chanson, S.T., Gao, Q. (eds.) Formal Methods for Protocol Engineering and Distributed Systems, vol.\u00a028, pp. 225\u2013240. Springer US (1999). https:\/\/doi.org\/10.1007\/978-0-387-35578-8_13. http:\/\/link.springer.com\/10.1007\/978-0-387-35578-8_13, series Title: IFIP Advances in Information and Communication Technology","DOI":"10.1007\/978-0-387-35578-8_13"},{"key":"15_CR33","doi-asserted-by":"publisher","unstructured":"Su\u00e1rez Acevedo, E., Ferreira, T., Batz, K., B\u00f8ving, O., Foster, N., Silva, A.: Weighted NetKAT: a programming language for quantitative network verification. Proc. ACM Program. Lang. 10(PLDI) (2026). https:\/\/doi.org\/10.1145\/3808318","DOI":"10.1145\/3808318"},{"key":"15_CR34","doi-asserted-by":"publisher","unstructured":"Tabakov, D., Vardi, M.Y.: Experimental evaluation of classical automata constructions. In: Sutcliffe, G., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning, vol.\u00a03835, pp. 396\u2013411. Springer Berlin Heidelber. https:\/\/doi.org\/10.1007\/11591191_28. http:\/\/link.springer.com\/10.1007\/11591191_28, series Title: Lecture Notes in Computer Science","DOI":"10.1007\/11591191_28"},{"key":"15_CR35","doi-asserted-by":"publisher","unstructured":"Tappler, M., Aichernig, B.K., Lorber, F.: Timed automata learning via SMT solving. In: Deshmukh, J.V., Havelund, K., Perez, I. (eds.) NASA Formal Methods, vol. 13260, pp. 489\u2013507. Springer International Publishing. https:\/\/doi.org\/10.1007\/978-3-031-06773-0_26","DOI":"10.1007\/978-3-031-06773-0_26"},{"key":"15_CR36","doi-asserted-by":"publisher","unstructured":"Vaandrager, F.W.: Model learning. Commun. ACM 60, 86\u201395 (2017). https:\/\/doi.org\/10.1145\/2967606","DOI":"10.1145\/2967606"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-32526-6_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T08:44:28Z","timestamp":1784796268000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-32526-6_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032325259","9783032325266"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-32526-6_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"24 July 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","label":"Disclosure of Interests","group":{"name":"EthicsHeading","label":"Ethics"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Lisbon","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 July 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 July 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"38","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.floc26.org\/program","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}