Document Open Access Logo

Satisfiability of Context-Free String Constraints with Subword-Ordering and Transducers

Authors C. Aiswarya , Soumodev Mal , Prakash Saivasan

PDF
Thumbnail PDF

File

LIPIcs.STACS.2024.5.pdf
  • Filesize: 0.95 MB
  • 20 pages

Document Identifiers

Author Details

C. Aiswarya
  • Chennai Mathematical Institute, India
  • CNRS, ReLaX, IRL 2000, Chennai, India
Soumodev Mal
  • Chennai Mathematical Institute, India
Prakash Saivasan
  • The Institute of Mathematical Sciences, HBNI, Chennai, India
  • CNRS, ReLaX, IRL 2000, Chennai, India

Funding

  • Saivasan, Prakash: MATRICS GRANT (MTR/2022/000312).

Acknowledgements

We thank Paul Gastin for helpful discussions.

Cite AsGet BibTex

C. Aiswarya, Soumodev Mal, and Prakash Saivasan. Satisfiability of Context-Free String Constraints with Subword-Ordering and Transducers. In 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 289, pp. 5:1-5:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.STACS.2024.5

Abstract

We study the satisfiability of string constraints where context-free membership constraints may be imposed on variables. Additionally a variable may be constrained to be a subword of a word obtained by shuffling variables and their transductions. The satisfiability problem is known to be undecidable even without rational transductions. It is known to be NExptime-complete without transductions, if the subword relations between variables do not have a cyclic dependency between them. We show that the satisfiability problem stays decidable in this fragment even when rational transductions are added. It is 2NExptime-complete with context-free membership, and NExptime-complete with only regular membership. For the lower bound we prove a technical lemma that is of independent interest: The length of the shortest word in the intersection of a pushdown automaton (of size 𝒪(n)) and n finite-state automata (each of size 𝒪(n)) can be double exponential in n.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • satisfiability
  • subword
  • string constraints
  • context-free
  • transducers

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. A. Parosh Abdulla, F. Mohamed Atig, Yu-Fang Chen, Diep Phi Bui, Lukáš Holík, Ahmed Rezine, and Philipp Rummer. Trau : SMT solver for string constraints. In Proceedings of the 18th Conference on Formal Methods in Computer-Aided Design, pages 165-169. FMCAD Inc., 2019. URL: https://doi.org/10.23919/FMCAD.2018.8602997.
  2. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Bui Phi Diep, Lukás Holík, Denghang Hu, Wei-Lun Tsai, Zhilin Wu, and Di-De Yen. Solving not-substring constraint with flat abstraction. In Hakjoo Oh, editor, Programming Languages and Systems - 19th Asian Symposium, APLAS 2021, Chicago, IL, USA, October 17-18, 2021, Proceedings, Lecture Notes in Computer Science. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-89051-3_17.
  3. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Bui Phi Diep, Lukáš Holík, Ahmed Rezine, and Philipp Rümmer. Flatten and conquer: A framework for efficient analysis of string constraints. In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017, pages 602-617, New York, NY, USA, 2017. Association for Computing Machinery. URL: https://doi.org/10.1145/3062341.3062384.
  4. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Bui Phi Diep, Lukáš Holík, Ahmed Rezine, and Philipp Rümmer. Flatten and conquer: A framework for efficient analysis of string constraints. SIGPLAN Not., 52(6), 2017. URL: https://doi.org/10.1145/3140587.3062384.
  5. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Lukás Holík, Ahmed Rezine, Philipp Rümmer, and Jari Stenman. String constraints for verification. In Armin Biere and Roderick Bloem, editors, Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings, volume 8559 of Lecture Notes in Computer Science, pages 150-166. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-08867-9_10.
  6. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Lukás Holík, Ahmed Rezine, Philipp Rümmer, and Jari Stenman. Norn: An SMT solver for string constraints. In Daniel Kroening and Corina S. Pasareanu, editors, Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I, volume 9206 of Lecture Notes in Computer Science, pages 462-469. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-21690-4_29.
  7. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Vrunda Dave, and Shankara Narayanan Krishna. On the separability problem of string constraints. In Igor Konnov and Laura Kovács, editors, 31st International Conference on Concurrency Theory, CONCUR 2020, September 1-4, 2020, Vienna, Austria (Virtual Conference), volume 171 of LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2020.16.
  8. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bui Phi Diep, Lukás Holík, and Petr Janku. Chain-free string constraints. In Yu-Fang Chen, Chih-Hong Cheng, and Javier Esparza, editors, Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings, volume 11781 of Lecture Notes in Computer Science. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-31784-3_16.
  9. C. Aiswarya, Soumodev Mal, and Prakash Saivasan. On the satisfiability of context-free string constraints with subword-ordering. In Christel Baier and Dana Fisman, editors, LICS '22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2 - 5, 2022. ACM, 2022. URL: https://doi.org/10.1145/3531130.3533329.
  10. C Aiswarya, Soumodev Mal, and Prakash Saivasan. Satisfiability of context-free string constraints with subword-ordering and transducers, 2024. URL: https://arxiv.org/abs/2401.07996.
  11. Roberto Amadini. A survey on string constraint solving. ACM Comput. Surv., 55(2):16:1-16:38, 2023. URL: https://doi.org/10.1145/3484198.
  12. Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, and Prakash Saivasan. On bounded reachability analysis of shared memory systems. In Venkatesh Raman and S. P. Suresh, editors, 34th International Conference on Foundation of Software Technology and Theoretical Computer Science, FSTTCS 2014, December 15-17, 2014, New Delhi, India, volume 29 of LIPIcs, pages 611-623. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014. URL: https://doi.org/10.4230/LIPICS.FSTTCS.2014.611.
  13. Mohamed Faouzi Atig, Ahmed Bouajjani, and Tayssir Touili. On the reachability analysis of acyclic networks of pushdown systems. In Franck van Breugel and Marsha Chechik, editors, Concurrency Theory, 19th International Conference, CONCUR 2008, Toronto, Canada, August 19-22, 2008. Proceedings, volume 5201 of Lecture Notes in Computer Science. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-85361-9_29.
  14. Mohamed Faouzi Atig, Dmitry Chistikov, Piotr Hofman, K. Narayan Kumar, Prakash Saivasan, and Georg Zetzsche. The complexity of regular abstractions of one-counter languages. In Martin Grohe, Eric Koskinen, and Natarajan Shankar, editors, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, New York, NY, USA, July 5-8, 2016, pages 207-216. ACM, 2016. URL: https://doi.org/10.1145/2933575.2934561.
  15. Mohamed Faouzi Atig, K. Narayan Kumar, and Prakash Saivasan. Adjacent ordered multi-pushdown systems. In Marie-Pierre Béal and Olivier Carton, editors, Developments in Language Theory - 17th International Conference, DLT 2013, Marne-la-Vallée, France, June 18-21, 2013. Proceedings, volume 7907 of Lecture Notes in Computer Science, pages 58-69. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-38771-5_7.
  16. Murphy Berzish, Joel D. Day, Vijay Ganesh, Mitja Kulczynski, Florin Manea, Federico Mora, and Dirk Nowotka. Towards more efficient methods for solving regular-expression heavy string constraints. Theor. Comput. Sci., 2023. URL: https://doi.org/10.1016/j.tcs.2022.12.009.
  17. Murphy Berzish, Vijay Ganesh, and Yunhui Zheng. Z3str3: A string solver with theory-aware heuristics. In Proceedings of the 17th Conference on Formal Methods in Computer-Aided Design, FMCAD '17, Austin, Texas, 2017. FMCAD Inc. URL: https://doi.org/10.23919/FMCAD.2017.8102241.
  18. J. Richard Büchi and Steven Senger. Definability in the existential theory of concatenation and undecidable extensions of this theory. Math. Log. Q., 34:337-342, 1988. Google Scholar
  19. Taolue Chen, Yan Chen, Matthew Hague, Anthony W. Lin, and Zhilin Wu. What is decidable about string constraints with the replaceall function. Proc. ACM Program. Lang., 2(POPL):3:1-3:29, 2018. URL: https://doi.org/10.1145/3158091.
  20. Taolue Chen, Alejandro Flores-Lamas, Matthew Hague, Zhilei Han, Denghang Hu, Shuanglong Kan, Anthony W. Lin, Philipp Rümmer, and Zhilin Wu. Solving string constraints with regex-dependent functions through transducers with priorities and variables. Proc. ACM Program. Lang., 6(POPL), 2022. URL: https://doi.org/10.1145/3498707.
  21. Taolue Chen, Alejandro Flores-Lamas, Matthew Hague, Zhilei Han, Denghang Hu, Shuanglong Kan, Anthony Widjaja Lin, Philipp Rümmer, and Zhilin Wu. Solving string constraints with regex-dependent functions through transducers with priorities and variables. CoRR, abs/2111.04298, 2021. Google Scholar
  22. Taolue Chen, Matthew Hague, Jinlong He, Denghang Hu, Anthony Widjaja Lin, Philipp Rümmer, and Zhilin Wu. A decision procedure for path feasibility of string manipulating programs with integer data type. In Dang Van Hung and Oleg Sokolsky, editors, Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Hanoi, Vietnam, October 19-23, 2020, Proceedings, volume 12302 of Lecture Notes in Computer Science, pages 325-342. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-59152-6_18.
  23. Taolue Chen, Matthew Hague, Anthony W. Lin, Philipp Rümmer, and Zhilin Wu. Decision procedures for path feasibility of string-manipulating programs with complex operations. Proc. ACM Program. Lang., 3(POPL), 2019. URL: https://doi.org/10.1145/3290362.
  24. Peter Chini, Jonathan Kolberg, Andreas Krebs, Roland Meyer, and Prakash Saivasan. On the complexity of bounded context switching. In Kirk Pruhs and Christian Sohler, editors, 25th Annual European Symposium on Algorithms, ESA 2017, September 4-6, 2017, Vienna, Austria, volume 87 of LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.ESA.2017.27.
  25. John Corcoran, William Frank, and Michael Maloney. String theory. J. Symb. Log., 39(4):625-637, 1974. URL: https://doi.org/10.2307/2272846.
  26. Joel D. Day. Word equations in the context of string solving. In Volker Diekert and Mikhail V. Volkov, editors, Developments in Language Theory - 26th International Conference, DLT 2022, Tampa, FL, USA, May 9-13, 2022, Proceedings, Lecture Notes in Computer Science. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-05578-2_2.
  27. Joel D. Day, Vijay Ganesh, Nathan Grewal, and Florin Manea. On the expressive power of string constraints. Proc. ACM Program. Lang., 7(POPL):278-308, 2023. URL: https://doi.org/10.1145/3571203.
  28. Joel D. Day, Vijay Ganesh, Paul He, Florin Manea, and Dirk Nowotka. The satisfiability of word equations: Decidable and undecidable theories. In Igor Potapov and Pierre-Alain Reynier, editors, Reachability Problems, pages 15-29, Cham, 2018. Springer International Publishing. Google Scholar
  29. Diego Figueira, Artur Jez, and Anthony W. Lin. Data path queries over embedded graph databases. In Leonid Libkin and Pablo Barceló, editors, PODS '22: International Conference on Management of Data, Philadelphia, PA, USA, June 12 - 17, 2022, pages 189-201. ACM, 2022. URL: https://doi.org/10.1145/3517804.3524159.
  30. Vijay Ganesh, Mia Minnes, Armando Solar-Lezama, and Martin C. Rinard. Word equations with length constraints: What’s decidable? In Armin Biere, Amir Nahir, and Tanja E. J. Vos, editors, Hardware and Software: Verification and Testing - 8th International Haifa Verification Conference, HVC 2012, Haifa, Israel, November 6-8, 2012. Revised Selected Papers, volume 7857 of Lecture Notes in Computer Science. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-39611-3_21.
  31. Michael R. Garey and David S. Johnson. Computers and Intractability; A Guide to the Theory of NP-Completeness. W. H. Freeman & Co., USA, 1990. Google Scholar
  32. Matthew Hague, Anthony Widjaja Lin, and C.-H. Luke Ong. Detecting redundant CSS rules in HTML5 applications: a tree rewriting approach. In Jonathan Aldrich and Patrick Eugster, editors, Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2015, part of SPLASH 2015, Pittsburgh, PA, USA, October 25-30, 2015, pages 1-19. ACM, 2015. URL: https://doi.org/10.1145/2814270.2814288.
  33. Hermes Hans. Semiotik. eine theorie der zeichengestalten als grundlage für untersuchungen von formalisierten sprachen. Journal of Philosophy, 36(13):356-357, 1939. URL: https://doi.org/10.2307/2017267.
  34. Lukás Holík, Petr Janku, Anthony W. Lin, Philipp Rümmer, and Tomás Vojnar. String constraints with concatenation and transducers solved efficiently. Proc. ACM Program. Lang., 2(POPL), 2018. URL: https://doi.org/10.1145/3158092.
  35. Shuanglong Kan, Anthony Widjaja Lin, Philipp Rümmer, and Micha Schrader. Certistr: a certified string solver. In Andrei Popescu and Steve Zdancewic, editors, CPP '22: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022. ACM, 2022. URL: https://doi.org/10.1145/3497775.3503691.
  36. Adam Kiezun, Vijay Ganesh, Shay Artzi, Philip J. Guo, Pieter Hooimeijer, and Michael D. Ernst. Hampi: A solver for word equations over strings, regular expressions, and context-free grammars. ACM Trans. Softw. Eng. Methodol., 21(4), February 2013. Google Scholar
  37. Adam Kiezun, Philip J. Guo, Pieter Hooimeijer, Michael D. Ernst, and Vijay Ganesh. Theory and practice of string solvers (invited talk abstract). In Dongmei Zhang and Anders Møller, editors, Proceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2019, Beijing, China, July 15-19, 2019. ACM, 2019. URL: https://doi.org/10.1145/3293882.3338993.
  38. Tianyi Liang, Andrew Reynolds, Nestan Tsiskaridze, Cesare Tinelli, Clark Barrett, and Morgan Deters. An efficient SMT solver for string constraints. Form. Methods Syst. Des., 48(3), 2016. URL: https://doi.org/10.1007/s10703-016-0247-6.
  39. Anthony Widjaja Lin and Pablo Barceló. String solving with word equations and transducers: towards a logic for analysing mutation XSS. In Rastislav Bodík and Rupak Majumdar, editors, Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, pages 123-136. ACM, 2016. URL: https://doi.org/10.1145/2837614.2837641.
  40. G S Makanin. The problem of solvability of equations in a free smigroup. Mathematics of the USSR-Sbornik, 32(2), 1977. URL: https://doi.org/10.1070/SM1977v032n02ABEH002376.
  41. Yu. V. Matiyasevich. A connection between systems of words-and-lengths equations and Hilbert’s tenth problem. Studies in constructive mathematics and mathematical logic. Part II,Zap. Nauchn. Sem. LOMI, 8, 1968. Google Scholar
  42. Wojciech Plandowski. Satisfiability of word equations with constants is in PSPACE. In 40th Annual Symposium on Foundations of Computer Science, FOCS '99, 17-18 October, 1999, New York, NY, USA, pages 495-500. IEEE Computer Society, 1999. URL: https://doi.org/10.1109/SFFCS.1999.814622.
  43. W. V. Quine. Concatenation as a basis for arithmetic. The Journal of Symbolic Logic, 11, 1946. URL: https://doi.org/10.2307/2268308.
  44. Alfred Tarski. Der wahrheitsbegriff in den formalisierten sprachen. Studia Philosophica, 1:261-405, 1935. Google Scholar
  45. Jean van Heijenoort. From Frege to Gödel : A Source Book in Mathematical Logic. Harvard University Press, January 2002. Google Scholar
  46. Georg Zetzsche. The complexity of downward closure comparisons. In Ioannis Chatzigiannakis, Michael Mitzenmacher, Yuval Rabani, and Davide Sangiorgi, editors, 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016, July 11-15, 2016, Rome, Italy, volume 55 of LIPIcs, pages 123:1-123:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPICS.ICALP.2016.123.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact