11institutetext:  Oxford University, UK 22institutetext: Max Planck Institute
for Software Systems, Germany

#  Quadratic Word Equations with Length Constraints, Counter Systems, and
Presburger Arithmetic with Divisibility

Anthony W. Lin 11 Rupak Majumdar 22

###### Abstract

Word equations are a crucial element in the theoretical foundation of
constraint solving over strings, which have received a lot of attention in
recent years. 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. In this paper, 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
theory of existential Presburger Arithmetic with divisibility (PAD). Since PAD
is decidable, we get 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). 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,
together with length constraints. Decidability holds when the constraints are
additionally extended with regular constraints with a 1-weak control
structure.

##  1 Introduction

Reasoning about strings is a fundamental problem in computer science and
mathematics. The full first order theory over strings and concatenation is
undecidable. A seminal result by Makanin [26] (see also [12, 18]) shows that
the satisfiability problem for the _existential fragment_ is decidable, by
showing an algorithm to check satisfiability of _word equations_. Precisely, a
word equation $L=R$ consists of two words $L$ and $R$ over an alphabet of
constants and variables. Such an equation is satisfiable if there is a mapping
$\sigma$ from the variables to strings over the constants such that
$\sigma(L)$ and $\sigma(R)$ are syntactically identical.

An original motivation for studying word equations was to show undecidability
of Hilbert’s 10th problem (see, e.g., [28]). While Makanin’s later result
shows that word equations could not, by themselves, show undecidability,
Matiyasevich in 1968 considered an extension of word equations with _length
constraints_ as a possible route to showing undecidability of Hilbert’s 10th
problem [28]. A length constraint constrains the solution of a word equation
by requiring a linear relationship to hold on the lengths of words in a
solution $\sigma$. For example, a length constraint might require that a
solution maps variable $x$ and variable $y$ to words of the same length. The
decidability of word equations with length constraints remains open.

In recent years, reasoning about strings with length constraints has found
renewed interest through applications in program verification and reasoning
about security vulnerabilities. The focus of most research has been on
developing practical string solvers [34, 32, 6, 1, 24, 3, 14, 15, 19, 36, 35,
8, 17, 33]. These solvers are sound but make no claims of completeness.
Relatively few results are known about the decidability status of strings with
length and other constraints (see [10] for an overview of the results in this
area). The main idea in most existing decidability results is the encoding of
length constraints into Presburger arithmetic [16, 10]. However, the length
abstraction of a word equation, that is, the set of possible lengths of
variables in its solutions, need not be Presburger definable. (Indeed, this
was Matiyasevich’s motivation in studying this problem as a way to prove
undecidability of Hilbert’s 10th problem.)

In this paper, we consider the case of _quadratic_ word equations, in which
each variable can appear at most twice [22, 13], together with length and
regularity constraints. For quadratic word equations, there is a simpler
decision procedure (called the Nielsen transform or Levi’s method) based on a
non-deterministic proof tree construction. The technique can be extended to
handle regular constraints [13]. However, we show that already for this class
(even for a simple equation like $xaby=yabx$, where $x,y$ are variables and
$a,b$ are constants), the length abstraction need not be Presburger-definable.
Thus, techniques based on Presburger encodings are not sufficient to prove
decidability.

Our first observation in this paper is a connection between the problem of
quadratic word equations with length constraints and a class of counter
systems with Presburger transitions. Informally, the counter system has
control states corresponding to the nodes of the proof tree constructed by
Levi’s method, and a counter standing for the length each word variable. Each
step of Levi’s method may decrease at most one counter. Thus, from any initial
state, the counter system terminates. We show that the set of initial counter
values which can lead to a successful leaf (i.e., one containing the trivial
equation $\epsilon=\epsilon$) is precisely the length abstraction of the word
equation.

Our second observation is that the reachability relation for a simple loop of
the counter system can be encoded in the existential theory of Presburger
arithmetic with divisibility $\mathcal{PAD}$. The encoding is non-trivial in
the presence of regular constraints, and depends on structural results on
semilinear sets. As $\mathcal{PAD}$ is decidable [25, 21], we obtain a
technique to symbolically represent the reachability relation for _flat_
counter systems, in which each node belongs to at most one loop.

Moreover, the same encoding shows decidability for word equations with length
constraints, provided the proof tree is associated with flat counter systems.
In particular, we show that the class of _regular-oriented_ word equations,
introduced by [11], have flat proof trees. Thus, the satisfiability problem
for quadratic regular-oriented word equations with length constraints is
decidable (and in NEXP).111 In fact, the decision procedure is NP with an
oracle access to a decision procedure for Presburger arithmetic with
decidability. The best complexity bounds for the latter are NEXP and NP-
hardness [21].

While our decidability result is for a simple subclass, this class is already
non-trivial without length and regular constraints: satisfiability of regular-
oriented word equations is NP-complete [11]. Our result generalizes previous
decidability results [10]. Moreover, we believe that the techniques introduced
in this paper, such as the connection between acceleration and word equations,
and the use of existential Presburger with divisibility, can open the way to
more sophisticated decision procedures or tools based on acceleration designed
for counter systems.

##  2 Preliminaries

General notation: Let $\mathbb{N}=\mathbb{Z}_{\geq 0}$ be the set of all
natural numbers. For integers $i\leq j$, we use $[i,j]$ to denote the set
$\\{i,i+1,\ldots,j-1,j\\}$ of integers. If $i\in\mathbb{N}$, let $[i]$ denote
$[0,i]$. We use $\preceq$ to denote the component-wise ordering on
$\mathbb{N}^{k}$, i.e., $(x_{1},\ldots,x_{k})\preceq(y_{1},\ldots,y_{k})$ iff
$x_{i}\leq y_{i}$ for all $i\in[1,k]$. If $\bar{x}\preceq\bar{y}$ and
$\bar{x}\neq\bar{y}$, we write $\bar{x}\prec\bar{y}$.

If $S$ is a set, we use $S^{*}$ to denote the set of all finite sequences
$\gamma=s_{1}\ldots s_{n}$ over $S$. The length $|\gamma|$ of $\gamma$ is $n$.
The empty sequence is denoted by $\epsilon$. Notice that $S^{*}$ forms a
monoid with the concatenation operator $\cdot$. If $\gamma^{\prime}$ is a
prefix of $\gamma$, we write $\gamma^{\prime}\preceq\gamma$. Additionally, if
$\gamma^{\prime}\neq\gamma$ (i.e. a strict prefix of $\gamma$), we write
$\gamma^{\prime}\prec\gamma$. Note that the operator $\preceq$ is overloaded
here, but the meaning should be clear from the context.

Words and Automata: We assume basic familiarity with word combinatorics and
automata theory. Fix a (finite) alphabet $A$. For each finite word
$w:=w_{1}\ldots w_{n}\in A^{*}$, we write $w[i,j]$, where $1\leq i\leq j\leq
n$, to denote the segment $w_{i}\ldots w_{j}$. We write $\epsilon$ for the
empty word.

Two words $x$ and $y$ are _conjugates_ if there exist words $u$ and $v$ such
that $x=uv$ and $y=vu$. Equivalently, $x=\mathrm{cyc}^{k}(y)$ for some $k$ and
for the cyclic permutation􏲄operation $\mathrm{cyc}:A^{*}\rightarrow A^{*}$,
defined as $\mathrm{cyc}(\epsilon)=\epsilon$, and $\mathrm{cyc}(a\cdot
w)=w\cdot a$ for $a\in A$ and $w\in A^{*}$.

Given a nondeterministic finite automaton (NFA)
$\mathcal{A}:=(A,Q,\Delta,q_{0},q_{F})$, a run of $\mathcal{A}$ on $w$ is a
function $\rho:\mathbb{N}\to Q$ with $\rho(0)=q_{0}$ that obeys the transition
relation $\Delta$. We may also denote the run $\rho$ by the word
$\rho(0)\cdots\rho(n)$ over the alphabet $Q$. The run $\rho$ is said to be
accepting if $\rho(n)=q_{F}$, in which case we say that the word $w$ is
accepted by $\mathcal{A}$. The language $\mathcal{L}(\mathcal{A})$ of
$\mathcal{A}$ is the set of words in $A^{*}$ accepted by $\mathcal{A}$. In the
sequel, for $p,q\in Q$ we will write $\mathcal{A}_{p,q}$ to denote the NFA
$\mathcal{A}$ with initial state replaced by $p$ and final is replaced by $q$.

Word equations: Let $A$ be a (finite) alphabet of constants and ${V}$ a set of
variables; we assume $A\cap{V}=\emptyset$. A _word equation_ $E$ is an
expression of the form $L=R$, where
$L,R\in(A\cup{V})^{*}\times(A\cup{V})^{*}$. A system of word equations is a
nonempty set ${\\{L_{1}=R_{1},L_{2}=R_{2},\ldots,L_{k}=R_{k}\\}}$ of word
equations. The length of a system of word equations is the length
$\sum_{i=1}^{k}(|L_{i}|+|R_{i}|)$. A system is called _quadratic_ if each
variable occurs at most twice in all. A _solution_ to a system of word
equations is a homomorphism ${\sigma}:(A\cup{V})^{*}\rightarrow A^{*}$ which
maps each $a\in A$ to itself that equates the l.h.s. and r.h.s. of each
equation, i.e., ${\sigma}(L_{i})={\sigma}(R_{i})$ for each $i=1,\ldots,k$.

For each variable $x\in{V}$, we shall use $|x|$ to denote a formal variable
that stands for the length of variable $x$. Let $L_{{V}}$ be the set
${\\{|x|\mid x\in{V}\\}}$. A _length constraint_ is a formula in Presburger
arithmetic whose free variables are in $L_{V}$.

A _solution_ to a system of word equations with a length constraint
$\Phi(l_{x_{1}},\ldots,l_{x_{n}})$ is a homomorphism
${\sigma}:(A\cup{V})^{*}\rightarrow A^{*}$ which maps each $a\in A$ to itself
such that ${\sigma}(L_{i})={\sigma}(R_{i})$ for each $i=1,\ldots,k$ and
moreover $\Phi(|{\sigma}(x_{1})|,\ldots,|{\sigma}(x_{n})|)$ holds. That is,
the homomorphism maps each variable to a word in $A^{*}$ such that each word
equation is satisfied, and the lengths of these words satisfy the length
constraint.

The satisfiability problem for word equations with length constraints asks,
given a system of word equations and a length constraint, whether it has a
solution.

We also consider the extension of the problem with regular constraints. For a
system of word equations, a variable $x\in{V}$, and a regular language
$\mathcal{L}\subseteq A^{*}$, a _regular constraint_ $x\in\mathcal{L}$ imposes
the additional restriction that any solution ${\sigma}$ must satisfy
${\sigma}(x)\in\mathcal{L}$. Given a system of word equations, a length
constraint, and a set of regular constraints, the satisfiability problem asks
if there is a solution satisfying the word equation, the length constraints,
as well as the regular constraints.

In the sequel, for clarity of exposition, we restrict our discussion to a
system consisting of a single word equation (w.l.o.g.).

Linear arithmetic with divisibility: Let $\mathcal{P}$ be a first-order
language with equality, with binary relation symbol $\leq$, and with terms
being linear polynomials with integer coefficients. We write $f(x)$, $g(x)$,
etc., for terms in integer variables $x=x_{1},\ldots,x_{n}$. Atomic formulas
in Presburger arithmetic have the form $f(x)\leq g(x)$ or $f(x)=g(x)$. The
language $\mathcal{PAD}$ of _Presburger arithmetic with divisibility_ extends
the language $\mathcal{P}$ with a binary relation $|$ (for divides). An atomic
formula has the form have the form $f(x)\leq g(x)$ or $f(x)=g(x)$ of
$f(x)|g(x)$, where $f(x)$ and $g(x)$ are linear polynomials with integer
coefficients. The full first order theory of $\mathcal{PAD}$ is undecidable,
but the existential fragment is decidable [25, 21].

Note that the divisibility predicate $x|y$ is _not_ expressible in Presburger
arithmetic: a simple way to see this is that ${\\{(x,y)\in\mathbb{N}^{2}\mid
x|y\\}}$ is not a semi-linear set.

