{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T15:33:16Z","timestamp":1759332796298,"version":"build-2065373602"},"reference-count":36,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2025,5,20]],"date-time":"2025-05-20T00:00:00Z","timestamp":1747699200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,5,20]],"date-time":"2025-05-20T00:00:00Z","timestamp":1747699200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100006260","name":"Technion - Israel Institute of Technology","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100006260","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2025,9]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Automated reasoning about systems with infinite domains requires an extension of automata, and in particular, finite-word automata, to <jats:italic>infinite alphabets<\/jats:italic>. We introduce and study <jats:italic>variable finite automata over infinite alphabets<\/jats:italic> (VFAs). VFAs form a natural and simple extension of regular automata, in which the alphabet consists of letters as well as variables that range over the infinite alphabet domain. Thus, VFAs have the same structure as finite automata, except that some of the transitions are labeled by variables. We compare VFAs with existing formalisms, and study their closure properties and classical decision problems. We further identify and study the <jats:italic>deterministic<\/jats:italic> fragment of VFAs (DVFAs). We show that while DVFAs are sufficiently strong to express many interesting properties, they are closed under the Boolean operations, and their nonemptiness and containment problems are decidable. We describe a determinization process for a determinizable subset of VFAs. Moreover, we show that DVFAs have a canonical form, making them a particularly robust model that is easy to reason about and work with. Building on these results, we construct an efficient active learning algorithm for DVFAs, based on the <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$L^*$$<\/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>\u2217<\/mml:mo>\n                  <\/mml:msup>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula> learning algorithm for regular languages.<\/jats:p>","DOI":"10.1007\/s10703-025-00472-7","type":"journal-article","created":{"date-parts":[[2025,5,20]],"date-time":"2025-05-20T11:20:41Z","timestamp":1747740041000},"page":"376-418","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Variable automata over infinite alphabets"],"prefix":"10.1007","volume":"66","author":[{"given":"Orna","family":"Grumberg","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Orna","family":"Kupferman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0524-7390","authenticated-orcid":false,"given":"Sarai","family":"Sheinvald","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,5,20]]},"reference":[{"issue":"2","key":"472_CR1","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/0890-5401(87)90052-6","volume":"75","author":"Dana Angluin","year":"1987","unstructured":"Angluin Dana (1987) Learning regular sets from queries and counterexamples. Information and Computation 75(2):87\u2013106","journal-title":"Information and Computation"},{"key":"472_CR2","doi-asserted-by":"crossref","unstructured":"George Argyros and Loris D\u2019Antoni. The learnability of symbolic automata. In Proc. 30th Int. Conf. on Computer Aided Verification, pages 427\u2013445, 2018","DOI":"10.1007\/978-3-319-96145-3_23"},{"key":"472_CR3","doi-asserted-by":"crossref","unstructured":"George Argyros, Ioannis Stais, Aggelos Kiayias, and Angelos\u00a0D. Keromytis. Back in black: Towards formal, black box analysis of sanitizers and filters. In IEEE Symposium on Security and Privacy, pages 91\u2013109, 2016","DOI":"10.1109\/SP.2016.14"},{"key":"472_CR4","doi-asserted-by":"crossref","unstructured":"M. Bojanczyk, L. Braud, B. Klin, and S. Lasota. Towards nominal computation. In Proc. 39th ACM Symp. on Principles of Programming Languages, pages 401\u2013412. ACM, 2012","DOI":"10.1145\/2103656.2103704"},{"key":"472_CR5","doi-asserted-by":"crossref","unstructured":"M. Bojanczyk, B. Klin, and S. Lasota. Automata theory in nominal sets. Logical Methods in Computer Science, 10(3), 2014","DOI":"10.2168\/LMCS-10(3:4)2014"},{"issue":"3","key":"472_CR6","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1516512.1516515","volume":"56","author":"Mikoaj Boja\u0144czyk","year":"2009","unstructured":"Boja\u0144czyk Mikoaj, Muscholl Anca, Schwentick Thomas, Segoufin Luc (2009) Two-variable logic on data trees and xml reasoning. Journal of the ACM 56(3):1\u201348","journal-title":"Journal of the ACM"},{"key":"472_CR7","doi-asserted-by":"crossref","unstructured":"Mikolaj Bojanczyk, Anca Muscholl, Thomas Schwentick, Luc Segoufin, and Claire David. Two-variable logic on words with data. In Proc. 21st IEEE Symp. on Logic in Computer Science, pages 7\u201316, 2006","DOI":"10.1109\/LICS.2006.51"},{"key":"472_CR8","first-page":"4","volume":"10","author":"Benedikt Bollig","year":"2014","unstructured":"Bollig Benedikt, Habermehl Peter, Leucker Martin, Monmege Benjamin (2014) A robust class of data languages and an application to learning. Logical Methods in Computer Science 10:4\u201319","journal-title":"Logical Methods in Computer Science"},{"key":"472_CR9","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1016\/S0304-3975(02)00397-3","volume":"295","author":"A Bouajjani","year":"2003","unstructured":"Bouajjani A, Habermehl P, Mayr R (2003) Automatic verification of recursive procedures with one integer parameter. Theoretical Computer Science 295:85\u2013106","journal-title":"Theoretical Computer Science"},{"key":"472_CR10","doi-asserted-by":"crossref","unstructured":"Ahmed Bouajjani, Peter Habermehl, Yan Jurski, and Mihaela Sighireanu. Rewriting systems with data. In Proc. 16th Int. Symp. on Fundamentals of Computation Theory, pages 1\u201322, 2007","DOI":"10.1007\/978-3-540-74240-1_1"},{"issue":"2","key":"472_CR11","first-page":"163","volume":"1","author":"Marco Brambilla","year":"2003","unstructured":"Brambilla Marco, Ceri Stefano, Comai Sara, Fraternali Piero, Manolescu Ioana (2003) Specification and design of workflow-driven hypertexts. Journal of Web Engineering 1(2):163\u2013182","journal-title":"Journal of Web Engineering"},{"key":"472_CR12","unstructured":"J.: B\u00fcchi. On a decision method in restricted second order arithmetic. In Int. Congress on Logic, Method, and Philosophy of Science, pages 1\u201312. Stanford University Press, 1962"},{"key":"472_CR13","volume-title":"Designing Data-Intensive Web Applications","author":"Stefano Ceri","year":"2002","unstructured":"Ceri Stefano, Fraternali Piero, Bongio Aldo, Brambilla Marco, Comai Sara, Matera Maristella (2002) Designing Data-Intensive Web Applications. Morgan Kaufmann Publishers Inc., San Francisco, CA, USA"},{"key":"472_CR14","doi-asserted-by":"crossref","unstructured":"Loris D\u2019Antoni, Tiago Ferreira, Matteo Sammartino, and Alexandra Silva. Symbolic register automata. In Proc. 31st Int. Conf. on Computer Aided Verification, pages 3\u201319, Cham, 2019","DOI":"10.1007\/978-3-030-25540-4_1"},{"key":"472_CR15","doi-asserted-by":"crossref","unstructured":"S. Demri, R. Lazic, and D.: Nowak. On the freeze quantifier in constraint ltl: Decidability and complexity. Information and Computation, 07:2\u201324, 2007","DOI":"10.1016\/j.ic.2006.08.003"},{"key":"472_CR16","doi-asserted-by":"crossref","unstructured":"Samuel Drews and Loris D\u2019Antoni. Learning symbolic automata. In Proc. 23d Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, pages 173\u2013189, 2017","DOI":"10.1007\/978-3-662-54577-5_10"},{"issue":"2","key":"472_CR17","first-page":"1","volume":"19","author":"Dana Fisman","year":"2023","unstructured":"Fisman Dana, Frenkel Hadar, Zilles Sandra (2023) Inferring symbolic automata. Logical Methods in Computer Science 19(2):1\u201337","journal-title":"Logical Methods in Computer Science"},{"key":"472_CR18","doi-asserted-by":"crossref","unstructured":"Hadar Frenkel, Orna Grumberg, Corina\u00a0S. Pasareanu, and Sarai Sheinvald. Assume, guarantee or repair. In Armin Biere and David Parker, editors, Proc. 26th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, pages 211\u2013227. Springer, 2020","DOI":"10.1007\/978-3-030-45190-5_12"},{"issue":"3\u20135","key":"472_CR19","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/s001650200016","volume":"13","author":"M Gabbay","year":"2002","unstructured":"Gabbay M, Pitts AM (2002) A new approach to abstract syntax with variable binding. Formal Aspects of Computing 13(3\u20135):341\u2013363","journal-title":"Formal Aspects of Computing"},{"key":"472_CR20","doi-asserted-by":"crossref","unstructured":"Orna Grumberg, Orna Kupferman, and Sarai Sheinvald. Variable automata over infinite alphabets. In Proc. 4th Int. Conf. on Language and Automata Theory and Applications, LNCS, pages 561\u2013572. Springer, 2010","DOI":"10.1007\/978-3-642-13089-2_47"},{"key":"472_CR21","doi-asserted-by":"crossref","unstructured":"Pieter Hooimeijer and Margus Veanes. An evaluation of automata algorithms for string analysis. In Proc. 12th Int. Conf. on Verification, Model Checking, and Abstract Interpretation, page 248-262. Springer-Verlag, 2011","DOI":"10.1007\/978-3-642-18275-4_18"},{"issue":"2","key":"472_CR22","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1016\/0304-3975(94)90242-9","volume":"134","author":"Michael Kaminski","year":"1994","unstructured":"Kaminski Michael, Francez Nissim (1994) Finite-memory automata. Theoretical Computer Science 134(2):329\u2013363","journal-title":"Theoretical Computer Science"},{"key":"472_CR23","doi-asserted-by":"publisher","first-page":"741","DOI":"10.1142\/S0129054110007532","volume":"21","author":"Michael Kaminski","year":"2010","unstructured":"Kaminski Michael, Zeitlin Daniel (2010) Finite-memory automata with non-deterministic reassignment. International Journal of Foundations of Computer Science 21:741\u2013760","journal-title":"International Journal of Foundations of Computer Science"},{"key":"472_CR24","doi-asserted-by":"crossref","unstructured":"Maler Oded, Mens Irini-Eleftheria (2017) A Generic Algorithm for Learning Symbolic Automata from Membership Queries. Springer International Publishing","DOI":"10.1007\/978-3-319-63121-9_8"},{"key":"472_CR25","doi-asserted-by":"crossref","unstructured":"Nicolas Markey and Ph. Schnoebelen. Model checking a path. In Proc. 14th Int. Conf. on Concurrency Theory, pages 248\u2013262, 2003","DOI":"10.1007\/978-3-540-45187-7_17"},{"key":"472_CR26","doi-asserted-by":"crossref","unstructured":"J. Moerman, M. Sammartino, A. Silva, B. Klin, and M. Szynwelski. Learning nominal automata. In Proc. 44th ACM Symp. on Principles of Programming Languages, pages 613\u2013625. ACM, 2017","DOI":"10.1145\/3009837.3009879"},{"issue":"1","key":"472_CR27","first-page":"1","volume":"18","author":"Joshua Moerman","year":"2022","unstructured":"Moerman Joshua, Sammartino Matteo (2022) Residuality and learning for nondeterministic nominal automata. Logical Methods in Computer Science 18(1):1\u201329","journal-title":"Logical Methods in Computer Science"},{"key":"472_CR28","doi-asserted-by":"crossref","unstructured":"Frank Neven, Thomas Schwentick, and Victor Vianu. Towards regular languages over infinite alphabets. In Proc. 26th Int. Symp. on Mathematical Foundations of Computer Science, pages 560\u2013572. Springer-Verlag, 2001","DOI":"10.1007\/3-540-44683-4_49"},{"issue":"3","key":"472_CR29","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/s10703-008-0049-6","volume":"32","author":"Corina S Pasareanu","year":"2008","unstructured":"Pasareanu Corina S, Giannakopoulou Dimitra, Bobaru Mihaela Gheorghiu, Cobleigh Jamieson M, Barringer Howard (2008) Learning to divide and conquer: applying the L* algorithm to automate assume-guarantee reasoning. Formal Methods in System Design 32(3):175\u2013205","journal-title":"Formal Methods in System Design"},{"key":"472_CR30","doi-asserted-by":"crossref","unstructured":"Sarai Sheinvald. Learning deterministic variable automata over infinite alphabets. In International Symposium on Formal Methods, volume 11800 of Lecture Notes in Computer Science, pages 633\u2013650. Springer, 2019","DOI":"10.1007\/978-3-030-30942-8_37"},{"key":"472_CR31","doi-asserted-by":"publisher","first-page":"192","DOI":"10.1006\/inco.1994.1085","volume":"114","author":"Y Shemesh","year":"1994","unstructured":"Shemesh Y, Francez N (1994) Finite-state unification automata and relational languages. Information and Computation 114:192\u2013213","journal-title":"Information and Computation"},{"key":"472_CR32","doi-asserted-by":"crossref","unstructured":"Tony: Tan. Pebble Automata for Data Languages: Separation, Decidability, and Undecidability. PhD thesis, Technion - Computer Science Department, 2009","DOI":"10.1007\/978-3-642-03816-7_60"},{"key":"472_CR33","doi-asserted-by":"crossref","unstructured":"Margus Veanes and Nikolaj Bj\u00f8rner. Symbolic automata: The toolkit. In Cormac Flanagan and Barbara K\u00f6nig, editors, Proc. 18th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, pages 472\u2013477. Springer Berlin Heidelberg, 2012","DOI":"10.1007\/978-3-642-28756-5_33"},{"key":"472_CR34","doi-asserted-by":"crossref","unstructured":"Margus Veanes, Peli de\u00a0Halleux, and Nikolai Tillmann. Rex: Symbolic regular expression explorer. In Proc. 3d International Conference on Software Testing, Verification and Validation, pages 498\u2013507, 2010","DOI":"10.1109\/ICST.2010.15"},{"key":"472_CR35","doi-asserted-by":"crossref","unstructured":"Victor Vianu. Automatic verification of database-driven systems: a new frontier. In Proc. 12th International Conference on Database Theory, pages 1\u201313. ACM, 2009","DOI":"10.1145\/1514894.1514896"},{"key":"472_CR36","doi-asserted-by":"crossref","unstructured":"F. Yu, M. Alkhalaf, and T. Bultan. Stranger: An automata-based string analysis tool for PHP. In Proc. 16th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, volume 6015 of Lecture Notes in Computer Science, pages 154\u2013157. Springer, 2010","DOI":"10.1007\/978-3-642-12002-2_13"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-025-00472-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-025-00472-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-025-00472-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,30]],"date-time":"2025-09-30T15:26:33Z","timestamp":1759245993000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-025-00472-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,5,20]]},"references-count":36,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2025,9]]}},"alternative-id":["472"],"URL":"https:\/\/doi.org\/10.1007\/s10703-025-00472-7","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2025,5,20]]},"assertion":[{"value":"11 March 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"28 February 2025","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"20 May 2025","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}