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

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


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.



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).


  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). Scholar
  2. 2.
    Babiak, T., Rehák, V., Strejcek, J.: Almost linear Büchi automata. Mathematical Structures in Computer Science 22(2), 203–235 (2012)MathSciNetCrossRefGoogle Scholar
  3. 3.
    Bardin, S., Finkel, A., Leroux, J., Petrucci, L.: FAST: acceleration from theory to practice. STTT 10(5), 401–424 (2008)CrossRefGoogle Scholar
  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). Scholar
  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). Scholar
  7. 7.
    Bozga, M., Iosif, R., Lakhnech, Y.: Flat parametric counter automata. Fundam. Inform. 91(2), 275–303 (2009)MathSciNetzbMATHGoogle Scholar
  8. 8.
    Chrobak, M.: Finite automata and unary languages. Theor. Comput. Sci. 47(3), 149–158 (1986)MathSciNetCrossRefGoogle Scholar
  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)CrossRefGoogle Scholar
  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). Scholar
  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)CrossRefGoogle Scholar
  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)CrossRefGoogle Scholar
  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)MathSciNetCrossRefGoogle Scholar
  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)CrossRefGoogle Scholar
  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). Scholar
  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)MathSciNetCrossRefGoogle Scholar
  24. 24.
    Makanin, G.S.: The problem of solvability of equations in a free semigroup. Sb. Math. 32(2), 129–198 (1977)MathSciNetCrossRefGoogle Scholar
  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)CrossRefGoogle Scholar
  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)MathSciNetCrossRefGoogle Scholar
  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). Scholar
  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). Scholar
  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)CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.Oxford UniversityOxfordUK
  2. 2.Max Planck Institute for Software SystemsKaiserslauternGermany

Personalised recommendations