Counter systems: In this paper, we specifically use the term “counter systems”
to mean counter systems with Presburger transition relations (e.g. see [4]).
These more general transition relations can be simulated by standard Minsky’s
counter machines, but they are more useful for coming up with decidable
subclasses of counter systems. A counter system $\mathcal{C}$ is a tuple
$(X,Q,\Delta)$, where $X=\\{x_{1},\ldots,x_{m}\\}$ is a finite set of
counters, $Q$ is a finite set of control states, and $\Delta$ is a finite set
of transitions of the form $(q,\Phi(\bar{}x,\bar{}x^{\prime}),q^{\prime})$,
where $q,q^{\prime}\in Q$ and $\Phi$ is a Presburger formula with free
variables $x_{1},\ldots,x_{m},x_{1}^{\prime},\ldots,x_{m}^{\prime}$. A
configuration of $\mathcal{C}$ is a tuple $(q,\text{\rm v})\in
Q\times\mathbb{N}^{m}$.

The semantics of counter systems is given as a transition system. A transition
system is a tuple $\mathfrak{S}:=\langle S;\to\rangle$, where $S$ is a set of
configurations and $\to\ \subseteq S\times S$ is a binary relation over $S$. A
path in $\mathfrak{S}$ is a sequence $s_{0}\to\cdots\to s_{n}$ of
configurations $s_{0},...,s_{n}\in S$.

A counter system $\mathcal{C}$ generates the transition system
$\mathfrak{S}_{\mathcal{C}}=\langle S;\to\rangle$, where $S$ is the set of all
configurations of $\mathcal{C}$, and $(q,\text{\rm v})\to(q^{\prime},\text{\rm
v}^{\prime})$ if there exists a transition
$(q,\Phi(\bar{}x,\bar{}x^{\prime}),q^{\prime})\in\Delta$ such that
$\Phi(\text{\rm v},\text{\rm v}^{\prime})$ is satisfiable.

In the sequel, we will be needing the notion of flat counter systems [7, 23,
5, 4]. Given a counter system $\mathcal{C}=(X,Q,\Delta)$, the control
structure of $\mathcal{C}$ is an edge-labeled directed graph $G=(V,E)$ with
the set $V=Q$ of nodes and the set $E=\Delta$. The counter system
$\mathcal{C}$ is flat if each node $v\in V$ is contained in at most one simple
cycle.

##  3 Solving Quadratic Word Equations

We start by recalling a simple textbook recipe (called Nielsen transformation,
a.k.a., Levi’s Method) [12, 22] for solving quadratic word equations, both for
the cases with and without regular constraints. We then discuss the length
abstractions of solutions to quadratic word equations, and provide several
natural examples that are not Presburger-definable.

###  3.1 Nielsen transformation

We will define a rewriting relation $E\Rightarrow E^{\prime}$ between
quadratic word equations $E,E^{\prime}$. Let $E$ be an equation of the form
$\alpha w_{1}=\beta w_{2}$ with $w_{1},w_{2}\in(A\cup{V})^{*}$ and
$\alpha,\beta\in A\cup{V}$. Then, there are several possible $E^{\prime}$:

  * •

Rules for erasing an empty prefix variable. These rules can be applied if
$\alpha\in{V}$ (symmetrically, $\beta\in{V}$). In this case, we can
nondeterministically guess that $\alpha$ be the empty word $\epsilon$. That
is, $E^{\prime}$ is $(w_{1}=w_{2})[\epsilon/\alpha]$. The symmetric case of
$\beta\in{V}$ is similar.

  * •

Rules for removing a nonempty prefix. These rules are applicable if each of
$\alpha$ and $\beta$ is either a constant or a variable that we
nondeterministically guess to be a nonempty word. There are several cases:

(P1)

$\alpha=\beta$ (syntactic equality). In this case, $E^{\prime}$ is
$w_{1}=w_{2}$.

(P2)

$\alpha\in A$ and $\beta\in{V}$. In this case, $E^{\prime}$ is $(w_{1}=\beta
w_{2})[\alpha\beta/\beta]$.

(P3)

$\alpha\in{V}$ and $\beta\in A$. In this case, $E^{\prime}$ is $(\alpha
w_{1}=w_{2})[\beta\alpha/\alpha]$.

(P4)

$\alpha,\beta\in{V}$. In this case, we nondeterministically guess if
$\alpha\preceq\beta$ or $\beta\preceq\alpha$. In the former case, the equation
$E^{\prime}$ is $(w_{1}=\beta w_{2})[\alpha\beta/\beta]$. In the latter case,
the equation $E^{\prime}$ is $E^{\prime}$ is $(\alpha
w_{1}=w_{2})[\beta\alpha/\alpha]$.

Note that the transformation keeps an equation quadratic.

###### Proposition 1

$E$ is solvable iff $E\Rightarrow^{*}(\epsilon=\epsilon)$. Furthermore,
checking if $E$ is solvable is in PSPACE.

See [12] for a proof. Roughly speaking, the proof uses the fact that each step
either decreases the size of the equation, or the length of a length-minimal
solution. It runs in PSPACE (in fact, linear space) because each rewriting
does not increase the size of the equation.

###  3.2 Handling regular constraints

Nielsen transformation easily extends to quadratic word equations with regular
constraints (e.g. see [13]). We assume that a regular constraint
$x\in\mathcal{L}$ is given as an NFA $\mathcal{A}_{p,q}$ representing
$\mathcal{L}$. [If $q_{0}$ and $q_{F}$ are the initial and final states
(respectively) of an NFA $\mathcal{A}$, we can be more explicit and write
$\mathcal{A}_{q_{0},q_{F}}$ instead of $\mathcal{A}$.]

Our rewriting relation $\Rightarrow$ now works over a pair consisting of an
equation $E$ and a set $S$ of regular constraints over variables in $E$. Let
$E$ be an equation of the form $\alpha w_{1}=\beta w_{2}$ with
$w_{1},w_{2}\in(A\cup{V})^{*}$ and $\alpha,\beta\in A\cup{V}$. We now define
$(E,S)\Rightarrow(E^{\prime},S^{\prime})$ by extending the definition of
$\Rightarrow$ without regular constraints. In particular, it has to be the
case that $E\Rightarrow E^{\prime}$ and additionally do the following:

  * •

Rules for erasing an empty prefix variable $x$. When applied, ensure that each
regular constraint $x\in\mathcal{L}$ in $S$ satisfies
$\epsilon\in\mathcal{L}$. Define $S^{\prime}$ as $S$ minus all regular
constraints of the form $x\in\mathcal{L}$.

  * •

Rules for removing a nonempty prefix. For (P1), we have set $S^{\prime}$ to be
$S$ minus all constraints of the form $\alpha\in\mathcal{L}$ if $\alpha$ is a
variable. For (P2)–(P4), assume that $E^{\prime}$ is $(w_{1}=\beta
w_{2})[\alpha\beta/\beta]$; the other case is symmetric. For each regular
constraint $\beta\in\mathcal{L}(\mathcal{A}_{p,q})$, we nondeterministically
guess a state $r$, and add $\alpha\in\mathcal{L}(\mathcal{A}_{p,r})$ and
$\beta\in\mathcal{L}(\mathcal{A}_{r,q})$ to $S^{\prime}$. In the case when
$\alpha\in A$, we could immediately perform the check
$\alpha\in\mathcal{L}(\mathcal{A}_{p,r})$: a positive outcome implies removing
this constraint from $S^{\prime}$, while on a negative outcome our algorithm
simply fails on this branch. For any variable $y$ that is distinct from $x$,
we add all regular constraints $y\in L$ in $S$ to $S^{\prime}$.

###### Proposition 2

$(E,S)$ is solvable iff $(E,S)\Rightarrow^{*}(\epsilon=\epsilon,\emptyset)$.
Furthermore, checking if $(E,S)$ is solvable is in PSPACE.

Note that this is still a PSPACE algorithm because it never creates a new NFA
or adds new states to existing NFA in the regular constraints, but rather adds
a regular constraint $x\in\mathcal{L}(\mathcal{A}_{p,q})$ to a variable $x$,
where $\mathcal{A}$ is an NFA that is already in the regular constraint.

###  3.3 Generating all solutions using Nielsen transformation

One result that we will need in this paper is that Nielsen transformation is
able to _generate all solutions_ of quadratic word equations with regular
constraints. To clarify this, we extend the definition of $\Rightarrow$ so
that each a configuration $E$ or $(E,S)$ in the graph of $\Rightarrow$ is also
annotated by an assignment ${\sigma}$ of the variables to concrete strings. We
write $E_{1}[{\sigma}_{1}]\Rightarrow E_{2}[{\sigma}_{2}]$ if
$E_{1}\Rightarrow E_{2}$ and ${\sigma}_{2}$ is the modification from
${\sigma}_{1}$ according to the operation used to obtain $E_{2}$ from $E_{1}$.
That is, suppose that ${\sigma}_{1}(x)=ab$ and ${\sigma}_{1}(y)=abaaab$ and
$E_{1}:=xy=yx$ and $E_{2}:=E_{1}[xy/y]$. In this case,
${\sigma}_{2}(x)={\sigma}_{1}(x)=ab$ but ${\sigma}_{2}(y)=aaab$ since we have
taken off the prefix ${\sigma}_{1}(x)$ from ${\sigma}_{1}(y)$. This definition
for the case with regular constraints is identical.

###### Proposition 3

$(E,S)[{\sigma}]\to^{*}(\epsilon=\epsilon,\emptyset)[{\sigma}^{\prime}]$ where
${\sigma}^{\prime}$ has the empty domain iff ${\sigma}$ is a solution of
$(E,S)$.

This proposition immediately follows from the proof of correctness of Nielsen
transformation for quadratic word equations [12].

###  3.4 Length abstractions and semilinearity

Given a quadratic word equation $E$ with constants $A$ and variables
${V}=\\{x_{1},\ldots,x_{k}\\}$, its _length abstraction_ is defined as follows

$\text{{Len}}(E)=\\{(|{\sigma}(x_{1})|,\ldots,|{\sigma}(x_{k})|):\text{${\sigma}$
is a solution to $E$}\\},$

namely the set of tuples of numbers corresponding to lengths of solutions to
$E$.

###### Example 1

Consider the quadratic equation $E:=\ xaby=yz$, where ${V}=\\{x,y,z\\}$ and
$A$ contains at least two letters $a$ and $b$. We will show that its length
abstraction $\text{{Len}}(E)$ can be captured by the Presburger formula
$|x|=|y|+2$. Observe that each $(n_{x},n_{y},n_{z})\in\text{{Len}}(E)$ must
satisfy $n_{x}=n_{y}+2$ by a length argument on $E$. Conversely, we will show
that each triple $(n_{x},n_{y},n_{z})\in\mathbb{N}^{3}$ satisfying
$n_{x}=n_{y}+2$ must be in $\text{{Len}}(E)$. To this end, we will define a
solution ${\sigma}$ to $E$ such that
$(|{\sigma}(x)|,|{\sigma}(y)|,|{\sigma}(z)|)=(n_{x},n_{y},n_{z})$. Consider
${\sigma}(x)=a^{n_{x}}$. Let $n_{z}=q(n_{x}+2)+r$ for some $q\in\mathbb{N}$
and $r\in[n_{x}+1]$. Let $w$ be a prefix of ${\sigma}(x)$ of length $r$.
Define ${\sigma}(z)={\sigma}(x)^{q}w$. Therefore, ${\sigma}(z)$ is a prefix of
${\sigma}(x)ab{\sigma}(z)$. That is, for some $v\in A^{*}$, it is the case
that ${\sigma}(z)v={\sigma}(x)ab{\sigma}(z)$. Letting ${\sigma}(y)=v$ suffices
to make ${\sigma}$ satisfy $E$. Also,
$|{\sigma}(y)|=|{\sigma}(x)ab{\sigma}(z)|-|{\sigma}(z)|=|{\sigma}(x)|+2$,
which satisfies the formula $|x|=|y|+2$. ∎

However, it turns out that Presburger Arithmetic is not sufficient for
capturing length abstractions of quadratic word equations.

###### Theorem 3.1

There is a quadratic word equation whose length abstraction is not Presburger-
definable.

