What is Decidable about Strings?
We prove several decidability and undecidability results for the satisfiability/validity problem of formulas over a language of finite-length strings and integers (interpreted as lengths of strings). The atomic formulas over this language are equality over string terms (word equations), linear inequ...
| Main Authors: | , , , |
|---|---|
| Other Authors: | |
| Published: |
2011
|
| Subjects: | |
| Online Access: | http://hdl.handle.net/1721.1/60877 |
| _version_ | 1811091099173781504 |
|---|---|
| author | Ganesh, Vijay Minnes, Mia Solar-Lezama, Armando Rinard, Martin |
| author2 | Martin Rinard |
| author_facet | Martin Rinard Ganesh, Vijay Minnes, Mia Solar-Lezama, Armando Rinard, Martin |
| author_sort | Ganesh, Vijay |
| collection | MIT |
| description | We prove several decidability and undecidability results for the satisfiability/validity problem of formulas over a language of finite-length strings and integers (interpreted as lengths of strings). The atomic formulas over this language are equality over string terms (word equations), linear inequality over length function (length constraints), and membership predicate over regularexpressions (r.e.). These decidability questions are important in logic, program analysis and formal verification. Logicians have been attempting to resolve some of these questions for many decades, while practical satisfiability procedures for these formulas are increasingly important in the analysis of string-manipulating programs such as web applications and scripts. We prove three main theorems. First, we consider Boolean combination of quantifier-free formulas constructed out of word equations and length constraints. We show that if word equations can be converted to a solved form, a form relevant in practice, then the satisfiability problem for Boolean combination of word equations and length constraints is decidable. Second, we show that the satisfiability problem for word equations in solved form that areregular, length constraints and r.e. membership predicate is also decidable. Third, we show that the validity problem for the set of sentences written as a forall-exists quantifier alternation applied to positive word equations is undecidable. A corollary of this undecidability result is that this set is undecidable even with sentences with at most two occurrences of a string variable. |
| first_indexed | 2024-09-23T14:57:00Z |
| id | mit-1721.1/60877 |
| institution | Massachusetts Institute of Technology |
| last_indexed | 2024-09-23T14:57:00Z |
| publishDate | 2011 |
| record_format | dspace |
| spelling | mit-1721.1/608772019-04-12T11:48:40Z What is Decidable about Strings? Ganesh, Vijay Minnes, Mia Solar-Lezama, Armando Rinard, Martin Martin Rinard Computer Architecture Theories of strings decidability undecidability word equations regular expressions JavaScript Formal methods Program Analysis We prove several decidability and undecidability results for the satisfiability/validity problem of formulas over a language of finite-length strings and integers (interpreted as lengths of strings). The atomic formulas over this language are equality over string terms (word equations), linear inequality over length function (length constraints), and membership predicate over regularexpressions (r.e.). These decidability questions are important in logic, program analysis and formal verification. Logicians have been attempting to resolve some of these questions for many decades, while practical satisfiability procedures for these formulas are increasingly important in the analysis of string-manipulating programs such as web applications and scripts. We prove three main theorems. First, we consider Boolean combination of quantifier-free formulas constructed out of word equations and length constraints. We show that if word equations can be converted to a solved form, a form relevant in practice, then the satisfiability problem for Boolean combination of word equations and length constraints is decidable. Second, we show that the satisfiability problem for word equations in solved form that areregular, length constraints and r.e. membership predicate is also decidable. Third, we show that the validity problem for the set of sentences written as a forall-exists quantifier alternation applied to positive word equations is undecidable. A corollary of this undecidability result is that this set is undecidable even with sentences with at most two occurrences of a string variable. 2011-02-01T20:15:11Z 2011-02-01T20:15:11Z 2011-02-01 http://hdl.handle.net/1721.1/60877 MIT-CSAIL-TR-2011-006 16 p. application/pdf |
| spellingShingle | Theories of strings decidability undecidability word equations regular expressions JavaScript Formal methods Program Analysis Ganesh, Vijay Minnes, Mia Solar-Lezama, Armando Rinard, Martin What is Decidable about Strings? |
| title | What is Decidable about Strings? |
| title_full | What is Decidable about Strings? |
| title_fullStr | What is Decidable about Strings? |
| title_full_unstemmed | What is Decidable about Strings? |
| title_short | What is Decidable about Strings? |
| title_sort | what is decidable about strings |
| topic | Theories of strings decidability undecidability word equations regular expressions JavaScript Formal methods Program Analysis |
| url | http://hdl.handle.net/1721.1/60877 |
| work_keys_str_mv | AT ganeshvijay whatisdecidableaboutstrings AT minnesmia whatisdecidableaboutstrings AT solarlezamaarmando whatisdecidableaboutstrings AT rinardmartin whatisdecidableaboutstrings |