(Un)Decidability Results for Word Equations with Length and Regular Expression Constraints

TL;DR

This paper investigates the boundaries of decidability for solving word equations with length and regular expression constraints, providing new undecidability proofs and identifying decidable fragments relevant to program analysis.

Contribution

It offers new undecidability proofs for certain logical formulas involving word equations and length constraints, and identifies decidable fragments for practical applications.

Findings

Undecidability of validity for certain quantified word equations.

Decidability of satisfiability for quantifier-free formulas with solved form word equations.

Decidability of satisfiability for formulas combining word equations, length constraints, and regular membership.

Abstract

We prove several decidability and undecidability results for the satisfiability and validity problems for languages that can express solutions to word equations with length constraints. The atomic formulas over this language are equality over string terms (word equations), linear inequality over the length function (length constraints), and membership in regular sets. These questions are important in logic, program analysis, and formal verification. Variants of these questions have been studied for many decades by mathematicians. More recently, practical satisfiability procedures (aka SMT solvers) for these formulas have become increasingly important in the context of security analysis for string-manipulating programs such as web applications. We prove three main theorems. First, we give a new proof of undecidability for the validity problem for the set of sentences written as a forall-exists quantifier alternation applied to positive word equations. A corollary of this undecidability result is that this set is undecidable even with sentences with at most two occurrences of a string variable. Second, we consider Boolean combinations 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 combinations of word equations and length constraints is decidable. Third, we show that the satisfiability problem for quantifier-free formulas over word equations in regular solved form, length constraints, and the membership predicate over regular expressions is also decidable.