Formal Languages via Theories over Strings: An Overview of Some Recent Results

Abstract

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 ex- pressible in terms of formulas over quantifier-free theories of word equa- tions, arithmetic over length constraints, and language membership predi- cates for the classes of regular, visibly pushdown, and deterministic context- free languages. As such, we have considered 20 distinct theories and decid- ability 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 uni- versality problem. To this end, it is worth noting that the emptiness problem for some theory is equivalent to the satisfiability problem over the corre- sponding 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 rel- evant 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.