ausblenden:
Schlagwörter:
Computer Science, Logic in Computer Science, cs.LO,Computer Science, Formal Languages and Automata Theory, cs.FL
Zusammenfassung:
Word equations are a crucial element in the theoretical foundation of
constraint solving over strings. A word equation relates two words over string
variables and constants. Its solution amounts to a function mapping variables
to constant strings that equate the left and right hand sides of the equation.
While the problem of solving word equations is decidable, the decidability of
the problem of solving a word equation with a length constraint (i.e., a
constraint relating the lengths of words in the word equation) has remained a
long-standing open problem. We focus on the subclass of quadratic word
equations, i.e., in which each variable occurs at most twice. We first show
that the length abstractions of solutions to quadratic word equations are in
general not Presburger-definable. We then describe a class of counter systems
with Presburger transition relations which capture the length abstraction of a
quadratic word equation with regular constraints. We provide an encoding of the
effect of a simple loop of the counter systems in the existential theory of
Presburger Arithmetic with divisibility (PAD). Since PAD is decidable (NP-hard
and is in NEXP), we obtain a decision procedure for quadratic words equations
with length constraints for which the associated counter system is flat (i.e.,
all nodes belong to at most one cycle). In particular, we show a decidability
result (in fact, also an NP algorithm with a PAD oracle) for a recently
proposed NP-complete fragment of word equations called regular-oriented word
equations, when augmented with length constraints. We extend this decidability
result (in fact, with a complexity upper bound of PSPACE with a PAD oracle) in
the presence of regular constraints.
