A closer look at the expressive power of logics based on word equations
Word equations are equations α = β where α and β are words consisting of letters from some alphabet Σ and variables from a set X. Recently, there has been substantial interest in the context of string solving in logics combining word equations with other kinds of constraints on words such as (regular) language membership (regular constraints) and arithmetic over string lengths (length constraints). We consider the expressive power of such logics by looking at the set of all values a single variable might take as part of a satisfying assignment for a given formula. Hence, each formula-variable pair defines a formal language, and each logic defines a class of formal languages. We consider logics arising from combining word equations with either length constraints, regular constraints, or both. We also consider word equations with visibly pushdown language membership constraints as a generalisation of the combination of regular and length constraints. We show that word equations with visibly pushdown membership constraints are sufficient to express all recursively enumerable languages and hence satisfiability is undecidable in this case. We then establish a strict hierarchy involving the other combinations. We also provide a complete characterisation of when a thin regular language is expressible by word equations (alone) and some further partial results for regular languages in the general case.
German Research Foundation (Deutsche Forschungsgemeinschaft, DFG), by the project with number 466789228
- Computer Science
Published inTheory of Computing Systems
- VoR (Version of Record)
Rights holder© The Author(s)
Publisher statementThis is an Open Access Article. It is published by Springer under the Creative Commons Attribution 4.0 International Licence (CC BY). Full details of this licence are available at: https://creativecommons.org/licenses/by/4.0/