To this end, we show that the length abstraction of $xaby=yabx$, where $a,b\in
A$ and $x,y\in{V}$, is not Presburger definable.

###### Lemma 1

The length abstraction $\text{{Len}}(xaby=yabx)$ coincides with tuples
$(|x|,|y|)$ of numbers satisfying the expression $\varphi(|x|,|y|)$ defined
as:

$\displaystyle|x|=|y|$ $\displaystyle\vee$ $\displaystyle(|x|=0\wedge|y|\equiv
0\pmod{2})\vee(|y|=0\wedge|x|\equiv 0\pmod{2})$ $\displaystyle\vee$
$\displaystyle(|x|,|y|>0\wedge\gcd(|x|+2,|y|+2)>1)$

Observe that this would imply non-Presburger-definability: for otherwise,
since the first three disjuncts are Presburger-definable, the last disjunct
would also be Presburger-definable, which is not the case since the property
that two numbers are relatively prime is not Presburger-definable. Note
however, that the expression is definable in existential Presburger arithmetic
with divisibility.

Let us prove this lemma. Let $S=\text{{Len}}(xaby=yabx)$. We first show that
given any numbers $n_{x},n_{y}$ satisfying $\varphi(n_{x},n_{y})$, there are
solutions ${\sigma}$ to $xaby=yabx$ with ${\sigma}(\alpha)=n_{\alpha}$ for
each $\alpha\in\\{x,y\\}$. If they satisfy the first disjunct in $\varphi$
(i.e. $n_{x}=n_{y}$), then set ${\sigma}(x)={\sigma}(y)$ to an arbitrary word
$w\in A^{n_{x}}$. If they satisfy the second disjunct, then $aby=yab$ and so
set ${\sigma}(x)=\epsilon$ ${\sigma}(y)\in(ab)^{*}$. The same goes with the
third disjunct. For the fourth disjunct (assuming the first three disjuncts
are false), let $d=\gcd(n_{x}+2,n_{y}+2)$. Define
${\sigma}(x),{\sigma}(y)\in(a^{d-1}b)^{*}(a^{d-2})$ so that
$|{\sigma}(\alpha)|=n_{\alpha}$ for $\alpha\in{V}$. It follows that
${\sigma}(x)ab{\sigma}(y)={\sigma}(y)ab{\sigma}(x)$.

We now prove the converse. So, we are given a solution ${\sigma}$ to
$xaby=yabx$ and let $u:={\sigma}(x)$, $v:={\sigma}(y)$. Assume to the contrary
that $\varphi(|u|,|v|)$ is false and that $u$ and $v$ are the shortest such
solutions. We have several cases to consider:

  * •

$u=v$. Then, $|u|=|v|$, contradicting that $\varphi(|u|,|v|)$ is false.

  * •

$u=\epsilon$. Then, $abv=vab$ and so $v\in(ab)^{*}$, which implies that
$|v|\equiv 0\pmod{2}$. Contradicting that $\varphi(|u|,|v|)$ is false.

  * •

$v=\epsilon$. Same as previous item and that $|u|\equiv 0\pmod{2}$.

  * •

$|u|>|v|>0$. Since $\varphi(|u|,|v|)$ is false, we have $\gcd(|u|+2,|v|+2)=1$.
It cannot be the case that $|u|=|v|+1$ since then, comparing prefixes of
$uabv=vabu$, the letter at position $|u|+2$ would be $b$ on l.h.s. and $a$ on
r.h.s., which is a contradiction. Therefore $|u|\geq|v|+2$. Let
$u^{\prime}=u[|v|+3,|u|]$, i.e., $u$ but with its prefix of length $|v|+2$
removed. By Nielsen transformation, we have $u^{\prime}abv=vabu^{\prime}$. It
cannot be the case that $u^{\prime}=\epsilon$; for, otherwise, $abv=vab$
implies $v\in(ab)^{*}$ and so $u=vab$, implying that 2 divides both $|u|+2$
and $|v|+2$, contradicting that $\gcd(|u|+2,|v|+2)=1$. Therefore,
$|u^{\prime}|>0$. Since $\gcd(|u^{\prime}|+2,|v|+2)=\gcd(|u|+2,|v|+2)=1$, we
have a shorter solution to $xaby=yabx$, contradicting minimality.

  * •

$|v|>|u|>0$. Same as previous item.

##  4 Reduction to Counter Systems

In this section, we will provide an algorithm for computing a counter system
from $(E,S)$, where $E$ is a quadratic word equation and $S$ is a set of
regular constraints. We will first describe this algorithm for the case
without regular constraints, after which we show the extension to the case
with regular constraints.

Given the quadratic word equation $E$, we show how to compute a counter system
$\mathcal{C}(E)=(X,Q,\Delta)$ such that the following theorem holds.

###### Theorem 4.1

The length abstraction of $E$ coincides with
$pre_{\mathcal{C}(E)}^{*}(\\{\epsilon=\epsilon\\}\times\mathbb{N}^{|{V}|})$.

Before defining $\mathcal{C}(E)$, we define some notation. Define the
following formulas:

  * •

$\text{{ID}}(\bar{x},\bar{x}^{\prime}):=\bigwedge_{x\in\bar{x}}x^{\prime}=x$

  * •

$\text{{SUB}}_{y,z}(\bar{x},\bar{x}^{\prime}):=z\leq y\wedge
y^{\prime}=y-z\wedge\bigwedge_{x\in\bar{x},x\neq y}x^{\prime}=x$

  * •

$\text{{DEC}}_{y}(\bar{x},\bar{x}^{\prime}):=y>0\wedge
y^{\prime}=y-1\wedge\bigwedge_{x\in\bar{x},x\neq y}x^{\prime}=x$

Note that the $\neq$ symbol in the guard of $\bigwedge$ denotes syntactic
equality (i.e. not equality in Preburger Arithmetic). We omit mention of the
free variables $\bar{x}$ and $\bar{x}^{\prime}$ when they are clear from the
context.

We now define the counter system. Given a quadratic word equation $E$ with
constants $A$ and variables ${V}$, we define a counter system
$\mathcal{C}(E)=(X,Q,\Delta)$ as follows. The counters $X$ will be precisely
all variables that appear in $E$, i.e., $X:={V}$. The control states are
precisely all equations $E^{\prime}$ that can be rewritten from $E$ using
Nielsen transformation, i.e.,
$Q:=\\{E^{\prime}:E\Rightarrow^{*}E^{\prime}\\}$. The set $Q$ is finite (at
most exponential in $|E|$) as per our discussion in the previous section.

We now define the transition relation $\Delta$. We use $\bar{x}$ to enumerate
${V}$ in some order. Given $E_{1}\Rightarrow E_{2}$ with $E_{1},E_{2}\in Q$,
we then add the transition $(E_{1},\Phi(\bar{x},\bar{x}^{\prime}),E_{2})$,
where $\Phi$ is defined as follows:

  * •

If $E_{1}\Rightarrow E_{2}$ applies a rule for erasing an empty prefix
variable $y\in\bar{x}$, then $\Phi:=y=0\wedge\text{{ID}}$.

  * •

If $E_{1}\Rightarrow E_{2}$ applies a rule for removing a nonempty prefix:

    * –

If (P1) is applied, then $\Phi=\text{{ID}}$.

    * –

If (P2) is applied, then $\Phi=\text{{DEC}}_{\beta}$.

    * –

If (P3) is applied, then $\Phi=\text{{DEC}}_{\alpha}$.

    * –

If (P4) is applied and $\alpha\preceq\beta$, then
$\Phi=\text{{SUB}}_{\beta,\alpha}$. If $\beta\preceq\alpha$, then
$\Phi=\text{{SUB}}_{\alpha,\beta}$.

Observe that if $(E_{1},\text{\rm v}_{1})\to(E_{2},\text{\rm v}_{2})$, then
$|E_{1}|\leq|E_{2}|$ and $\text{\rm v}_{1}\preceq\text{\rm v}_{2}$. In
addition, if $\text{\rm v}_{1}=\text{\rm v}_{2}$, then $|E_{1}|<|E_{2}|$. This
implies the following lemma.

###### Lemma 2

The counter system $\mathcal{C}(E)$ terminates from every configuration
$(E_{0},\text{\rm v}_{0})$.

The proof of Theorem 4.1 immediately follows from Proposition 3 that Nielsen
transformation generates all solutions.

#### Extension to the case with regular constraints:

In this extension, we will only need to assert that the counter values belong
to the length abstractions of the regular constraints, which are effectively
semilinear due to Parikh’s Theorem [29]. Given a quadratic word equation $E$
with a set $S$ of regular constraints, we define the counter system
$\mathcal{C}(E,S)=(X,Q,\Delta)$ as follows. Let
$\mathcal{C}(E)=(X_{1},Q_{1},\Delta_{1})$. Let $X=X_{1}$. Let $Q$ be the
finite set of all configurations reachable from $(E,S)$, i.e.,
$Q=\\{(E^{\prime},S^{\prime}):(E,S)\Rightarrow^{*}(E^{\prime},S^{\prime})\\}$.
Given $(E_{1},S_{1})\Rightarrow(E_{2},S_{2})$, we add the transition
$((E_{1},S_{2}),\Phi(\bar{x},\bar{x}^{\prime}),(E_{2},S_{2}))$ as follows.
Suppose that $(E_{1},\Phi^{\prime}(\bar{x},\bar{x}^{\prime}),E_{2})$ was added
to $\Delta_{1}$ by $E_{1}\Rightarrow E_{2}$. Then,

$\Phi^{\prime}:=\Phi\wedge\bigwedge_{x\in\bar{x}}\left(x\in\text{{Len}}(\bigcap_{(x\in
L)\in S}L)\wedge x^{\prime}\in\text{{Len}}(\bigcap_{(x\in L)\in
S^{\prime}}L)\right).$

The size of the NFA for $\bigcap_{(x\in L)\in S}L$ is exponential in the
number of constraints of the form $(x\in L)$ in $S$ (of which there are
polynomially many). The constraint $x\in\text{{Len}}(L)$ is well-known to be
effectively semilinear [29], and in fact we can compute using the algorithm of
Chrobak-Martinez [9, 27, 30] in polynomial time two finite sets $A,A^{\prime}$
of integers and an integer $b$ such that, for each $n\in\mathbb{N}$, $n\in
U:=A\cup(A^{\prime}+b\mathbb{N})$ is true iff $n\in\text{{Len}}(L)$. Note that
$U$ is a fintie union of arithmetic progressions (with period 0 and/or $b$).
In fact, each number $a\in A\cup A^{\prime}$ (resp. the number $b$) is at most
quadratic in the size of the NFA, and so it is a polynomial 222Note that we
mean polynomial in the size of the NFA, which can be exponential in $|S|$.
size even when they are written in unary. Therefore, treating $U$ as an
existential Presburger formula $\varphi(x)$ with one free variable (an
existential quantifier is needed to guess the coefficient $n$ such that
$x=a_{i}+bn$ for some $i$), the resulting $\Phi^{\prime}$ is a polynomial-
sized existential Presburger formula.

###### Theorem 4.2

The length abstraction of $(E,S)$ coincides with
$pre_{\mathcal{C}(E,S)}^{*}(\\{(\epsilon=\epsilon,\emptyset)\\}\times\mathbb{N}^{|{V}|})$.

As for the case without regular constraints, the proof of Theorem 4.1
immediately follows from Proposition 3 that Nielsen transformation generates
all solutions.

##  5 Decidability via Linear Arithmetic with Divisibility

###  5.1 Accelerating a 1-variable-reducing cycle

Consider a counter system $\mathcal{C}=(X,Q,\Delta)$ with
$X=\\{q_{0},\ldots,q_{n-1}\\}$, and for some $y\in X$ the transition relation
$\Delta$ consists of precisely the following transition
$(q_{i},\Phi_{i},q_{i+1\pmod{n}})$, for each $i\in[n-1]$, such that $\Phi_{i}$
is either $\text{{SUB}}_{y,z}$ (with $z$ a variable distinct from $y$) or
$\text{{DEC}}_{y}$. Such a counter system is said to be a 1-variable-reducing
cycle.

###### Lemma 3

