# Quadratic Word Equations with Length Constraints, Counter Systems, and Presburger Arithmetic with Divisibility

• Anthony W. Lin
• Rupak Majumdar
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11138)

## Abstract

Word equations are a crucial element in the theoretical foundation of constraint solving over strings. A word equation relates two words over string variables and constants. Its solution amounts to a function mapping variables to constant strings that equate the left and right hand sides of the equation. While the problem of solving word equations is decidable, the decidability of the problem of solving a word equation with a length constraint (i.e., a constraint relating the lengths of words in the word equation) has remained a long-standing open problem. We focus on the subclass of quadratic word equations, i.e., in which each variable occurs at most twice. We first show that the length abstractions of solutions to quadratic word equations are in general not Presburger-definable. We then describe a class of counter systems with Presburger transition relations which capture the length abstraction of a quadratic word equation with regular constraints. We provide an encoding of the effect of a simple loop of the counter systems in the existential theory of Presburger Arithmetic with divisibility (PAD). Since PAD is decidable, we get a decision procedure for quadratic words equations with length constraints for which the associated counter system is flat (i.e., all nodes belong to at most one cycle). In particular, we show a decidability result (in fact, also an NP algorithm with a PAD oracle) for a recently proposed NP-complete fragment of word equations called regular-oriented word equations, when augmented with length constraints. Decidability holds when the constraints are extended with regular constraints with a 1-weak control structure.

## Notes

### Acknowledgment

We thank Jatin Arora, Dmitry Chistikov, Volker Diekert, Matthew Hague, Artur Jeż, Philipp Rümmer, and James Worrell for the helpful discussions. This research was partially funded by the ERC Starting Grant AV-SMP (grant agreement no. 759969) and the ERC Synergy Grant IMPACT (grant agreement no. 610150).

## References

