{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,4]],"date-time":"2025-11-04T21:28:13Z","timestamp":1762291693979,"version":"build-2065373602"},"publisher-location":"Cham","reference-count":54,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032095237","type":"print"},{"value":"9783032095244","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,11,5]],"date-time":"2025-11-05T00:00:00Z","timestamp":1762300800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,11,5]],"date-time":"2025-11-05T00:00:00Z","timestamp":1762300800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-09524-4_4","type":"book-chapter","created":{"date-parts":[[2025,11,4]],"date-time":"2025-11-04T21:14:00Z","timestamp":1762290840000},"page":"51-67","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Word Equations with\u00a0Length Constraints via\u00a0Weak Arithmetics and\u00a0Matrix Reachability Problems"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3660-7766","authenticated-orcid":false,"given":"Joel D.","family":"Day","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-3346-5517","authenticated-orcid":false,"given":"Matthew","family":"Konefal","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,11,5]]},"reference":[{"key":"4_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1007\/978-3-319-08867-9_10","volume-title":"Computer Aided Verification","author":"PA Abdulla","year":"2014","unstructured":"Abdulla, P.A., et al.: String constraints for verification. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 150\u2013166. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_10"},{"key":"4_CR2","doi-asserted-by":"publisher","unstructured":"Albert, M.H., Lawrence, J.: A proof of Ehrenfeucht\u2019s conjecture. Theor. Comput. Sci. 41, 121\u2013123 (1985)https:\/\/doi.org\/10.1016\/0304-3975(85)90066-0","DOI":"10.1016\/0304-3975(85)90066-0"},{"key":"4_CR3","doi-asserted-by":"publisher","unstructured":"Amadini, R.: A survey on string constraint solving. ACM Comput. Surv. 55(2), 16:1\u201316:38 (2023). https:\/\/doi.org\/10.1145\/3484198","DOI":"10.1145\/3484198"},{"key":"4_CR4","unstructured":"Bel\u2019tyukov, A.P.: Decidability of the universal theory of natural numbers with addition and divisibility. Zapiski Nauchnykh Seminarov POMI 60, 15\u201328 (1976), https:\/\/www.mathnet.ru\/eng\/znsl2066"},{"key":"4_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1007\/978-3-030-81688-9_14","volume-title":"Computer Aided Verification","author":"M Berzish","year":"2021","unstructured":"Berzish, M., et al.: An SMT solver for regular expressions and linear arithmetic over string length. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12760, pp. 289\u2013312. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_14"},{"key":"4_CR6","doi-asserted-by":"publisher","unstructured":"B\u00fcchi, J.R., Senger, S.: Definability in the existential theory of concatenation and undecidable extensions of this theory. Math. Log. Q. 34(4), 337\u2013342 (1988). https:\/\/doi.org\/10.1002\/MALQ.19880340410","DOI":"10.1002\/MALQ.19880340410"},{"issue":"OOPSLA2","key":"4_CR7","doi-asserted-by":"publisher","first-page":"2112","DOI":"10.1145\/3622872","volume":"7","author":"Y Chen","year":"2023","unstructured":"Chen, Y., Chocholat\u00fd, D., Havlena, V., Hol\u00edk, L., Leng\u00e1l, O., S\u00edc, J.: Solving string constraints with lengths by stabilization. Proc. ACM Program. Lang. 7(OOPSLA2), 2112\u20132141 (2023). https:\/\/doi.org\/10.1145\/3622872","journal-title":"Proc. ACM Program. Lang."},{"key":"4_CR8","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1007\/978-3-642-59136-5_6","volume-title":"Handbook of Formal Languages","author":"C Choffrut","year":"1997","unstructured":"Choffrut, C., Karhum\u00e4ki, J.: Combinatorics of words. In: Rozenberg, G., Salomaa, A. (eds.) Handbook of Formal Languages, pp. 329\u2013438. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/978-3-642-59136-5_6"},{"key":"4_CR9","doi-asserted-by":"publisher","unstructured":"Christian, C.: Equations in words. In: Lothaire, M. (ed.) Combinatorics on Words, pp. 162\u2013183. Cambridge Mathematical Library, Cambridge University Press (1997). https:\/\/doi.org\/10.1017\/CBO9780511566097.012","DOI":"10.1017\/CBO9780511566097.012"},{"issue":"5","key":"4_CR10","doi-asserted-by":"publisher","first-page":"843","DOI":"10.1142\/S0218196716500363","volume":"26","author":"L Ciobanu","year":"2016","unstructured":"Ciobanu, L., Diekert, V., Elder, M.: Solution sets for equations over free groups are EDT0L languages. Int. J. Algebra Comput. 26(5), 843\u2013886 (2016). https:\/\/doi.org\/10.1142\/S0218196716500363","journal-title":"Int. J. Algebra Comput."},{"issue":"1","key":"4_CR11","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1137\/23M1604679","volume":"9","author":"L Ciobanu","year":"2025","unstructured":"Ciobanu, L., Evetts, A., Levine, A.: Effective equation solving, constraints, and growth in virtually abelian groups. SIAM J. Appl. Algebra Geom. 9(1), 235\u2013260 (2025). https:\/\/doi.org\/10.1137\/23M1604679","journal-title":"SIAM J. Appl. Algebra Geom."},{"key":"4_CR12","doi-asserted-by":"publisher","unstructured":"Ciobanu, L., Zetzsche, G.: Slice closures of indexed languages and word equations with counting constraints. In: Sobocinski, P., Lago, U.D., Esparza, J. (eds.) Proceedings of the 39th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2024, Tallinn, Estonia, 8\u201311 July 2024, pp. 25:1\u201325:12. ACM (2024). https:\/\/doi.org\/10.1145\/3661814.3662134","DOI":"10.1145\/3661814.3662134"},{"key":"4_CR13","doi-asserted-by":"publisher","unstructured":"Colcombet, T., Ouaknine, J., Semukhin, P., Worrell, J.: On reachability problems for low-dimensional matrix semigroups. In: Baier, C., Chatzigiannakis, I., Flocchini, P., Leonardi, S. (eds.) 46th International Colloquium on Automata, Languages, and Programming, ICALP 2019, July 9-12, 2019, Patras, Greece. LIPIcs, vol.\u00a0132, pp. 44:1\u201344:15. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2019). https:\/\/doi.org\/10.4230\/LIPICS.ICALP.2019.44","DOI":"10.4230\/LIPICS.ICALP.2019.44"},{"key":"4_CR14","doi-asserted-by":"publisher","unstructured":"Day, J.D., Ganesh, V., He, P., Manea, F., Nowotka, D.: The satisfiability of extended word equations: the boundary between decidability and undecidability. CoRR abs\/1802.00523 (2018). https:\/\/doi.org\/10.48550\/ARXIV.1802.00523","DOI":"10.48550\/ARXIV.1802.00523"},{"key":"4_CR15","doi-asserted-by":"publisher","unstructured":"Day, J.D., Manea, F.: On the structure of solution sets to regular word equations. In: Czumaj, A., Dawar, A., Merelli, E. (eds.) 47th International Colloquium on Automata, Languages, and Programming, ICALP 2020, July 8-11, 2020, Saarbr\u00fccken, Germany (Virtual Conference). LIPIcs, vol.\u00a0168, pp. 124:1\u2013124:16. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2020). https:\/\/doi.org\/10.4230\/LIPICS.ICALP.2020.124","DOI":"10.4230\/LIPICS.ICALP.2020.124"},{"key":"4_CR16","unstructured":"D\u2019Costa, J.R.: Reachability and escape problems in linear dynamical systems. PhD thesis, University of Oxford (2024)"},{"key":"4_CR17","doi-asserted-by":"publisher","unstructured":"Diekert, V., Robson, J.M.: Quadratic word equations, pp. 314\u2013326. Springer, Berlin, Heidelberg (1999). https:\/\/doi.org\/10.1007\/978-3-642-60207-8_28","DOI":"10.1007\/978-3-642-60207-8_28"},{"key":"4_CR18","doi-asserted-by":"publisher","unstructured":"Dong, R.: Recent advances in algorithmic problems for semigroups. ACM SIGLOG News 10(4), 3\u201323 (2023). https:\/\/doi.org\/10.1145\/3636362.3636365","DOI":"10.1145\/3636362.3636365"},{"key":"4_CR19","doi-asserted-by":"publisher","unstructured":"Draghici, A., Haase, C., Manea, F.: Sem\u00ebnov arithmetic, affine VASS, and string constraints. In: Beyersdorff, O., Kant\u00e9, M.M., Kupferman, O., Lokshtanov, D. (eds.) 41st International Symposium on Theoretical Aspects of Computer Science, STACS 2024, 12\u201314 March 2024, Clermont-Ferrand, France. LIPIcs, vol.\u00a0289, pp. 29:1\u201329:19. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2024). https:\/\/doi.org\/10.4230\/LIPICS.STACS.2024.29","DOI":"10.4230\/LIPICS.STACS.2024.29"},{"issue":"3","key":"4_CR20","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1016\/0304-3975(90)90050-R","volume":"71","author":"S Dulucq","year":"1990","unstructured":"Dulucq, S., Gouyou-Beauchamps, D.: Sur les facteurs des suites de Sturm. Theoret. Comput. Sci. 71(3), 381\u2013400 (1990). https:\/\/doi.org\/10.1016\/0304-3975(90)90050-R","journal-title":"Theoret. Comput. Sci."},{"key":"4_CR21","doi-asserted-by":"publisher","unstructured":"Figueira, D., Je\u017c, A., Lin, A.W.: Data path queries over embedded graph databases. In: Libkin, L., Barcel\u00f3, P. (eds.) PODS 2022: International Conference on Management of Data, Philadelphia, PA, USA, 12\u201317 June 2022, pp. 189\u2013201. ACM (2022). https:\/\/doi.org\/10.1145\/3517804.3524159","DOI":"10.1145\/3517804.3524159"},{"key":"4_CR22","doi-asserted-by":"publisher","unstructured":"Freydenberger, D.D., Peterfreund, L.: The theory of concatenation over finite models. In: Bansal, N., Merelli, E., Worrell, J. (eds.) 48th International Colloquium on Automata, Languages, and Programming, ICALP 2021, 12\u201316 July 2021, Glasgow, Scotland (Virtual Conference). LIPIcs, vol.\u00a0198, pp. 130:1\u2013130:17. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2021). https:\/\/doi.org\/10.4230\/LIPICS.ICALP.2021.130","DOI":"10.4230\/LIPICS.ICALP.2021.130"},{"key":"4_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/978-3-642-39611-3_21","volume-title":"Hardware and Software: Verification and Testing","author":"V Ganesh","year":"2013","unstructured":"Ganesh, V., Minnes, M., Solar-Lezama, A., Rinard, M.: Word equations with length constraints: what\u2019s decidable? In: Biere, A., Nahir, A., Vos, T. (eds.) HVC 2012. LNCS, vol. 7857, pp. 209\u2013226. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39611-3_21"},{"key":"4_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"310","DOI":"10.1007\/978-3-030-71995-1_16","volume-title":"Foundations of Software Science and Computation Structures","author":"C Haase","year":"2021","unstructured":"Haase, C., R\u00f3\u017cycki, J.: On the expressiveness of B\u00fcchi arithmetic. In: FOSSACS 2021. LNCS, vol. 12650, pp. 310\u2013323. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-71995-1_16"},{"key":"4_CR25","doi-asserted-by":"publisher","first-page":"439","DOI":"10.1007\/978-3-642-59136-5_7","volume-title":"Handbook of Formal Languages","author":"T Harju","year":"1997","unstructured":"Harju, T., Karhum\u00e4ki, J.: Morphisms. In: Rozenberg, G., Salomaa, A. (eds.) Handbook of Formal Languages, pp. 439\u2013510. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/978-3-642-59136-5_7"},{"key":"4_CR26","doi-asserted-by":"publisher","unstructured":"Havlena, V., Hol\u00edk, L., Leng\u00e1l, O., S\u00ed\u010d, J.: Cooking string-integer conversions with noodles. In: Chakraborty, S., Jiang, J.R. (eds.) 27th International Conference on Theory and Applications of Satisfiability Testing, SAT 2024, 21\u201324 August 2024, Pune, India. LIPIcs, vol.\u00a0305, pp. 14:1\u201314:19. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2024). https:\/\/doi.org\/10.4230\/LIPICS.SAT.2024.14","DOI":"10.4230\/LIPICS.SAT.2024.14"},{"key":"4_CR27","unstructured":"Hmelevskii, J.I., Kandall, G.A.: Equations in free semigroups. In: Proceedings of the Steklov Institute of Mathematics ; no. 107 (1971), AMS, Providence, Rhode Island (1976), https:\/\/www.mathnet.ru\/eng\/tm2975"},{"issue":"1\u20132","key":"4_CR28","doi-asserted-by":"publisher","first-page":"109","DOI":"10.3233\/FI-1999-381209","volume":"38","author":"L Ilie","year":"1999","unstructured":"Ilie, L.: Subwords and power-free words are not expressible by word equations. Fundam. Informaticae 38(1\u20132), 109\u2013118 (1999). https:\/\/doi.org\/10.3233\/FI-1999-381209","journal-title":"Fundam. Informaticae"},{"key":"4_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/3-540-46541-3_10","volume-title":"STACS 2000","author":"L Ilie","year":"2000","unstructured":"Ilie, L., Plandowski, W.: Two-variable word equations. In: Reichel, H., Tison, S. (eds.) STACS 2000. LNCS, vol. 1770, pp. 122\u2013132. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-46541-3_10"},{"key":"4_CR30","doi-asserted-by":"publisher","unstructured":"Je\u017c, A.: Recompression: a simple and powerful technique for word equations. In: Portier, N., Wilke, T. (eds.) 30th International Symposium on Theoretical Aspects of Computer Science, STACS 2013, February 27 - March 2, 2013, Kiel, Germany. LIPIcs, vol.\u00a020, pp. 233\u2013244. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2013). https:\/\/doi.org\/10.4230\/LIPICS.STACS.2013.233","DOI":"10.4230\/LIPICS.STACS.2013.233"},{"issue":"3","key":"4_CR31","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1145\/337244.337255","volume":"47","author":"J Karhum\u00e4ki","year":"2000","unstructured":"Karhum\u00e4ki, J., Mignosi, F., Plandowski, W.: The expressibility of languages and relations by word equations. J. ACM 47(3), 483\u2013505 (2000). https:\/\/doi.org\/10.1145\/337244.337255","journal-title":"J. ACM"},{"issue":"2","key":"4_CR32","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1142\/S0129054111008088","volume":"22","author":"M Laine","year":"2011","unstructured":"Laine, M., Plandowski, W.: Word equations with one unknown. Int. J. Found. Comput. Sci. 22(2), 345\u2013375 (2011). https:\/\/doi.org\/10.1142\/S0129054111008088","journal-title":"Int. J. Found. Comput. Sci."},{"key":"4_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"350","DOI":"10.1007\/978-3-030-02768-1_19","volume-title":"Programming Languages and Systems","author":"QL Le","year":"2018","unstructured":"Le, Q.L., He, M.: A decision procedure for string logic with quadratic equations, regular expressions and length constraints. In: Ryu, S. (ed.) APLAS 2018. LNCS, vol. 11275, pp. 350\u2013372. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-02768-1_19"},{"key":"4_CR34","doi-asserted-by":"publisher","unstructured":"Lechner, A., Ouaknine, J., Worrell, J.: On the complexity of linear arithmetic with divisibility. In: 2015 30th Annual ACM\/IEEE Symposium on Logic in Computer Science, pp. 667\u2013676 (2015). https:\/\/doi.org\/10.1109\/LICS.2015.67","DOI":"10.1109\/LICS.2015.67"},{"key":"4_CR35","doi-asserted-by":"publisher","unstructured":"Lin, A.W., Majumdar, R.: Quadratic word equations with length constraints, counter systems, and Presburger arithmetic with divisibility. Log. Methods Comput. Sci. 17(4) (2021). https:\/\/doi.org\/10.46298\/LMCS-17(4:4)2021","DOI":"10.46298\/LMCS-17(4:4)2021"},{"key":"4_CR36","doi-asserted-by":"publisher","unstructured":"Lin, A.W., Barcel\u00f3, P.: String solving with word equations and transducers: towards a logic for analysing mutation XSS. In: Bod\u00edk, R., Majumdar, R. (eds.) Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016. pp. 123\u2013136. ACM (2016). https:\/\/doi.org\/10.1145\/2837614.2837641","DOI":"10.1145\/2837614.2837641"},{"key":"4_CR37","doi-asserted-by":"publisher","unstructured":"Lipshitz, L.: The diophantine problem for addition and divisibility. Trans. Am. Math. Soc. 235, 271\u2013283 (1978). https:\/\/doi.org\/10.1090\/S0002-9947-1978-0469886-1","DOI":"10.1090\/S0002-9947-1978-0469886-1"},{"issue":"1","key":"4_CR38","first-page":"41","volume":"33","author":"L Lipshitz","year":"1981","unstructured":"Lipshitz, L.: Some remarks on the Diophantine problem for addition and divisibility. Bull. Soc. Math. Belg. S\u00e9r. B 33(1), 41\u201352 (1981)","journal-title":"Bull. Soc. Math. Belg. S\u00e9r. B"},{"key":"4_CR39","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1070\/SM1977v032n02ABEH002376","volume":"32","author":"GS Makanin","year":"1977","unstructured":"Makanin, G.S.: The problem of solvability of equations in a free semigroup. Math. USSR-Sbornik 32, 129\u2013198 (1977). https:\/\/doi.org\/10.1070\/SM1977v032n02ABEH002376","journal-title":"Math. USSR-Sbornik"},{"issue":"3","key":"4_CR40","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1070\/IM1983v021n03ABEH001803","volume":"21","author":"GS Makanin","year":"1983","unstructured":"Makanin, G.S.: Equations in a free group. Math. USSR-Izvestiya 21(3), 483\u2013546 (1983). https:\/\/doi.org\/10.1070\/IM1983v021n03ABEH001803","journal-title":"Math. USSR-Izvestiya"},{"key":"4_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/978-3-662-53132-7_25","volume-title":"Developments in Language Theory","author":"F Manea","year":"2016","unstructured":"Manea, F., Nowotka, D., Schmid, M.L.: On the solvability problem for restricted classes of word equations. In: Brlek, S., Reutenauer, C. (eds.) DLT 2016. LNCS, vol. 9840, pp. 306\u2013318. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-53132-7_25"},{"key":"4_CR42","unstructured":"Matiyasevich, Y.V.: A connection between systems of words-and-lengths equations and Hilbert\u2019s tenth problem. Zapiski Nauchnykh Seminarov POMI 8, 132\u2013144 (1968), https:\/\/www.mathnet.ru\/eng\/znsl2256"},{"key":"4_CR43","doi-asserted-by":"publisher","unstructured":"Matiyasevich, Y.V.: Enumerable sets are Diophantine. In: Soviet Math. Dokl. vol.\u00a011, pp. 354\u2013358 (1970). https:\/\/doi.org\/10.1142\/9789812564894_0013","DOI":"10.1142\/9789812564894_0013"},{"key":"4_CR44","doi-asserted-by":"publisher","unstructured":"Perrin, D.: Words. In: Lothaire, M. (ed.) Combinatorics on Words, pp. 1\u201317. Cambridge Mathematical Library, Cambridge University Press (1997). https:\/\/doi.org\/10.1017\/CBO9780511566097.004","DOI":"10.1017\/CBO9780511566097.004"},{"key":"4_CR45","doi-asserted-by":"publisher","unstructured":"Plandowski, W.: An efficient algorithm for solving word equations. In: Kleinberg, J.M. (ed.) Proceedings of the 38th Annual ACM Symposium on Theory of Computing, Seattle, WA, USA, 21\u201323 May 2006, pp. 467\u2013476. ACM (2006). https:\/\/doi.org\/10.1145\/1132516.1132584","DOI":"10.1145\/1132516.1132584"},{"key":"4_CR46","doi-asserted-by":"publisher","unstructured":"Plandowski, W., Rytter, W.: Application of Lempel-Ziv encodings to the solution of words equations. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) Automata, Languages and Programming, 25th International Colloquium, ICALP 1998, Aalborg, Denmark, 13\u201317 July 1998, Proceedings. LNCS, vol.\u00a01443, pp. 731\u2013742. Springer (1998). https:\/\/doi.org\/10.1007\/BFB0055097","DOI":"10.1007\/BFB0055097"},{"key":"4_CR47","doi-asserted-by":"publisher","unstructured":"Potapov, I., Semukhin, P.: Vector and scalar reachability problems in $$\\text{SL(2,}\\mathbb{Z}\\text{) }$$. J. Comput. Syst. Sci. 100, 30\u201343 (2019). https:\/\/doi.org\/10.1016\/j.jcss.2018.09.003","DOI":"10.1016\/j.jcss.2018.09.003"},{"key":"4_CR48","unstructured":"Presburger, M.: \u00dcber die Vollst\u00e4ndigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchen die Addition als einzige Operation hervortritt. (On the completeness of a certain system of arithmetic of whole numbers in which addition occurs as the only operation). In: Comptes-Rendus du ler Congres des Mathematiciens des Pays Slavs (1929)"},{"issue":"2","key":"4_CR49","doi-asserted-by":"publisher","first-page":"98","DOI":"10.2307\/2266510","volume":"14","author":"J Robinson","year":"1949","unstructured":"Robinson, J.: Definability and decision problems in arithmetic. J. Symb. Log. 14(2), 98\u2013114 (1949). https:\/\/doi.org\/10.2307\/2266510","journal-title":"J. Symb. Log."},{"key":"4_CR50","doi-asserted-by":"publisher","unstructured":"Samimi, H., Sch\u00e4fer, M., Artzi, S., Millstein, T.D., Tip, F., Hendren, L.J.: Automated repair of HTML generation errors in PHP applications using string constraint solving. In: Glinz, M., Murphy, G.C., Pezz\u00e8, M. (eds.) 34th International Conference on Software Engineering, ICSE 2012, 2\u20139 June 2012, Zurich, Switzerland, pp. 277\u2013287. IEEE Computer Society (2012). https:\/\/doi.org\/10.1109\/ICSE.2012.6227186","DOI":"10.1109\/ICSE.2012.6227186"},{"key":"4_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/3-540-55124-7_4","volume-title":"Word Equations and Related Topics","author":"KU Schulz","year":"1992","unstructured":"Schulz, K.U.: Makanin\u2019s algorithm for word equations - two improvements and a generalization. In: Schulz, K.U. (ed.) IWWERT 1990. LNCS, vol. 572, pp. 85\u2013150. Springer, Heidelberg (1992). https:\/\/doi.org\/10.1007\/3-540-55124-7_4"},{"key":"4_CR52","unstructured":"Theys, J.: Joint spectral radius: theory and approximations. PhD thesis, Universit\u00e9 catholique de Louvain (2005)"},{"issue":"1","key":"4_CR53","doi-asserted-by":"publisher","first-page":"157","DOI":"10.2140\/pjm.2004.213.157","volume":"213","author":"C Weinbaum","year":"2004","unstructured":"Weinbaum, C.: Word equation $$ABC=CDA$$, $$B\\ne D$$. Pac. J. Math. 213(1), 157\u2013162 (2004). https:\/\/doi.org\/10.2140\/pjm.2004.213.157","journal-title":"Pac. J. Math."},{"issue":"2\u20133","key":"4_CR54","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/S10703-016-0263-6","volume":"50","author":"Y Zheng","year":"2017","unstructured":"Zheng, Y., et al.: Z3str2: an efficient solver for strings, regular expressions, and length constraints. Formal Methods Syst. Des. 50(2\u20133), 249\u2013288 (2017). https:\/\/doi.org\/10.1007\/S10703-016-0263-6","journal-title":"Formal Methods Syst. Des."}],"container-title":["Lecture Notes in Computer Science","Reachability Problems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-09524-4_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,4]],"date-time":"2025-11-04T21:14:04Z","timestamp":1762290844000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-09524-4_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,5]]},"ISBN":["9783032095237","9783032095244"],"references-count":54,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-09524-4_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,11,5]]},"assertion":[{"value":"5 November 2025","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","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"RP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Reachability Problems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Madrid","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Spain","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 October 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 October 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"rp2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/rp25.software.imdea.org\/index.html","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}