There exists a polynomial-time algorithm which given a 1-variable-reducing
cycle $\mathcal{C}=(X,Q,\Delta)$ and two states $p,q\in Q$ computes an formula
$\varphi_{p,q}(\bar{x},\bar{x}^{\prime})$ in existential Presburger with
divisibility such that $(p,\text{\rm v})\to_{\mathcal{C}}^{*}(q,\text{\rm w})$
iff $\varphi_{p,q}(\text{\rm v},\text{\rm w})$ is satisfiable.

This lemma can be seen as a special case of the acceleration lemma for flat
parametric counter automata [7] (where all variables other than $y$ are
treated as parameters). However, its proof is in fact quite simple. Without
loss of generality, we assume that $q=q_{0}$ and $p=q_{i}$, for some
$i\in\mathbb{N}$. Any path $(q_{0},\text{\rm
v})\to_{\mathcal{C}}^{*}(q_{i},\text{\rm w})$ can be decomposed into the cycle
$(q_{0},\text{\rm v})\to^{*}(q_{0},\text{\rm v}^{\prime})$ and the simple path
$(q_{0},\text{\rm w}_{0})\to\cdots\to(q_{i},\text{\rm w}_{i})$ of length $i$.
Therefore, the reachability relation $(q_{0},\text{\rm
x})\to_{\mathcal{C}}^{*}(q_{i},\text{\rm y})$ can be expressed as

$\exists\text{\rm z}_{0},\cdots,\text{\rm
z}_{i-1}:\varphi_{q_{0},q_{0}}(\text{\rm x},\text{\rm
z}_{0})\wedge\Phi_{0}(\text{\rm z}_{0},\text{\rm
z}_{1})\wedge\cdots\wedge\Phi_{i-1}(\text{\rm z}_{i-1},\text{\rm y}).$

Thus, it suffices to show that $\varphi_{q_{0},q_{0}}(\text{\rm x},\text{\rm
x}^{\prime})$ is expressible in $\mathcal{PAD}$. Define a multiset $M$ of
counter decrements as follows:

  * •

The number of the integer constant 1 $M$ can contain is defined as the number
of $i$ such that $\Phi_{i}=\text{{DEC}}_{y}$.

  * •

For each variable $x\in{V}\setminus\\{y\\}$, the number of times $x$ could
appear in $M$ is defined as the number of $i$ such that
$\Phi_{i}=\text{{SUB}}_{y,x}$.

For any variable/constant $e$, we will write $M(e)$ to denote the number of
times $e$ appears in $M$. Therefore, for some $n\in\mathbb{N}$ we have
$y^{\prime}=y-n\sum_{e}M(e)$, or equivalently

$n\sum_{e}M(e)=y-y^{\prime}$

The formula $\varphi_{q_{0},q_{0}}$ can be defined as follows:

$\varphi_{q_{0},q_{0}}:=\ \left(\sum_{e}M(e)\right)\mid(y-y^{\prime})\wedge
y^{\prime}\leq y\wedge\bigwedge_{x\in{V}\setminus\\{y\\}}x^{\prime}=x.$

Handling unary Presburger guards:  Recalling our reduction for the case with
regular constraints from Section 4 reveals that we also need unary Presburger
guards on the counters. We will show how to extend our aforementioned
acceleration lemma to handle such guards. As we will see shortly, we will need
a bit of the theory of semilinear sets.

As before, our counter system $\mathcal{C}=(X,Q,\Delta)$ has counters
$X=\\{q_{0},\ldots,q_{n-1}\\}$, and the control structure is a simple cycle of
length $n$, i.e., the transitions in $\Delta$ are precisely
$(q_{i},\Phi_{i},q_{i+1\pmod{n}})$ for some Presburger formula
$\Phi_{i}(\bar{x},\bar{x}^{\prime})$, for each $i\in[n-1]$. We say that
$\mathcal{C}$ is 1-variable-reducing with unary Presburger guards if there
exists a counter $y\in X$ such that each $\Phi_{i}$ is of the form
$\theta_{i}\wedge\psi_{i}$, where $\theta_{i}$ is either $\text{{SUB}}_{y,z}$
(with $z$ a variable distinct from $y$) or $\text{{DEC}}_{y}$, and $\psi_{i}$
is a conjunction of formulas of the form $x\in
A_{i}\cup(A_{i}^{\prime}+b\mathbb{N})$, where both $A_{i}$ and
$A_{i}^{\prime}$ are finite sets of natural numbers and $x\in X$. For each
counter $x\in X$, we use $\psi_{i,x}$ to denote the set of conjuncts in
$\psi_{i}$ that refers to the counter $x$.

###### Lemma 4

There exists a polynomial-time algorithm which given a 1-variable-reducing
cycle with unary Presburger guards $\mathcal{C}=(X,Q,\Delta)$ and two states
$p,q\in Q$ computes an formula $\lambda_{p,q}(\bar{x},\bar{x}^{\prime})$ in
existential Presburger with divisibility such that $(p,\text{\rm
v})\to_{\mathcal{C}}^{*}(q,\text{\rm w})$ iff $\lambda_{p,q}(\text{\rm
v},\text{\rm w})$ is satisfiable.

Unlike Lemma 3, this lemma does not immediately follow from the results of [7]
on flat parametric counter automata. To prove this, let us first take the
formula $\varphi_{p,q}(\bar{x},\bar{x}^{\prime})$ from Lemma 3 applied to
$\mathcal{C}^{\prime}$, which is obtained from $\mathcal{C}$ by first removing
the unary Presburger guards. We can insert these unary Presburger guards to
$\varphi_{p,q}$, but this is not enough because we need to make sure that all
“intermediate” values of $y$ have to also satisfy the Presburger guards
corresponding to $y$ on that control state. More precisely, let the counter
decrement in $\theta_{i}$ be $\alpha_{i}$ (which can either be a variable $x$
distinct from $y$ or 1). For $j\in[n-1]$, we use $f_{j}(\bar{x})$ to denote
$\sum_{i=0}^{j}\alpha_{i}$. Write $f(\bar{x})$ for $f_{n-1}(\bar{x})$. Then,
we can write

$\displaystyle\lambda_{q_{0},q_{0}}$ $\displaystyle:=$
$\displaystyle\bar{x}^{\prime}=\bar{x}\vee\left(\varphi_{q_{0},q_{0}}\wedge\bigwedge_{i=0}^{n-1}\psi_{i}(\bar{x})\wedge\eta_{q_{0},q_{0}}\right)$
$\displaystyle\eta_{q_{0},q_{0}}$ $\displaystyle:=$ $\displaystyle\forall
k:y^{\prime}+(k+1)f(\bar{x})\leq y\longrightarrow$
$\displaystyle\quad\left(\bigwedge_{i=0}^{n-1}\bigwedge_{(\alpha_{i}\in A\cup
A^{\prime}+b\mathbb{N})\in\psi_{i,y}}y^{\prime}+kf(\bar{x})+\alpha_{i}\in
A\cup(A^{\prime}+b\mathbb{N})\right)$

This is a correct expression that captures the reachability relation
$(q_{0},\text{\rm w})\to_{\mathcal{C}}^{*}(q_{0},\text{\rm w}^{\prime})$, but
the problem is that it has a universal quantifier and therefore is not a
formula of $\mathcal{PAD}$. To fix this problem, we will need to exploit the
semilinear structure of unary Presburger guards. To this end, we first notice
that, by taking the big conjunction over $i$ and the big conjuncton over
$\alpha_{i}$ out, the formula $\eta_{q_{0},q_{0}}$ is equivalent to:

$\displaystyle\eta_{q_{0},q_{0}}$ $\displaystyle\equiv$
$\displaystyle\bigwedge_{i=0}^{n-1}\bigwedge_{(\alpha_{i}\in A\cup
A^{\prime}+b\mathbb{N})\in\psi_{i,y}}\forall k:y^{\prime}+(k+1)f(\bar{x})\leq
y\longrightarrow$ $\displaystyle\quad(y^{\prime}+kf(\bar{x})+\alpha_{i}\in
A\cup(A^{\prime}+b\mathbb{N}))$