1. 1.
Abdulla, P.A., Atig, M.F., Chen, Y.-F., Holík, L., Rezine, A., Rümmer, P., Stenman, J.: String constraints for verification. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 150–166. Springer, Cham (2014).
2. 2.
Babiak, T., Rehák, V., Strejcek, J.: Almost linear Büchi automata. Mathematical Structures in Computer Science 22(2), 203–235 (2012)
3. 3.
Bardin, S., Finkel, A., Leroux, J., Petrucci, L.: FAST: acceleration from theory to practice. STTT 10(5), 401–424 (2008)
4. 4.
Bardin, S., Finkel, A., Leroux, J., Schnoebelen, P.: Flat acceleration in symbolic model checking. In: Peled, D.A., Tsay, Y.-K. (eds.) ATVA 2005. LNCS, vol. 3707, pp. 474–488. Springer, Heidelberg (2005).
5. 5.
Berzish, M., Ganesh, V., Zheng, Y.: Z3str3: a string solver with theory-aware heuristics. In: FMCAD, pages 55–59. (2017)Google Scholar
6. 6.
Bjørner, N., Tillmann, N., Voronkov, A.: Path feasibility analysis for string-manipulating programs. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 307–321. Springer, Heidelberg (2009).
7. 7.
Bozga, M., Iosif, R., Lakhnech, Y.: Flat parametric counter automata. Fundam. Inform. 91(2), 275–303 (2009)
8. 8.
Chrobak, M.: Finite automata and unary languages. Theor. Comput. Sci. 47(3), 149–158 (1986)
9. 9.
Day, J.D., et al.: The Satisfiability of Extended Word Equations: The Boundary Between Decidability and Undecidability. CoRR, abs/1802.00523 (2018)Google Scholar
10. 10.
Day, J.D., Manea, F., Nowotka, D.: The hardness of solving simple word equations. In: MFCS, pp. 18:1–18:14 (2017)Google Scholar
11. 11.
Diekert, V.: Makanin’s algorithm. In: Lothaire, M.(ed.) Algebraic Combinatorics on Words, Volume 90 of Encyclopedia of Mathematics and its Applications, Chapter 12, pp. 387–442. Cambridge University Press, Cambridge (2002)Google Scholar
12. 12.
Diekert, V., Robson, J.M.: Quadratic word equations. In: Jewels are Forever, Contributions on Theoretical Computer Science in Honor of Arto Salomaa, pp. 314–326. (1999)
13. 13.
Ganesh, V., Minnes, M., Solar-Lezama, A., Rinard, M.: Word equations with length constraints: what’s decidable? In: Biere, A., Nahir, A., Vos, T. (eds.) HVC 2012. LNCS, vol. 7857, pp. 209–226. Springer, Heidelberg (2013).
14. 14.
Holík, L., Janku, P., Lin, A.W., Rümmer, P., Vojnar, T.: String constraints with concatenation and transducers solved efficiently. PACMPL, 2(POPL):4:1–4:32 (2018)
15. 15.
Jéz, A.: Recompression: a simple and powerful technique for word equations. In: STACS 2013, LIPIcs, vol. 20, pp. 233–244 (2013)Google Scholar
16. 16.
Kiezun, A.: HAMPI: A solver for word equations over strings, regular expressions, and context-free grammars. ACM Trans. Softw. Eng. Methodol. 21(4), 25 (2012)
17. 17.
Kretínský, M., Rehák, V., Strejcek, J.: Reachability is decidable for weakly extended process rewrite systems. Inf. Comput. 207(6), 671–680 (2009)
18. 18.
Lechner, A., Ouaknine, J., Worrell, J.: On the complexity of linear arithmetic with divisibility. In: LICS 15: Logic in Computer Science. IEEE (2015)Google Scholar
19. 19.
Lentin, A.: Equations dans les Monoides Libres. Gauthier-Villars, Paris (1972)
20. 20.
Leroux, J., Sutre, G.: Flat counter automata almost everywhere! In: Software Verification: Infinite-State Model Checking and Static Program Analysis, 19.02.2006–24.02.2006 (2006)Google Scholar
21. 21.
Liang, T., Reynolds, A., Tinelli, C., Barrett, C., Deters, M.: A DPLL(T) theory solver for a theory of strings and regular expressions. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 646–662. Springer, Cham (2014).
22. 22.
Lin, A.W., Barceló, P.: String solving with word equations and transducers: towards a logic for analysing mutation XSS. In: POPL, pp. 123–136 (2016)Google Scholar
23. 23.
Lipshitz, L.: The Diophantine problem for addition and divisibility. Trans. Am. Math. Soc. 235, 271–283 (1976)
24. 24.
Makanin, G.S.: The problem of solvability of equations in a free semigroup. Sb. Math. 32(2), 129–198 (1977)
25. 25.
Martinez, A.: Efficient computation of regular expressions from unary NFAs. In: DFCS, pp. 174–187 (2002)Google Scholar
26. 26.
Matiyasevich, Y.: A connection between systems of words-and-lengths equations and Hilbertc tenth problem. Zap. Nauchnykh Semin. POMI 8, 132–144 (1968)Google Scholar
27. 27.
Parikh, R.: On context-free languages. J. ACM 13(4), 570–581 (1966)
28. 28.
Saxena, P., Akhawe, D., Hanna, S., Mao, F., McCamant, S., Song, D., et al.: A symbolic execution framework for JavaScript. In: S&P, pp. 513–528 (2010)Google Scholar
29. 29.
To, A.W.: Unary finite automata vs. arithmetic progressions. Inf. Process. Lett. 109(17), 1010–1014 (2009)
30. 30.
To, A.W., Libkin, L.: Algorithmic metatheorems for decidable LTL model checking over infinite systems. In: Ong, L. (ed.) FoSSaCS 2010. LNCS, vol. 6014, pp. 221–236. Springer, Heidelberg (2010).
31. 31.
Trinh, M., Chu, D., Jaffar, J.: S3: a symbolic string solver for vulnerability detection in web applications. In: CCS, pp. 1232–1243. (2014)Google Scholar
32. 32.
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–260. Springer, Cham (2016).
33. 33.
Yu, F., Alkhalaf, M., Bultan, T., Ibarra, O.H.: Automata-based symbolic string analysis for vulnerability detection. Form. Methods Syst. Des. 44(1), 44–70 (2014)