FORMAL LANGUAGES VIA THEORIES OVER STRINGS: AN OVERVIEW OF SOME RECENT RESULTS

In this note, we overview a series of results that were obtained in [16, 15]. In these papers, we have investigated the properties of formal languages expressible in terms of formulas over quantifier-free theories of word equations, arithmetic over length constraints, and language membership predicates for the classes of regular, visibly pushdown, and deterministic contextfree languages. As such, we have considered 20 distinct theories and decidability questions for problems such as emptiness and universality for formal languages over them. In this note, we first present the relative expressive power of the approached theories. Secondly, we discuss the decidability status of several important decision problems, some of them with practical applications in the area of string solving, such as the emptiness and the universality problem. To this end, it is worth noting that the emptiness problem for some theory is equivalent to the satisfiability problem over the corresponding theory. Finally, we discuss the problem of deciding whether a language expressible in one theory is also expressible in another one, and show several undecidability results; these investigations are particularly relevant in the context of normal forms for string constraints, and, as such, they are relevant to both the practical and theoretical side of string solving. The current note is heavily based on the contents of [16, 15], and the readers are encouraged to check these references for complete details.