Therefore, it suffices to rewrite each conjunct $C(\bar{x}):=\forall
k:y^{\prime}+(k+1)f(\bar{x})\leq
y\longrightarrow\quad(y^{\prime}+kf(\bar{x})+\alpha_{i}\in
A\cup(A^{\prime}+b\mathbb{N})$ as an existential Presburger formula, for each
$i$ and constraint $(\alpha_{i}\in A\cup A^{\prime}+b\mathbb{N})$. To this
end, let $a:=\max A$ and let $N$ denote $|A^{\prime}|$. We claim that

$\displaystyle C(\bar{x})$ $\displaystyle\equiv$
$\displaystyle\bigwedge_{i=0}^{a}y^{\prime}+if(\bar{x})+\alpha_{i}\leq y\to
y^{\prime}+if(\bar{x})+\alpha_{i}\in A\cup(A^{\prime}+b\mathbb{N})$
$\displaystyle\wedge\bigwedge_{i=a+1}^{a+N+1}y^{\prime}+if(\bar{x})+\alpha_{i}\leq
y\to y^{\prime}+if(\bar{x})+\alpha_{i}\in A^{\prime}+b\mathbb{N}.$

Simply put, we distinguish the cases when $y^{\prime}+if(\bar{x})+\alpha_{i}$
is “small” (i.e., less than the maximum threshold that can keep this number in
an arithmetic progression with 0 period), and when this number is “big” (i.e.
must be in an arithmetic progression with a nonzero period). To prove this
equivalence, it suffices to show that if
$y^{\prime}+kf(\bar{x})+\alpha_{i}\notin A\cup(A^{\prime}+b\mathbb{N})$ with
$k>a+N+1$ and $y^{\prime}+kf(\bar{x})+\alpha_{i}\leq y$, then we can find
$k^{\prime}\leq a+N+1$ such that
$y^{\prime}+k^{\prime}f(\bar{x})+\alpha_{i}\notin
A\cup(A^{\prime}+b\mathbb{N})$. Suppose to the contrary that such $k^{\prime}$
does not exist. Then, since there are $N+1$ numbers in between $a+1$ and
$a+N+1$, by pigeonhole principle there is an arithmetic progression
$a^{\prime}+b\mathbb{N}$ and two different numbers $a+1\leq j_{1}<j_{2}\leq
a+N+1$ such that $y^{\prime}+j_{h}f(\bar{x})+\alpha_{i}\in
a^{\prime}+b\mathbb{N}$, for $h=1,2$. Let $d:=(j_{2}-j_{1})$. Note that
$df(\bar{x})$ denotes the difference between
$y^{\prime}+j_{1}f(\bar{x})+\alpha_{i}$ and
$y^{\prime}+j_{2}f(\bar{x})+\alpha_{i}$, and this difference is of the form
$mb$, for some positive integer $m$. We now find a number $j\in[a+1,a+N]$ with
$j+qd=k$ for some positive integer $q$. Since
$y^{\prime}+jf(\bar{x})+\alpha_{i}\in a^{\prime\prime}+b\mathbb{N}$ for some
$a^{\prime\prime}\in A^{\prime}$, it must be the case that
$y^{\prime}+(j+qd)f(\bar{x})+\alpha_{i}\in a^{\prime\prime}+b\mathbb{N}$ for
$q\in\mathbb{N}$, contradicting that $y^{\prime}+kf(\bar{x})+\alpha_{i}\notin
A\cup(A^{\prime}+b\mathbb{N})$.

We have proven correctness, and what remains is to analyse the size of the
formula $\lambda_{q_{0},q_{0}}$. To this end, it suffices to show that each
formula $C(\bar{x})$ is of polynomial size. This is in fact the case since
there are at most polynomially many numbers in $A$ and $A^{\prime}$ and that
the size of all numbers in $A\cup A^{\prime}\cup\\{b\\}$ are of polynomial
size even when they are written in unary.

###  5.2 An extension to flat control structures and an acceleration scheme

The following generalisation to flat control structures is an easy corollary
of Lemma 3 and 4.

###### Theorem 5.1

There exists a polynomial-time algorithm which, given a flat Presburger
counter system $\mathcal{C}=(X,Q,\Delta)$, each of whose simple cycle is
1-variable-reducing with unary Presburger guards and two states $p,q\in Q$,
computes an formula $\lambda_{p,q}(\bar{x},\bar{x}^{\prime})$ in existential
Presburger with divisibility such that $(p,\text{\rm
v})\to_{\mathcal{C}}^{*}(q,\text{\rm w})$ iff $\lambda_{p,q}(\text{\rm
v},\text{\rm w})$ is satisfiable.

Indeed, to prove this theorem, we can simply use Lemma 4 to accelerate all
cycles and the fact that transition relations expressed in existential
Presburger with divisibility is closed under composition.

###  5.3 Application to word equations with length constraints

Theorem 5.1 gives rise to a simple and sound (but not complete) technique for
solving quadratic word equations with length constraints: given a quadratic
word equation $(E,S)$ with regular constraints, if the counter system
$\mathcal{C}(E,S)$ is flat, each of whose simple cycle is 1-variable-reducing
with unary Presburger guards, then apply the decision procedure from Theorem
5.1. In this section, we show completeness of this method for the class of
regular-oriented word equations recently defined in [11], which can be
extended with regular constraints given as 1-weak NFA [2]. A word equation is
regular if each variable $x\in{V}$ occurs at most once on each side of the
equation. Observe that $xy=yx$ is regular, but $xxyy=zz$ is not. It is easy to
see that a regular word equation is quadratic. A word equation $L=R$ is said
to be oriented if there is a total ordering $<$ on ${V}$ such that the
occurrences of variables on each side of the equation preserve $<$, i.e., if
$w=L$ or $w=R$ and $w=w_{1}\alpha w_{2}\beta w_{3}$ for some
$w_{1},w_{2},w_{3}\in(A\cup{V})^{*}$ and $\alpha,\beta\in{V}$, then
$\alpha<\beta$. Observe that $xy=yz$ (i.e. that $x$ and $z$ are conjugates) is
oriented, but $xy=yx$ is not oriented. It was shown in [11] that the
satisfiability for regular-oriented word equations is NP-hard. We show
satisfiability for this class with length constraints is decidable.

###### Theorem 5.2

The satisfiability problem of regular-oriented word equations with length
constraints is decidable in nondeterministic exponential time.

This decidability (in fact, an NP upper bound) for the _strictly regular-
ordered_ subcase (i.e. each variable occurs precisely once on each side) was
proven in [10]. For solving this subcase, it was shown that Presburger
Arithmetic is sufficient, but the decidability for the general class of
regular-oriented word equations with length constraints remains open, which we
prove in this paper.

###### Lemma 5

Given a regular-oriented word equation $E$, the counter system
$\mathcal{C}(E)$ is flat. Moreover, the length of each simple cycle (resp.
path) in the control structure of $\mathcal{C}(E)$ is of length $O(|E|)$
(resp. $O(|E|^{2})$).

Before proving this lemma, we show a simple lemma that $\Rightarrow$ preserves
regular-orientedness. Its proof can be found in the appendix.

###### Lemma 6

If $E\Rightarrow E^{\prime}$ and $E$ is regular-oriented, then $E^{\prime}$ is
also regular-oriented.

We now prove Lemma 5. Let $E:=L=R$. We first show that the length of a simple
cycle in the control structure of $\mathcal{C}(E)$ is of length at most
$N=\max\\{|L|,|R|\\}-1$. Given a simple cycle $E_{0}\Rightarrow
E_{1}\Rightarrow\cdots\Rightarrow E_{n}$ with $n>0$ (i.e. $E_{0}=E_{n}$ and
$E_{i}\neq E_{j}$ for all $0\leq i<j<n$), it has to be the case that each
rewriting in this cycle applies one of the (P2)–(P4) rules since the other
rules reduce the size of the equation. We have
$|E_{0}|=|E_{1}|=\cdots=|E_{n}|$. Let $E_{i}:=L_{i}=R_{i}$ with
$L_{i}=\alpha_{i}w_{i}$ and $R_{i}=\beta_{i}w_{i}^{\prime}$. Let us assume
that $E_{1}=E_{0}[\alpha_{0}\beta_{0}/\beta_{0}]$; the case with
$E_{1}=E_{0}[\beta_{0}\alpha_{0}/\alpha_{0}]$ will be easily seen to be
symmetric. This assumption implies that $\beta_{0}$ is a variable $y$, and
that $L_{0}=uyv$ for some words $u,v\in(A\cup{V})^{*}$ (for, otherwise,
$|E_{1}|<|E_{0}|$). Furthermore, it follows that, for each $i\in[n-1]$,
$E_{i+1}=E_{i}[\beta_{i}\alpha_{i}/\beta_{i}]$, i.e., the counter system
$\mathcal{C}(E)$ applies either $\text{{SUB}}_{y,x}$ (in the case when
$x=\alpha_{i}$) or $\text{{DEC}}_{y}$ (in the case when $\alpha_{i}\in A$).
For, otherwise, taking a minimal $i\in[1,n-1]$ with
$E_{i}[\beta_{i}\alpha_{i}/\alpha_{i}]$ for some variable $x=\alpha_{i}$ shows
that $E_{i}$ is of the form $x...y...=y...x...$ (since $|E_{i+1}|=|E_{i}|$)
contradicting that $E_{i}$ is oriented. Consequently, we have

  * •

$R_{i}=R_{j}$ for all $i,j$, and

  * •

$L_{i}=\mathrm{cyc}^{i}(u)yv$ for all $i\in[n]$

implying that the length of the cycle is at most $|R_{0}|-1\leq|R|-1$.

Consider the control structure $\mathcal{C}(E)$ as a dag of SCCs. In this dag,
each edge from one SCC to the next is size-reducing. Therefore, the maximal
length of a path in this dag is $|E|$. Therefore, since the maximal path of
each SCC is $N$ (from the above analysis), the maximal length of a simple path
in the control structure is at most $N^{2}$.

Handling regular constraints:  It is difficult to extend Theorem 5.2 to the
case with regular constraints because they may introduce nestings of cycles
(which breaks the flat control structure) even for regular-oriented word
equation. However, we can show that restricting to regular constraints given
by 1-weak NFA [2] (i.e. a dag of SCCs, each with at most one state) preserves
the flat control structure. The class of 1-weak automata is in fact quite
powerful, e.g., when considered as recognisers of languages of $\omega$-words,
they capture the subclass of LTL with operators F and G [2]. They have also
been used to obtain a decidable extension of infinite-state concurrent systems
in term rewriting systems, e.g., see [20, 31]. In the context of quadratic
word equations, we can use 1-weak NFA to capture the regular constraint
$x,y\in\\#(a+b)^{*}$, which in conjunction with $xy=yz$ gives rise a non-
Presburger length abstraction. Such an NFA will have two states $q_{0}$ and
$q_{1}$, and transitions
$q_{0}\stackrel{{\scriptstyle\\#}}{{\longrightarrow}}q_{1}$ and
$q_{1}\stackrel{{\scriptstyle a,b}}{{\longrightarrow}}q_{1}$, where $q_{0}$ is
an initial state and $q_{1}$ a final state.

###### Theorem 5.3

The satisfiability problem of regular-oriented word equations with 1-weak
regular constraints and length constraints is solvable in nondeterministic
double exponential time (2NEXP).

Let us prove this theorem. Suppose $E$ is a regular-oriented word equation
with the set $S$ of 1-weak regular constraints. Let
$\mathcal{C}(E,S)=(X,Q,\Delta)$ be the corresponding counter system. Let
$M(S)$ denote the maximum number of states ranging over all NFA in $S$.

###### Lemma 7

The counter system $\mathcal{C}(E,S)$ is flat. Moreover, the length of each
simple cycle in the control structure of $\mathcal{C}(E,S)$ is of length
$O(|E|)$, while the length of each simple path is of length
$O(|E|^{2}|\mathcal{V}||S|M^{3})$.

By virtue of Theorem 5.1, this lemma implies decidability of Theorem 5.3, but
it does NOT imply the nondeterministic exponential time upper bound since each
unary Presburger guard in $\mathcal{C}(E)$ will be of the form
$x\in\text{{Len}}(\bigcap_{(x\in L)\in S}L)$. Even though we know that $|S|$
is always of a polynomial size, their intersection requires performing a
product automata construction, which will result in an NFA of an exponential
size. Therefore, we obtain a nondeterministic double exponential time
complexity upper bound (2NEXP), instead of NEXP as for the case without
regular constraints. The proof of Lemma 7 can be found in the appendix.

###### Remark 1

Our proof of Theorem 5.3 does not extend to the case when we allow
_generalised flat_ NFA (i.e. after mapping all the letters in $A$ to a new
symbol ’?’, the control structure of the NFA is flat) in the regular
constraints. This is because a simple cycle involving two or more states will
result in a counter system that is no longer flat.

Finally, we mention that the length abstraction of regular-oriented word
equations with regular constraints is in general not Presburger-definable (see
appendix for proof).

###### Proposition 4

The regular-oriented word equation $xy=yz$ with regular constraints
$x,y\in\\#(a+b)^{*}$ has non-Presburger-definable length abstraction.

##  6 Future Work

One obvious research direction is to study extensions of our techniques to
deal with the class of regular (but not necessarily oriented) word equations
with length constraints. We believe that this is a key subproblem of the
general class of quadratic word equations with length constraints. Finally, we
conjecture that the length abstractions of general quadratic word equations
with regular constraints can be effectively captured by existential Presburger
with divisibility.

##### Acknowledgment.

We thank Artur Jeż for the constructive feedback and his lecture notes on word
equations. We thank Dmitry Chistikov, Matthew Hague, Philipp Rümmer, and James
Worrell for the helpful discussions.

## References

  * [1] P. A. Abdulla, M. F. Atig, Y. Chen, L. Holík, A. Rezine, P. Rümmer, and J. Stenman.  String constraints for verification.  In CAV, pages 150–166, 2014.
  * [2] T. Babiak, V. Rehák, and J. Strejcek.  Almost linear Büchi automata.  Mathematical Structures in Computer Science, 22(2):203–235, 2012\.
  * [3] D. Balzarotti, M. Cova, V. Felmetsger, N. Jovanovic, E. Kirda, C. Kruegel, and G. Vigna.  Saner: Composing static and dynamic analysis to validate sanitization in web applications.  In S&P, pages 387–401, 2008.
  * [4] S. Bardin, A. Finkel, J. Leroux, and L. Petrucci.  FAST: acceleration from theory to practice.  STTT, 10(5):401–424, 2008.
  * [5] S. Bardin, A. Finkel, J. Leroux, and P. Schnoebelen.  Flat acceleration in symbolic model checking.  In ATVA, pages 474–488, 2005.
  * [6] N. Bjørner, N. Tillmann, and A. Voronkov.  Path feasibility analysis for string-manipulating programs.  In TACAS, pages 307–321, 2009.
  * [7] M. Bozga, R. Iosif, and Y. Lakhnech.  Flat parametric counter automata.  Fundam. Inform., 91(2):275–303, 2009.
  * [8] A. S. Christensen, A. Møller, and M. I. Schwartzbach.  Precise analysis of string expressions.  In SAS, pages 1–18, 2003.
  * [9] M. Chrobak.  Finite automata and unary languages.  Theor. Comput. Sci., 47(3):149–158, 1986.
  * [10] J. D. Day, V. Ganesh, P. He, F. Manea, and D. Nowotka.  The satisfiability of extended word equations: The boundary between decidability and undecidability.  CoRR, abs/1802.00523, 2018.
  * [11] J. D. Day, F. Manea, and D. Nowotka.  The hardness of solving simple word equations.  In MFCS, pages 18:1–18:14, 2017.
  * [12] V. Diekert.  Makanin’s Algorithm.  In M. Lothaire, editor, Algebraic Combinatorics on Words, volume 90 of Encyclopedia of Mathematics and its Applications, chapter 12, pages 387–442. Cambridge University Press, 2002.
  * [13] V. Diekert and J. M. Robson.  Quadratic word equations.  In Jewels are Forever, Contributions on Theoretical Computer Science in Honor of Arto Salomaa, pages 314–326, 1999.
  * [14] X. Fu and C. Li.  Modeling regular replacement for string constraint solving.  In NFM, pages 67–76, 2010.
  * [15] X. Fu, M. C. Powell, M. Bantegui, and C. Li.  Simple linear string constraints.  Formal Asp. Comput., 25(6):847–891, 2013.
  * [16] V. Ganesh, M. Minnes, A. Solar-Lezama, and M. Rinard.  Word equations with length constraints: what’s decidable?  In Hardware and Software: Verification and Testing, pages 209–226. Springer, 2013.
  * [17] L. Holík, P. Janku, A. W. Lin, P. Rümmer, and T. Vojnar.  String constraints with concatenation and transducers solved efficiently.  PACMPL, 2(POPL):4:1–4:32, 2018.
  * [18] A. Jéz.  Recompression: a simple and powerful technique for word equations.  In STACS 2013, LIPIcs, Vol. 20, pages 233–244, 2013.
  * [19] A. Kiezun et al.  HAMPI: A solver for word equations over strings, regular expressions, and context-free grammars.  ACM Trans. Softw. Eng. Methodol., 21(4):25, 2012.
  * [20] M. Kretínský, V. Rehák, and J. Strejcek.  Reachability is decidable for weakly extended process rewrite systems.  Inf. Comput., 207(6):671–680, 2009.
  * [21] A. Lechner, J. Ouaknine, and J. Worrell.  On the complexity of linear arithmetic with divisibility.  In LICS 15: Logic in Computer Science. IEEE, 2015.
  * [22] A. Lentin.  Equations dans les Monoides Libres.  Gauthier-Villars, Paris, 1972.
  * [23] J. Leroux and G. Sutre.  Flat counter automata almost everywhere!  In Software Verification: Infinite-State Model Checking and Static Program Analysis, 19.02. - 24.02.2006, 2006.
  * [24] T. Liang, A. Reynolds, C. Tinelli, C. Barrett, and M. Deters.  A DPLL(T) theory solver for a theory of strings and regular expressions.  In CAV, pages 646–662, 2014.
  * [25] L. Lipshitz.  The Diophantine problem for addition and divisibility.  Transactions of the American Mathematical Society, 235:271–283, 1976.
  * [26] G. S. Makanin.  The problem of solvability of equations in a free semigroup.  Sbornik: Mathematics, 32(2):129–198, 1977.
  * [27] A. Martinez.  Efficient computation of regular expressions from unary nfas.  In In DFCS, pages 174–187, 2002.
  * [28] Y. Matiyasevich.  A connection between systems of words-and-lengths equations and Hilbert’s tenth problem.  Zapiski Nauchnykh Seminarov POMI, 8:132–144, 1968.
  * [29] R. Parikh.  On context-free languages.  J. ACM, 13(4):570–581, 1966.
  * [30] A. W. To.  Unary finite automata vs. arithmetic progressions.  Inf. Process. Lett., 109(17):1010–1014, 2009.
  * [31] A. W. To and L. Libkin.  Algorithmic metatheorems for decidable LTL model checking over infinite systems.  In FOSSACS, 2010.
  * [32] M. Trinh, D. Chu, and J. Jaffar.  S3: A symbolic string solver for vulnerability detection in web applications.  In CCS, pages 1232–1243, 2014.
  * [33] H. Wang, T. Tsai, C. Lin, F. Yu, and J. R. Jiang.  String analysis via automata manipulation with logic circuit representation.  In CAV, pages 241–260, 2016.
  * [34] F. Yu, M. Alkhalaf, T. Bultan, and O. H. Ibarra.  Automata-based symbolic string analysis for vulnerability detection.  Formal Methods in System Design, 44(1):44–70, 2014.
  * [35] F. Yu, T. Bultan, and O. H. Ibarra.  Relational string verification using multi-track automata.  Int. J. Found. Comput. Sci., 22(8):1909–1924, 2011.
  * [36] Y. Zheng, X. Zhang, and V. Ganesh.  Z3-str: a Z3-based string solver for web application analysis.  In ESEC/SIGSOFT FSE, pages 114–124, 2013.

APPENDIX

##  Appendix 0.A Proof of Lemma 6

It is easy to see each rewriting rule preserves regularity. Now, because
$E^{\prime}$ is regular, to show that $E^{\prime}:=L=R$ is also oriented it is
sufficient and necessary to show that there are no two variables $x,y$ such
that $x$ occurs before $y$ in $L$, but $y$ occurs before $x$ in $R$. All
rewriting rules except for (P2)–(P4) are easily seen to preserve orientedness.
Let us write $E:=\alpha w_{1}=\beta w_{2}$ with $\alpha\neq\beta$, and assume
$E^{\prime}=E[\alpha\beta/\beta]$; the case of
$E^{\prime}=E[\beta\alpha/\alpha]$ is symmetric. So, $\beta$ is some variable
$y$. If $\beta$ does not occur in $w_{1}$, then $L=w_{1}$ and $R=\beta w_{2}$
and that $E$ is oriented implies that $E^{\prime}$ is oriented. So assume that
$\beta$ appears in $w_{1}$, say, $w_{1}=u\beta v$. Then, $R=\beta w_{2}$ and
$L=u\alpha\beta v$. Thus, if $\alpha\in A$, $E^{\prime}$ is oriented because
we can use the same variable ordering that witnesses that $E$ is oriented. So,
assume $\alpha\in{V}$. It suffices to show that $\alpha$ occurs _at most once_
in $E$. For, if $\alpha$ also occurs on the other side of the equation $E$
(i.e. in $w_{2}$), $\alpha$ precedes $\beta$ on l.h.s. of $E$, while $\beta$
precedes $\alpha$ on r.h.s. of $E$, which would show that $E$ is not oriented.

##  Appendix 0.B Proof of Lemma 7

Since $\mathcal{C}(E,S)$ is simply $\mathcal{C}(E)$ but annotated by the
regular constraints and how they are modified, it suffices to prove that each
SCC $G$ in the control structure of $\mathcal{C}(E)$ with nodes
$E_{1},\ldots,E_{m}$ the restrictions $\mathcal{C}^{\prime}$ of
$\mathcal{C}(E,S)$ to control states of the form $(E_{i},S)$, for some set $S$
of regular constraints, is a flat each of whose cycle is of length $O(|E|)$,
and each of whose simple path is of length at most
$O(|E||\mathcal{V}||S|M^{3})$. By Theorem 5.2, we know that $\mathcal{C}(E)$
is flat, each of whose simple cycle is 1-variable-reducing and is of length
$|E|$ and each of whose simple path over the dag of SCCs corresponding to the
control structure of $\mathcal{C}(E)$ is of length at most $O(|E|)$.
Therefore, we may assume that the SCC $G$ is a cycle $E_{1}\to\cdots\to E_{m}$
and there exists a counter $y$ which is reduced by each transition in $G$
using $\text{{SUB}}_{y,z}$ or $\text{{DEC}}_{y}$.

We will next define a partial order $\trianglerighteq$ on sets of regular
constraints of the form $x\in L(\mathcal{A}_{p,q})$, where $x\in{V}$ and
$\mathcal{A}$ is an NFA in $S$. We will write $S_{1}\triangleright S_{2}$ if
$S_{1}\trianglerighteq S_{2}$ but $S_{1}\neq S_{2}$. Before defining
$\trianglerighteq$, the intuition behind this partial order is that each
transition
$((E^{\prime},S^{\prime}),\Phi,(E^{\prime\prime},S^{\prime\prime}))$ in the
control structure $G^{\prime}$ of $\mathcal{C}^{\prime}$ will
$\trianglerighteq$-decrease $S^{\prime}$, i.e., $S^{\prime}\trianglerighteq
S^{\prime\prime}$. In particular, this implies that every simple cycle in
$G^{\prime}$ will consist of the nodes $(E_{1},H),\ldots,(E_{m},H)$ for some
set $H$ of regular constraints. Therefore, the length of each simple cycle in
$G^{\prime}$ is at most $O(|E|)$. Since we will see that the length a simple
path in $\trianglerighteq$ is at most $O(|\mathcal{V}||S|M^{3})$, it will
follow that the length of a simple path in $G^{\prime}$ is at most
$O(|E||\mathcal{V}||S|M^{3})$.

We write $S_{1}\trianglerighteq S_{2}$ if:

  * •

The number of regular constraints in $S_{2}$ on $y$ (i.e. of the form $y\in L$
for some $L$) is at most the number of regular constraints in $S_{1}$ on $y$.

  * •

For each variable $x$ distinct from $y$, if $x\in L$ is in $S_{1}$, then it is
also in $S_{2}$.

  * •

For each constraint $y\in\mathcal{L}(\mathcal{A}_{r,q})$ in $S_{2}$, there
exists a state $p$ that can reach $r$ in $\mathcal{A}$ such that the
constraint $y\in\mathcal{L}(\mathcal{A}_{p,q})$ is in $S_{1}$.

The fact that $\trianglerighteq$ is a partial order then follows from the fact
that each $\mathcal{A}$ is 1-weak, i.e., whose transition relation gives rise
to a partial order on the states of $\mathcal{A}$. To show that the length of
a simple path in $\trianglerighteq$ is at most $O(|\mathcal{V}||S|M^{3})$,
observe that we can add at most $|S|M^{2}$ regular constraints on $x$
(distinct from $y$). In addition, if the constraints on $y$ in some $S_{1}$
are

$y\in\mathcal{L}(\mathcal{A}_{p_{1},q_{1}}^{1}),\ldots,y\in\mathcal{L}(\mathcal{A}_{p_{K},q_{K}}^{K}),$

and if $k_{i}$ is the length of maximal simple path in
$\mathcal{A}_{p_{i},q_{i}}^{i}$, then one can change the set of constraints on
$y$ in $S_{1}$ to any $S_{2}\trianglelefteq S_{1}$ by at most
$\sum_{i=1}^{K}k_{i}=O(|S|M^{3})$. This proves that any simple path in
$\trianglerighteq$ is of length $O(|\mathcal{V}||S|M^{3})$.

##  Appendix 0.C Proof of Proposition 4

We claim that its length abstraction is precisely the set of triples
$(n_{x},n_{y},n_{z})\in\mathbb{N}^{3}$ satisfying the formula

$\varphi(l_{x},l_{y},l_{z}):=l_{x}=l_{y}\wedge l_{x}>0\wedge l_{x}\mid l_{z}.$

Since divisibility is not Presburger-definable, the theorem immediately
follows. To show that for each triple $\bar{n}=(n_{x},n_{y},n_{z})$ satisfying
$\varphi$ there exists a solution ${\sigma}$ to $E$ and the constraint
$x,y\in\\#(a+b)^{*}$, simply consider ${\sigma}$ with
${\sigma}(x)={\sigma}(y)=\\#a^{l_{x}-1}$, and
${\sigma}(z)={\sigma}(z)={\sigma}(x)^{n_{z}/n_{x}}$. Conversely, consider a
solution ${\sigma}$ satisfying $xz=zy$ and $x,y\in\\#(a+b)^{*}$. We must have
$x=y$ since two conjugates $x,y\in\\#(a+b)^{*}$ must apply a full cyclical
permutation, i.e., the same words. We then have
$|{\sigma}(x)|=|{\sigma}(y)|>0$. To show that
$|{\sigma}(x)|\mid|{\sigma}(z)|$, let $|{\sigma}(z)|=q|{\sigma}(x)|+r$ for
some $q\in\mathbb{N}$ and $r\in[|{\sigma}(x)|-1]$. It suffices to show that
$r=0$. To this end, matching both sides of $E$, we obtain $z=x^{q}w$, where
$w$ is a prefix of ${\sigma}(x)$ of length $r$. If $r>0$, then matching both
sides of the equation from the _right_ reveals that the last $|{\sigma}(y)|-1$
letters on l.h.s. of ${\sigma}(E)$ contains $\\#$, which is not the case on
r.h.s. of ${\sigma}(E)$, contradicting that ${\sigma}$ is a solution to $E$.
Therefore, $r=0$, proving the claim.


# Leveraging Evolutionary Algorithms for
Feasible Hexapod Locomotion Across Uneven Terrain

Jack Vice, Gita Sukthankar, and Pamela K. Douglas
University of Central Florida
Orlando, FL US

###### Abstract

> Optimizing gait stability for legged robots is a difficult problem. Even on
> level surfaces, effectively traversing across different textures (e.g.,
> carpet) rests on dynamically tuning parameters in multidimensional space.
> Inspired by biology, evolutionary algorithms (EA) remain an attractive
> solution for feasibly implementing robotic locomotion with both energetic
> economy and rapid parameter convergence. Here, we leveraged this class of
> algorithms to evolve a stable hexapod gait controller capable of traversing
> uneven terrain and obstacles. Gait parameters were evolved in a rigid body
> dynamics simulation on an 8 x 3 meter obstacle course comprised of random
> step field, linear obstacles and inclined surfaces. Using a fitness function
> that jointly optimized locomotion velocity and stability, we found that
> multiple successful gait parameter evolutions yielded specialized
> functionality for each leg. Specific gait parameters were identified as
> critical to developing a rough terrain gait.

## Introduction

Small and medium-sized mobile ground robots that operate in urban and rural
outdoor environments must cope with terrain that is uneven and cluttered with
obstacles. For traversing uneven terrain and scaling obstacles, legged
locomotion has several advantages over wheeled and tracked vehicles including
enabling omni-directional movement, scaling obstacles higher than the robot’s
center of gravity, avoiding contact with ground hazards, and fault tolerance.

For biological systems with legged locomotion, evolution by natural selection
has favored (in terms of species count) hexapods, which possess the inherent
stability of a tripod gait as well as the ability to articulate the front two
legs for climbing and manipulation tasks while maintaining a stable stance on
the rear four legs. Effective execution of a hexapod gait generally requires a
minimum of 18 degrees of freedom. Thus developing an agile and stable gait for
traversing randomly uneven terrain has a large search space that serves as a
good candidate problem for evolutionary algorithms, and the application of
evolutionary algorithms to the field of gait controller optimization has been
a subject of ongoing research (?; ?).

For legged robots on uneven surfaces, a closed loop gait controller that can
detect when and with what force the feet contact the ground, and dynamically
adjust to the uneven surface, will usually outperform open loop systems (?;
?). However an open loop gait for uneven surfaces is useful for many legged
robots which may not have ground contact sensing or motor force feedback.
Additionally, some common deformable surfaces, such as vegetation and litter,
do not provide ground contact certainty, requiring the use of an open loop
gait. This paper demonstrates a method for evolving an open loop hexapod gait
controller capable of traversing uneven terrain and obstacles and presents
results on a PhantomX hexapod simulated using the Open Dynamics Engine in
Gazebo.

Figure 1: Gazebo simulation environment. Obstructions include a random step
field on an incline and linear obstacles.

## Related Work

Evolutionary algorithms have been used to evolve flat surface forward gaits
for hexapods in the Open Dynamics Engine; for instance ? (?) demonstrated the
usage of an evolutionary algorithm in which fitness based selection and
crossover was replaced by population density based reproduction. Real value
gait parameters were used to encode the genotype. To overcome the reality gap
between simulation and the physical robot, they attempted to identify a set of
parameters which would induce the most commonality between the simulated gait
and the physical robot gait. However, very little work has been done to evolve
a gait controller capable traversing randomly uneven surfaces and scaling
obstacles.

An interesting problem in locomotion research is creating gaits for “injury”
conditions such as complete leg failure (?) or individual joint failure (?).
Similar to our work, ? (?) used combinations of sinusoidal waves to govern all
leg servo motion. The gait parameters composing the genotype were eight real
valued parameters; four leg angles and four distance parameters. Gaits were
evolved using a genetic algorithm with a population of 50 individuals over 40
generations. Evolution was performed in a simple Matlab mathematical
simulation and then gaits were tested on a physical robot. However, when the
gaits were transferred to the physical robot, inefficiencies were observed due
to the lack of physical dynamics modeling in the simulation (e.g., friction).
This illustrates the problem with conducting the evolution process in low
fidelity simulations.

In an effort to adapt to leg joint failure, ? (?) evolved their 18 DOF hexapod
gaits in simulation for 200 generations with fifty individuals per generation,
adapting gaits to individual motor loss rather than entire leg loss. A binary
genotype of 540 bits corresponded to fifty-four phenotype decimal gait
parameters. Their method relied on seeding the population with a hand tuned
gait; the evolved gaits were able to adapt to single and dual joint failure
albeit with many gaits considered spastic.

Rather than evolving a single gait, it may be useful to design multiple gaits
for different conditions (?; ?). ? (?) evolved a repertoire of hexapod walking
gaits by selecting multiple gaits per generation. This was accomplished using
a complex fitness mechanism which selected multiple individuals in each
population based on the resulting trajectories of the various gaits. For
transfer to the physical robot, gaits developed in simulation using the Open
Dynamics Engine were tested on the robot at regular intervals and given a
transfer rating. This transfer rating was used to train an SVM classifier.
Once the classifier had been trained with enough transferred gaits, it could
predict the likelihood of successful transfer of a given simulated gait to the
physical robot. The methodology produced several hundred functional gait
controllers useful for adjusting speed and direction.

## Method

Simulation environments are often used for evolutionary algorithm work as it
is impractical to test thousands of robot control configurations on a physical
robot. For our research, the Gazebo simulation environment was used to test
evolved gait configurations. Gazebo can be integrated with the Robot Operating
System (ROS) such that Gazebo receives control input from ROS and also
provides telemetry back to ROS which can then be published as a ROS topic.
There are a number of physics engines that can be used to power the Gazebo
simulation physics. For this effort, the default Open Dynamics Engine (ODE)
was used, though the future work section will discuss additional dynamics
engines that could be tested.

The simulated obstacle course shown in Figure 1 is approximately 3 meters in
width and 8.2 meters in length. The initial 3 meters of the course is composed
of a random step field which varies in height from 0 to 7.6 cm followed by a
11.4 x 11.4 cm box beam obstacle and then another meter and a half of random
step field followed by a dual box beam obstacle, and finally a 45 degree
inclined random step field. The course is enclosed with walls on either side
to prevent the robot from moving off the course and the trial is ended after
90 seconds, or if the robot reaches the top of the incline (8.2 meters).

Figure 2: PhantomX hexapod

With three degrees of freedom per leg, the PhantomX hexapod (Figure 2) has a
total of 18 degrees of freedom. The middle leg coxa servos are positioned at a
90 degree angle while the front and rear coxa are at 45 degree angles. Each
leg is 24 cm long fully extended and the thorax is approximately 9 x 20 x 5
cm. The tallest walking gait can achieve a ground clearance of just over 15 cm
at the expense of stability and mobility. Typical stable gait ground clearance
is 5 cm. The PhantomX Gazebo model
(https://github.com/HumaRobotics/phantomx_gazebo) was used with an increased
mass value of 2.5 kg to more accurately match the mass of the target PhantomX
hexapod with a battery and CPU. For this setup, the phantomx_walker and Gazebo
nodes are created, joint angles are initialized, and then the evolutionary
algorithm software creates a controller node. This node sends joint angles to
the PhantomX controller which in turn communicates the model movements to the
simulation. Lastly, a listener node receives ground truth of the robot’s
position and orientation to be evaluated by the fitness function.

For the hexapod control, the coxal servos are set to a constant tripod joint
angle trajectory using a continuous sinusoidal wave with the ROS clock as the
input value. A hexapod tripod gait is a symmetric gait in which the front and
rear legs on a given side will lift and move forward while the middle leg
pushes rearward on the ground. Then the front and rear legs touch down and
push back while the middle leg lifts. Both sides are timed so that there are
always three feet on the ground, one on one side and two on the other. The
front and rear coxal servos move forward in unison while the middle servo
moves rearward, with the opposite trajectory on the opposing side. Coxal servo
range values were set to maximize range of motion without collision and
limited to reaching directly forward and directly rearward. The evolution of
femur and tibia parameters is such that the two joint angles follow a
sinusoidal wave with either the same period or double the period of the coxal
trajectory. Assuming a symmetric gait only requires that half the total gait
parameters need to be evolved as one side is simply a phase shift from the
other side for all joint angles. Consequently, there are 8 parameters for each
leg for a total of 24 real value gait parameters composing the genome. For
each leg, the parameters are as follows: femur period, femur phase, femur
range, femur vertical shift, tibia period, tibia phase, tibia range, and tibia
vertical shift. The period value was either 1 or 2, phase value ranged from 0
to 2, servo range from 0 to 1.7 and vertical shift valued -1 to 1.

Similar to the joint angle trajectory approaches (?), the trajectory of each
leg joint is defined by a periodic function of the amplitude , phase shift
$\phi$ , period multiplier p, time t, and the vertical shift v.

$\gamma(\alpha,\textit{p},\textit{t},\phi,\textit{v})=\alpha\cdot\cos((\textit{p}\cdot\textit{t})+\phi)+\textit{v}$

This sinusoidal wave function for gait control was designed to achieve a
number of goals. With the intent to transfer the gait controller to the
physical robot, and because the physical dynamics accuracy of the PhantomX
Gazebo model is not known with certainty, a complex wave function (?), could
evolve into a gait in simulation that would be beyond the maximum angular
velocities of the physical PhantomX servos, causing the servo trajectory to
lag behind that of desired. This effect could be compounded given the unknown
update rates for the main controller loop when running on the robot’s CPU.
Because ROS is a distributed architecture, the simulator is running on a
separate CPU from the controller, allowing the controller loop to execute
quickly. It must be taken into account that the controller loop may not update
as quickly while running on the robot’s ARM processor which will also be
processing sensor data.

The performance of EAs rest on fitness functions which evaluate and select
individuals, z, in combination based on their evolutionary utility for future
generations. In robotic locomotion tasks, distance successfully traveled,
orientational stability, and speed are crucial elements of performance. Here,
we combined these performance metrics into a fitness function, designed to
jointly maximize velocity, $v$, and negative orientational displacement, $D$,
to quantify locomotion stability:

$fitness=\max_{z_{j}\ \in{C}}f(v,D_{p})\textrm{where}\quad
D_{p}=\sum_{j}-\frac{|\partial{D_{j}}|}{\partial{D_{j_{0}}}}$

Here, $D_{p}$ is the negative orientational displacement pooled across
dimensions with respect to initial orientation conditions. Note, this could
also be cast as a maximization, minimization problem.

There are two basic methods to initialize a population for the first
generation of an evolutionary algorithm. The first is generating random
(Gaussian or uniform) legal values for each parameter. The second is to start
with a seed individual and randomly mutate the individual to form the first
population. For this effort, the initial population was a Gaussian mutation of
a hand tuned all terrain gait. The seed individual itself was not included in
the first generation. For each new generation, the fitness function was used
to evaluate all individuals and then two parents were chosen using tournament
style selection. Specifically, the first parent was selected as the highest
fitness individual from the first half of the population and the second parent
was the highest fitness individual from the second half of the population.
Once parents were selected, a new population is produced in the following
manner. Each new individual has a 0.5 probability to be either generated by
Gaussian mutation of the higher fitness parent or generated by a two point
random genetic crossover of both parents. For those mutated from a single
parent, the mutation probability was 0.4 for each parameter. Elitism was not
employed, so parents did not survive to subsequent generations. The two point
crossover function used for the evolutionary algorithm was imported from the
DEAP evolutionary computation framework (http://github.com/deap/deap).

As to be expected with random mutation, many individual gaits were found to be
extremely unstable during initial testing. To manage this, maximum orientation
thresholds were imposed such that an individual gait trial would terminate
early if the gait proved excessively unstable or reversed in direction. During
the trial for each individual, the published (ROS topic) quaternion values
were used to determine drastic changes in orientation and thus end the trial
early if the individual went outside specific orientation parameters. Maximum
orientation parameters were set at 45 degrees roll, 70 degrees pitch and 90
degrees yaw. Additionally, if the gait drove the robot in reverse for more
than 0.2 meters, the trial was ended. The average rate of change in the w
quaternion value was used to measure orientation stability of the gait. This
stability accounted for 5% of the overall fitness score. The time period for
each trial was set at 90 seconds. Lateral displacement was not explicitly
penalized, as a real world gait controller would provide steering capability
and any open loop gait is likely to veer of course a bit in a random step
field. The overall linear directional fitness provided implicit penalty to
lateral displacement, and though it may possible for an erratic gait to
achieve higher linear directional fitness by bouncing off of the walls, the
orientation stability component of the fitness value would explicitly penalize
such a gait. We executed the evolutionary algorithm with a population of 200
individuals for 23 generations.

## Evaluation

For comparison, the hand tuned, fast, flat surface gait was able to traverse
the 8.6 meters on flat ground in 34.8 seconds. When traversing the random step
field, this initial tripod gait only achieved 1.28 meters in the same time
period. The evolutionary algorithm evolved a gait controller which was able to
traverse over 6 meters of random step field and obstacles over 90 seconds.

Figure 3: Fitness (blue) and distance traveled (red) by generation (x-axis).
The highest distance achieved in generation 8 had relatively low stability.

Fitness results indicate that the evolved gaits were able to reach the first
obstacle starting with the 1st generation and then didn't find a good obstacle
climbing gait until the 6th generation (Fig 3). From the 5th generation to the
8th, the algorithm achieved a rapid improvement in fitness with the fitness
scoring diverging slightly from the distance achieved once the hexapod passed
the 5 meter mark, likely due to the obstacles at that point. Distance achieved
for generation 8 was 6.2 meters which is just starting to climb the step field
incline. Fitness then sharply dropped off for the next few generations; the
robot was unable to traverse the second obstacle until generation 22 and 23,
with generation 23 reaching the second furthest distance of 5.9 meters. If
elitism had been employed, in which parents survive to the next generation,
the generation 23 gait solution would likely not have been discovered,
limiting the overall search space.

| Gen. 8 | Gen. 23 | Diff. | % Range
---|---|---|---|---
Fitness | 6 | 5.7 | .3 | 5%
Distance | 6.2 | 5.9 | .3 | 5%
Front Femur Phase | 6.28 | 6.28 | 0.00 | 0%
Front Femur Range | 0.41 | 1.27 | 0.86 | 51%
Front Femur Shift | -0.27 | -1.00 | .73 | 37%
Front Tibia Phase | 2.29 | 2.89 | 0.60 | 10%
Front Tibia Range | 1.50 | 1.36 | 0.14 | 8%
Front Tibia Shift | 0.71 | 0.81 | 0.11 | 5%
Middle Femur Phase | 0.46 | 6.28 | 5.82 | 7%
Middle Femur Range | 0.97 | 1.08 | 0.11 | 6%
Middle Femur Shift | -0.67 | 0.31 | 0.97 | 49%
Middle Tibia Phase | 0.94 | 1.36 | 0.41 | 7%
Middle Tibia Range | 0.05 | 0.73 | 0.67 | 40%
Middle Tibia Shift | 0.41 | 0.54 | 0.13 | 7%
Rear Femur Phase | 6.23 | .71 | 0.52 | 10%
Rear Femur Range | 0.12 | 0.62 | 0.50 | 29%
Rear Femur Shift | -0.75 | -0.87 | 0.13 | 6%
Rear Tibia Phase | 1.62 | 6.03 | 4.41 | 70%
Rear Tibia Range | 0.14 | 0.87 | 0.73 | 43%
Rear Tibia Shift | 0.00 | -0.21 | 0.21 | 11%
Table 1: The two best gaits compared. The scalar value difference is shown
along with the percentage difference. The large difference in gait values
likely indicates the generation 23 gait was toward a different optima in
search space.

Table 1 shows the gait parameters for generation 8 and generation 23, the
highest fitness individuals. The period multiplier value is not shown as it
converged to one in every generation but the first. The average difference
between the two gaits is 22% with 9 of the 18 parameters values within 10% of
each other. The front tibia kinematics appear to be most similar between the
two gaits at only 20% difference, while the rear tibias have the most
difference at 41%. With only a 5% difference in fitness and distance between
the two gaits, there are no obvious indications that gait 23 was converging
toward the same optima as gait 8.

Figure 4: Distance achieved in meters (blue) and scaled orientational
stability value (red) is shown for each generation (x-axis).

Figure 4 shows distance achieved versus scaled stability. A higher stability
value in the chart indicates higher orientational stability. The stability
(average change in quaternion w) over the generations indicates that the
initial high fitness of generation 8 was not as stable as the solution found
in generation 23, further evidence of the different location in search space
between the two solutions. Traversing the box beam obstacles has the highest
adverse impact on stability, in that the hexapod encounters a vertical
obstacle which causes rapid changes in pitch when traversing. Three of the
five highest stability gaits were the ones that stopped at or just before the
first obstacle (gaits 4, 11 and 15). Consequently, the main stability
challenge was the dual box beam obstacle which was configured with the first
beam starting at 4.75 meters and the next beam at 5.2 meters, leaving only a
35cm gap between box beams. The PhantomX hexapod neutral stance has a minimum
of 40cm between front and rear feet so the dual box beam forms a single
obstacle. For gaits 16, 18 and 20, encountering this obstacle likely adversely
affected their stability score as well as halting any further directional
progress.

Figure 5: Front leg angular trajectories. Red is the coxa, green is the femur
and blue is the tibia, with higher coxa values being servo forward and higher
values for the femur and tibia both being servo up.

Figure 5 shows the right front leg angular trajectories for the highest
fitness gait. As illustrated, it is evident that just before the coxa drives
rearward, the femur starts its downward stroke, followed quickly by the tibia.
Next, the femur and tibia start their upward stroke before the coxa reaches
its rearmost point. The tibia range (amplitude) of 1.5 is much greater than
that of the femur range 0.4 which is in stark contrast to the hand tuned all-
terrain seed gait which had a tibia range of only 0.4 and a femur range of
0.8. Furthermore, the tibia wave is shifted higher, giving the tibia the
ability to reach up and over obstacles.

Unlike the front legs, where the tibia had a much higher range of motion than
the femur, in the middle legs the femur is doing most of the work while the
tibia is angled up slightly but with very little range of motion. For the rear
legs, femur and tibia have evolved a very low range of motion. With the femur
angled down (horizontal shift) and the tibia in phase with the coxal, it would
appear the rear legs are acting more to stabilize the hexapod orientation
while still providing ground clearance versus any significant contribution to
forward momentum.

Figure 6: Change in gait parameters (generation 5 through 8). The nearest data
is generation 5 with Front Femur Phase (FFR) on the left, then Front Femur
Range (FFR), then Front Femur Shift (FFS), Front Tibia Phase (FTP) and so on
for middle and rear values.

Figure 6 shows the parameter data from generation 5 through 8; it reveals a
rapid increase in fitness, going from the second lowest fitness to the highest
in only 4 generations. The largest increase in fitness was observed between
generations 6 and 7 where we see a substantial decrease in middle tibia phase
which may be correlated with the large change in fitness.

Figure 7: Gait covariance with distance. This analysis reveals that the front
femur phase, middle femur phase, and rear tibia phase parameters are highly
correlated with distance achieved.

By examining the covariance of each parameter over all generations with
respect to distance traveled (Fig. 7), it is evident that front femur phase,
middle femur phase and rear tibia phase are key parameters for a successful
adverse terrain gait evolution. Front femur vertical shift, middle tibia
range, rear femur vertical shift and rear tibia range are the least correlated
with distance traveled. Since the phase shift parameters control the
relationship between a given joint movement cycle with respect to the coxa,
having this timing off would greatly affect vehicle movement (e.g., if the
coxal joint is moving rearward and the femur has the leg in the air versus on
the ground).

## Conclusion and Future Work

Using an evolutionary algorithm, an open loop gait controller was evolved to
enable a hexapod robot to traverse uneven terrain and obstacles in simulation.
Using a population of 200 individuals over 23 generations, the evolutionary
algorithm evolved a gait that was able to traverse just over 6 meters of
random step field and linear obstacles in 90 seconds. The highest fitness
score was actually reached in the 8th generation, then fitness lowered for the
population and eventually climbed back up to 96% of the earlier solution.

For the given hexapod simulation model and physics engine, evolving a multi-
terrain gait for a high degree of freedom legged robotic platform was
successful in fewer generations than anticipated. A gait was evolved that
could traverse random step fields, box beam obstacles and a inclined step
field while also maintaining a degree of orientational stability. Future
research into characterizing highly transferable multi-terrain gaits could
allow a multitude of obstacle traversing gaits to be developed in simulation
for successful transfer to the physical robot. Furthermore, considering the
correlation of changes in gait parameters with respect to performance should
inform additional refinement towards the most efficient strategy for evolving
robotic gaits.

Evolving the gait in simulation is only useful if it is transferable to an
actual hardware platform. Given this, the next step is to test the various
peak performing gaits on the actual hardware of the PhantomX hexapod. From the
fitness graph, it is evident that there may be more than one capable gait
worth transfer testing.

Selecting and fine tuning the various evolutionary algorithm techniques and
choice of parameters has a significant impact on algorithm performance. The
practice of meta-evolution, in which these variables are themselves evolved
and optimized, enables much more efficient genotype-to-phenotype mapping as
shown by previous work (?). Specifically, a linear pleiotropic encoding would
enable a single genotype value to alter multiple gait parameters and discover
solutions more efficiently.

A future study could also implement different rigid body dynamics engines in
Gazebo such as Bullet, DART or Symbody, and then test transfer to the physical
platform to see which dynamics engines are evolving the most transferable
gaits. Additionally, implementing machine learning to classify gaits based on
the the quality of each gait transfer from hardware to simulation (?) could
also help overcome the “reality gap”.

Anther consideration for future research is a repertoire of gaits approach in
which a gait controller is evolved separately for each obstacle class. These
gaits could then be bred as seed genomes for an initial population, in the
interest of discovering new multi-obstacle hybrid gaits.

Finally, Gazebo supports a contact sensor module, which reports collisions and
forces between objects. This module could provide the means to evolve a closed
loop gait controller if the contact sensor were added to the tibia/foot. A
dynamic controller that could maximize agility as well as minimize contact
forces would help to increase power efficiency, which is a significant
challenge for legged robotics, especially over rough terrain.

## References

  * [Belter and Skrzypczyński 2010] Belter, D., and Skrzypczyński, P.  2010\.  A biologically inspired approach to feasible gait learning for a hexapod robot.  International Journal of Applied Mathematics and Computer Science 20(1):69–84.
  * [Cully and Mouret 2016] Cully, A., and Mouret, J.-B.  2016\.  Evolving a behavioral repertoire for a walking robot.  Evolutionary Computation 24(1):59–88.
  * [Irawan and Nonami 2012] Irawan, A., and Nonami, K.  2012\.  Force threshold-based omni-directional movement for hexapod robot walking on uneven terrain.  In IEEE International Conference on Computational Intelligence, 127–132.
  * [Koenig et al. 2011] Koenig, A.; Novak, D.; Omlin, X.; Pulfer, M.; Perreault, E.; Zimmerli, L.; Mihelj, M.; and Riener, R.  2011\.  Real-time closed-loop control of cognitive load in neurological patients during robot-assisted gait training.  IEEE Transactions on Neural Systems and Rehabilitation Engineering 19(4):453–464.
  * [Kon and Sahin 2020] Kon, J., and Sahin, F.  2020\.  Gait generation for damaged hexapods using a genetic algorithm.  In IEEE International Conference of System of Systems Engineering (SoSE), 451–456.
  * [Lewis, Fagg, and Solidum 1992] Lewis, M. A.; Fagg, A. H.; and Solidum, A.  1992\.  Genetic programming approach to the construction of a neural network for control of a walking robot.  In IEEE International Conference on Robotics and Automation, 2618–2623.
  * [Li et al. 2015] Li, W.; Chen, W.; Wu, X.; and Wang, J.  2015\.  Parameter tuning of CPGs for hexapod gaits based on genetic algorithm.  In IEEE Conference on Industrial Electronics and Applications (ICIEA), 45–50.
  * [Manglik, Gupta, and Bhanot 2016] Manglik, A.; Gupta, K.; and Bhanot, S.  2016\.  Adaptive gait generation for hexapod robot using a genetic algorithm.  In IEEE International Conference on Power Electronics, Intelligent Control and Energy Systems (ICPEICES), 1–6.
  * [Scott and Bassett 2015] Scott, E. O., and Bassett, J. K.  2015\.  Learning genetic representations for classes of real-valued optimization problems.  In Proceedings of the Companion Publication of the Annual Conference on Genetic and Evolutionary Computation, 1075–1082.