Quadratic Word Equations with Length Constraints,
Counter Systems, and Presburger Arithmetic with
Divisibility
Anthony W. Lin1 and Rupak Majumdar2
1

2

Oxford University, UK
Max Planck Institute for Software Systems, Germany

Abstract. 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 toconstant 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 abstractionsof 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 regularconstraints. We provide an encoding of the effect of a simple loop of the countersystems in the existential theory of 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). 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. Decidability holds when the constraints
are 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 first order theory over strings and concatenation is undecidable. A seminal
result by Makanin [24] (see also [11, 15]) shows that the satisfiability problem for the
existential fragment is decidable, by giving an algorithm for the satisfiability of word
equations. A word equation L = R consists of two words L and R over an alphabetof constants and variables. It is satisfiable if there is a mapping σ from the variables tostrings over the constants such that σ(L) and σ(R) are syntactically identical.
An original motivation for studying word equations was to show undecidability ofHilbert’s 10th problem (see, e.g., [26]). 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 [26]. A length constraint constrains
the solution of a word equation by requiring a linear relation to hold on the lengths ofwords in a solution σ (e.g., |x| = |y|, where | · | denotes the string-length function). The
decidability of word equations with length constraints remains open.
In recent years, reasoning about strings with length constraints has found renewedinterest through applications in program verification and reasoning about security vulnerabilities. The focus of most research has been on developing practical string solvers(cf. [1, 5, 6, 14, 16, 21, 28, 31–33]). These solvers are sound but make no claims of completeness. Relatively few results are known about the decidability status of strings withlength and other constraints (see [9] 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 [1, 9, 13, 22]. However, as we shall see in this paper, the length
abstraction of a word equation (i.e. the set of possible lengths of variables in its solutions) need not be Presburger definable.
In this paper, we consider the case of quadratic word equations, in which each variable can appear at most twiceVn [12, 19], together with length constraints and regularconstraints (conjunctions i=1 x ∈ Li of assertions that the variable x must be assigned a string in the regular language Li for each i). 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 [12]. However, we show that already for this class (evenfor 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 basedon 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 nodesof the proof tree constructed by Levi’s method, and a counter standing for the lengtheach 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  = ) is precisely the length abstraction of the word equation.
Our second observation is that the reachability relation for a simple loop of thecounter system can be encoded in the existential theory of Presburger arithmetic withdivisibility (PAD). The encoding is non-trivial in the presence of regular constraints,
and depends on structural results on semilinear sets. As PAD is decidable [18, 23], we
obtain a technique to symbolically represent the reachability relation for flat countersystems, 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 [10],have flat proof trees. Thus, the satisfiability problem for quadratic regular-oriented word
equations with length constraints is decidable (and in NEXP3 ).
3

In fact, it is a NP algorithm with an oracle access to PAD. The best complexity bound for thelatter is NEXP and NP-hardness [18].

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 [10]. Our result generalizes previous decidability results [9]. Moreover,
we believe that the techniques in this paper — the connection between acceleration andword equations, and the use of existential Presburger with divisibility — can pave theway to more sophisticated decision procedures based on counter system acceleration.

2

Preliminaries

General notation: Let N = Z≥0 be the set of all natural numbers. For integers i ≤ j,
we use [i, j] to denote the set {i, i + 1, . . . , j − 1, j} of integers. If i ∈ N, let [i] denote[0, i]. We use  to denote the component-wise ordering on Nk , i.e., (x1 , . . . , xk ) (y1 , . . . , yk ) iff xi ≤ yi for all i ∈ [1, k]. If x̄  ȳ and x̄ 6= ȳ, we write x̄ ≺ ȳ.
If S is a set, we use S ∗ to denote the set of all finite sequences, or words, γ =s1 . . . sn over S. The length |γ| of γ is n. The empty sequence is denoted by . Noticethat S ∗ forms a monoid with the concatenation operator ·. If γ 0 is a prefix of γ, we write
γ 0  γ. Additionally, if γ 0 6= γ (i.e. a strict prefix of γ), we write γ 0 ≺ γ. Note that theoperator  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 := w1 . . . wn ∈ A∗ , wewrite w[i, j], where 1 ≤ i ≤ j ≤ n, to denote the segment wi . . . wj .
Two words x and y are conjugates if there exist words u and v such that x = uv andy = vu. Equivalently, x = cyck (y) for some k and for the cyclic permutation operation
cyc : A∗ → A∗ , defined as cyc() = , and cyc(a · w) = w · a for a ∈ A and w ∈ A∗ .
Given a nondeterministic finite automaton (NFA) A := (A, Q, ∆, q0 , qF ), a run of
A on w is a function ρ : N → Q with ρ(0) = q0 that obeys the transition relation ∆.
We may also denote the run ρ by the word ρ(0) · · · ρ(n) over the alphabet Q. The run ρis said to be accepting if ρ(n) = qF , in which case we say that the word w is acceptedby A. The language L(A) of A is the set of words in A∗ accepted by A. In the sequel,for p, q ∈ Q we will write Ap,q to denote the NFA A with initial state replaced by p
and final state replaced by q.
Word equations: Let A be a (finite) alphabet of constants and V a set of variables;
we assume A ∩ V = ∅. A word equation E is an expression of the form L = R,
where (L, R) ∈ (A ∪ V )∗ × (A ∪ V )∗ . A system of word equations is a nonempty
set {L1 = R1 , L2 = R2 , . . . , Lk = Rk } of word equations. The length of a system ofPkword equations is the length i=1 (|Li | + |Ri |). A system is called quadratic if eachvariable occurs at most twice in all. A solution to a system of word equations is ahomomorphism σ : (A ∪ V )∗ → A∗ which maps each a ∈ A to itself that equates thel.h.s. and r.h.s. of each equation, i.e., σ(Li ) = σ(Ri ) for each i = 1, . . . , k.
For each variable x ∈ V , we shall use |x| to denote a formal variable that stands forthe length of variable x, i.e., for any solution σ, the formal variable |x| takes the value|σ(x)|. Let LV be the set {|x| | x ∈ V }. A length constraint is a formula in Presburger
arithmetic whose free variables are in LV .
A solution to a system of word equations with a length constraint Φ(|x1 |, . . . , |xn |)is a homomorphism σ : (A ∪ V )∗ → A∗ which maps each a ∈ A to itself such that

σ(Li ) = σ(Ri ) for each i = 1, . . . , k and moreover Φ(|σ(x1 )|, . . . , |σ(xn )|) 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 asystem 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 ∈ V , and a regular language L ⊆ A∗ , a regularconstraint x ∈ L imposes the additional restriction that any solution σ must satisfy
σ(x) ∈ 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.
Linear arithmetic with divisibility: Let P be a first-order language with equality,with binary relation symbol ≤, and with terms being linear polynomials with integer
coefficients. We write f (x), g(x), etc., for terms in integer variables x = x1 , . . . , xn .
Atomic formulas in Presburger arithmetic have the form f (x) ≤ g(x) or f (x) = g(x).
The language PAD of Presburger arithmetic with divisibility extends the language P
with a binary relation | (for divides). An atomic formula has the form f (x) ≤ g(x)or f (x) = g(x) or f (x)|g(x), where f (x) and g(x) are linear polynomials with integer coefficients. The full first order theory of PAD is undecidable, but the existential
fragment is decidable [18, 23].
Note that the divisibility predicate x|y is not expressible in Presburger arithmetic: a
simple way to see this is that {(x, y) ∈ N2 | 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 [3]). These more general transition relations can be simulated by standard Minsky’s counter machines, butthey are more useful for coming up with decidable subclasses of counter systems. A
counter system C is a tuple (X, Q, ∆), where X = {x1 , . . . , xm } is a finite set of counters, Q is a finite set of control states, and ∆ is a finite set of transitions of the form(q, Φ(x̄, x̄0 ), q 0 ), where q, q 0 ∈ Q and Φ is a Presburger formula with free variables
x1 , . . . , xm , x01 , . . . , x0m . A configuration of C is a tuple (q, v) ∈ Q × Nm .
The semantics of counter systems is given as a transition system. A transition system
is a tuple S := hS; →i, where S is a set of configurations and → ⊆ S × S is abinary relation over S. A path in S is a sequence s0 → · · · → sn of configurations
s0 , ..., sn ∈ S. If S 0 ⊆ S, let pre ∗ (S 0 ) denote the set of s ∈ S such that s →∗ s0 forsome s0 ∈ S 0 . We might write pre ∗→ (S 0 ) to disambiguate the transition system.
A counter system C generates the transition system SC = hS; →i, where S is
the set of all configurations of C, and (q, v) → (q 0 , v0 ) if there exists a transition(q, Φ(x̄, x̄0 ), q 0 ) ∈ ∆ such that Φ(v, v0 ) is true.
In the sequel, we will be needing the notion of flat counter systems [3, 4, 7, 20].
Given a counter system C = (X, Q, ∆), the control structure of C is an edge-labeled
directed graph G = (V, E) with the set V = Q of nodes and the set E = ∆. The
counter system C is flat if each node v ∈ V is contained in at most one simple cycle.

3

Solving Quadratic Word Equations

We start by recalling a simple textbook recipe (Nielsen transformation, a.k.a., Levi’s
Method) [11, 19] 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 a natural example that is not Presburger-definable.
3.1

Nielsen transformation

We will define a rewriting relation E ⇒ E 0 between quadratic word equations E, E 0 .
Let E be an equation of the form αw1 = βw2 with w1 , w2 ∈ (A ∪ V )∗ and α, β ∈A ∪ V . Then, there are several possible E 0 :– Rules for erasing an empty prefix variable. These rules can be applied if α ∈ V(symmetrically, β ∈ V ). We nondeterministically guess that α be the empty word, i.e., E 0 is (w1 = βw2 )[/α]. The symmetric case of β ∈ V is similar.
– Rules for removing a nonempty prefix. These rules are applicable if each of αand β is either a constant or a variable that we nondeterministically guess to bea nonempty word. There are several cases:(P1) α ≡ β (syntactic equality). In this case, E 0 is w1 = w2 .
(P2) α ∈ A and β ∈ V . In this case, E 0 is w1 [αβ/β] = β(w2 [αβ/β]). In
the sequel, to avoid notational clutter we will write βw2 [αβ/β] instead ofβ(w2 [αβ/β]).
(P3) α ∈ V and β ∈ A. In this case, E 0 is α(w1 [βα/α]) = w2 [βα/α].
(P4) α, β ∈ V . In this case, we nondeterministically guess if α  β or β  α.
In the former case, the equation E 0 is w1 [αβ/β] = β(w2 [αβ/β]). In the latter
case, the equation E 0 is E 0 is α(w1 [βα/α]) = w2 [βα/α].
Note that the transformation keeps an equation quadratic.
Proposition 1. E is solvable iff E ⇒∗ ( = ). Furthermore, checking if E is solvable
is in PSPACE.
See [11] 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 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 [12]). We assume that a regular constraint x ∈ L is given as an NFA
Ap,q representing L. If q0 and qF are the initial and final states (respectively) of an NFAA, we can be more explicit and write Aq0 ,qF instead of A.
Our rewriting relation ⇒ 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 αw1 =βw2 with w1 , w2 ∈ (A ∪ V )∗ and α, β ∈ A ∪ V . We now define (E, S) ⇒ (E 0 , S 0 )by extending the pervious definition of ⇒ without regular constraints. Firstly, we make

sure that S is satisfiable by a standard automata-theoretic algorithm, which can be donein PSPACE. In particular, it has to be the case that E ⇒ E 0 and additionally do thefollowing:– Rules for erasing an empty prefix variable α. When applied, ensure that each regular constraint α ∈ L in S satisfies  ∈ L. Define S 0 as S minus all regular constraints of the form α ∈ L.
– Rules for removing a nonempty prefix. For (P1), we set S 0 to be S minus all constraints of the form α ∈ L if α is a variable. For (P2)–(P4), assume that E 0 is
w1 [αβ/β] = β(w2 [αβ/β]); the other case is symmetric. For each regular constraint β ∈ L(Ap,q ), we nondeterministically guess a state r, and add α ∈ L(Ap,r )and β ∈ L(Ar,q ) to S 0 . In the case when α ∈ A, we could immediately performthe check α ∈ L(Ap,r ): a positive outcome implies removing this constraint fromS 0 , while on a negative outcome our algorithm simply fails on this branch. For any
variable y that is distinct from β, we add all regular constraints y ∈ L in S to S 0 . If
α still occurs in E 0 , add regular constraints α ∈ L in S to S 0 . If S 0 is unsatisfiable,
fail on this this branch.
Proposition 2. (E, S) is solvable iff (E, S) ⇒∗ ( = , ∅). 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 constraintx ∈ L(Ap,q ) to a variable x, where 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 ⇒ so that each a configuration E or (E, S) in the graph of⇒ is also annotated by an assignment σ of the variables in E to concrete strings. We
write E1 [σ1 ] ⇒ E2 [σ2 ] if E1 ⇒ E2 and σ2 is the modification from σ1 according to theoperation used to obtain E2 from E1 . Observe that the domain of σ2 is a subset of thedomain of σ1 ; in fact, some rules (e.g., erasing an empty prefix variable) could remove
a variable in the prefix in E1 from σ1 . The following example illustrates how ⇒ works
with this extra annotated assignment. Suppose that σ1 (x) = ab and σ1 (y) = abab andE1 := xy = yx and E2 is obtained from E1 using rule (P4), i.e., substitute xy for y.
In this case, σ2 (x) = σ2 (y) = σ1 (x) = ab. Observe that E2 [σ2 ] ⇒ E3 [σ3 ] ⇒ E4 [σ4 ],where E3 := E2 , σ3 (x) = ab, σ3 (y) = , E4 := x = x, and σ4 (x) = ab. The
definition for the case with regular constraints is identical.
Proposition 3. (E, S)[σ] →∗ ( = , ∅)[σ 0 ] where σ 0 has the empty domain iff σ is asolution of (E, S).
This proposition immediately follows from the proof of correctness of Nielsen transformation for quadratic word equations (cf. [11]).

3.4

Length abstractions and semilinearity

Given a quadratic word equation E with constants A and variables V = {x1 , . . . , xk },its length abstraction is defined as follows
L EN(E) = {(|σ(x1 )|, . . . , |σ(xk )|) : σ 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 L EN(E) can be captured by the Presburger formula |z| = |x| + 2. Observethat each (nx , ny , nz ) ∈ L EN(E) must satisfy nz = nx + 2 by a length argument on E. Conversely, we will show that each triple (nx , ny , nz ) ∈ N3 satisfying
nz = nx + 2 must be in L EN(E). To this end, we will define a solution σ to E such that(|σ(x)|, |σ(y)|, |σ(z)|) = (nx , ny , nz ). Consider σ(x) = anx . Then, for some q ∈ N
and r ∈ [nx + 1], we have ny = q(nx + 2) + r. Let w be a prefix of σ(x)ab of lengthr. Therefore, for some v, we have wv = σ(x)ab. Define σ(y) = (σ(x)ab)q w. We thenhave σ(x)abσ(y) = σ(y)vw. Thus, setting σ(z) = vw gives us a satisfying assignmentfor E which satisfies the desired length constraint.
tuHowever, it turns out that Presburger Arithmetic is not sufficient for capturing length
abstractions of quadratic word equations.
Theorem 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 ∈ A andx, y ∈ V , is not Presburger definable.
Lemma 1. The length abstraction L EN(xaby = yabx) coincides with tuples (|x|, |y|)of numbers satisfying the expression ϕ(|x|, |y|) defined as:|x| = |y| ∨ (|x| = 0 ∧ |y| ≡ 0(mod 2)) ∨ (|y| = 0 ∧ |x| ≡ 0(mod 2))∨ (|x|, |y| > 0 ∧ 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 Presburgerdefinable, which is not the case since the property that two numbers are relatively prime
is not Presburger-definable. Let us prove this lemma. Let S = L EN(xaby = yabx). We
first show that given any numbers nx , ny satisfying ϕ(nx , ny ), there are solutions σ toxaby = yabx with |σ(x)| = nx and |σ(y)| = ny . If they satisfy the first disjunct in ϕ(i.e., nx = ny ), then set σ(x) = σ(y) to an arbitrary word w ∈ Anx . If they satisfy thesecond disjunct, then aby = yab and so set σ(x) =  and σ(y) ∈ (ab)∗ . The same goeswith the third disjunct, symmetrically. For the fourth disjunct (assuming the first three
disjuncts are false), let d = gcd(nx + 2, ny + 2). Define σ(x), σ(y) ∈ (ad−1 b)∗ (ad−2 )so that |σ(α)| = nα for α ∈ V . It follows that σ(x)abσ(y) = σ(y)abσ(x).
We now prove the converse. So, we are given a solution σ to xaby = yabx and let
u := σ(x), v := σ(y). Assume to the contrary that ϕ(|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 ϕ(|u|, |v|) is false.
– u = . Then, abv = vab and so v ∈ (ab)∗ , which implies that |v| ≡ 0 (mod 2).
Contradicting that ϕ(|u|, |v|) is false.
– v = . Same as previous item and that |u| ≡ 0 (mod 2).
– |u| > |v| > 0. Since ϕ(|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, theletter at position |u|+2 would be b on l.h.s. and a on r.h.s., which is a contradiction.
Therefore |u| ≥ |v| + 2. Let u0 = u[|v| + 3, |u|], i.e., u but with its prefix oflength |v| + 2 removed. By Nielsen transformation, we have u0 abv = vabu0 . It
cannot be the case that u0 = ; for, otherwise, abv = vab implies v ∈ (ab)∗ andso u = vab, implying that 2 divides both |u| + 2 and |v| + 2, contradicting that
gcd(|u| + 2, |v| + 2) = 1. Therefore, |u0 | > 0. Since gcd(|u0 | + 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 weshow the extension to the case with regular constraints.
Given the quadratic word equation E, we show how to compute a counter system
C(E) = (X, Q, ∆) such that the following theorem holds.
Theorem 2. The length abstraction of E coincides with{v ∈ N|V | | (E, v) ∈ pre ∗C(E) ({ = } × N|V | )}Before defining C(E), we define some notation. Define the following formulas:V– ID(x̄, x̄0 ) := x∈x̄ x0 = x
V– SUBy,z (x̄, x̄0 ) := z ≤ y ∧ y 0 = y − z ∧V x∈x̄,x6=y x0 = x– DECy (x̄, x̄0 ) := y > 0 ∧ y 0 = y − 1 ∧ x∈x̄,x6=y x0 = x
V
Note that the 6= symbol in the guard of denotes syntactic equality (i.e. not equality
in Preburger Arithmetic). We omit mention of the free variables x̄ and x̄0 when they areclear 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 C(E) = (X, Q, ∆) 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 0 that can be rewritten from E using Nielsentransformation, i.e., Q := {E 0 : E ⇒∗ E 0 }. The set Q is finite (at most exponential in|E|) as per our discussion in the previous section.
We now define the transition relation ∆. We use x̄ to enumerate V in some order.
Given E1 ⇒ E2 with E1 , E2 ∈ Q, we then add the transition (E1 , Φ(x̄, x̄0 ), E2 ), whereΦ is defined as follows:– If E1 ⇒ E2 applies a rule for erasing an empty prefix variable y ∈ x̄, then Φ :=y = 0 ∧ ID.
– If E1 ⇒ E2 applies a rule for removing a nonempty prefix:• If (P1) is applied, then Φ = ID.
• If (P2) is applied, then Φ = DECβ .
• If (P3) is applied, then Φ = DECα .
• If (P4) is applied and α  β, then Φ = SUBβ,α . If β  α, then Φ = SUBα,β .
Observe that if (E1 , v1 ) → (E2 , v2 ), then |E1 | ≤ |E2 | and v1  v2 . In addition, if
v1 = v2 , then |E1 | < |E2 |. This implies the following lemma.
Lemma 2. The counter system C(E) terminates from every configuration (E0 , v0 ).
The proof of Theorem 2 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 regularconstraints, which are effectively semilinear due to Parikh’s Theorem [27]. Given aquadratic word equation E with a set S of regular constraints, we define the countersystem C(E, S) = (X, Q, ∆) as follows. Let C(E) = (X1 , Q1 , ∆1 ) be the countersystem from the previous paragraph, obtained by ignoring the regular constraints. We
define X = X1 . Let Q be the finite set of all configurations reachable from (E, S), i.e.,
Q = {(E 0 , S 0 ) : (E, S) ⇒∗ (E 0 , S 0 )}. Given (E1 , S1 ) ⇒ (E2 , S2 ), we add the transition ((E1 , S2 ), Φ(x̄, x̄0 ), (E2 , S2 )) as follows. Suppose that (E1 , Φ0 (x̄, x̄0 ), E2 ) was
added to ∆1 by E1 ⇒ E2 . Then,


^
\
\
x ∈ L EN(
Φ := Φ0 ∧L) ∧ x0 ∈ L EN(
L) .
x∈x̄

(x∈L)∈S(x∈L)∈S 0

T
The size of the NFA for (x∈L)∈S L is exponential in the number of constraints of theform (x ∈ L) in S (of which there are polynomially many). The constraint x ∈ L EN(L)is well-known to be effectively semilinear [27]. In fact, using the algorithm of ChrobakMartinez [8, 25, 29], we can compute in polynomial time two finite sets A, A0 of integers
and an integer b such that, for each n ∈ N, n ∈ U := A ∪ (A0 + bN) is true iffn ∈ L EN(L). Note that U is a finite union of arithmetic progressions (with period 0
and/or b). In fact, each number a ∈ A ∪ A0 (resp. the number b) is at most quadratic in
the size of the NFA, and so it is a polynomial 4 size even when they are written in unary.
Therefore, treating U as an existential Presburger formula ϕ(x) with one free variable(an existential quantifier is needed to guess the coefficient n such that x = ai + bn forsome i), the resulting Φ0 is a polynomial-sized existential Presburger formula.
Theorem 3. The length abstraction of (E, S) coincides with{v ∈ N|V | | ((E, S), v) ∈ pre ∗C(E,S) ({( = , ∅)} × N|V | )}4

Note that we mean polynomial in the size of the NFA, which can be exponential in |S|.

As for the case without regular constraints, the proof of Theorem 2 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 C = (X, Q, ∆) with Q = {q0 , . . . , qn−1 }, such that forsome y ∈ X the transition relation ∆ consists of precisely the following transition(qi , Φi , qi+1 (mod n) ), for each i ∈ [n − 1], and each Φi is either SUBy,z (with z avariable distinct from y) or DECy . Such a counter system is said to be a 1-variablereducing cycle.
Lemma 3. There exists a polynomial-time algorithm which given a 1-variablereducing cycle C = (X, Q, ∆) and two states p, q ∈ Q computes an formula ϕp,q (x̄, x̄0 )in existential Presburger arithmetic with divisibility such that (p, v) →∗C (q, w) iff
ϕp,q (v, w) is satisfiable.
This lemma can be seen as a special case of the acceleration lemma for flat parametriccounter 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 = q0
and p = qi , for some i ∈ N. Any path (q0 , v) →∗C (qi , w) can be decomposed into thecycle (q0 , v) →∗ (q0 , v0 ) and the simple path (q0 , w0 ) → · · · → (qi , wi ) of length i.
Therefore, the reachability relation (q0 , x) →∗C (qi , y) can be expressed as∃z0 , · · · , zi−1 : ϕq0 ,q0 (x, z0 ) ∧ Φ0 (z0 , z1 ) ∧ · · · ∧ Φi−1 (zi−1 , y).
Thus, it suffices to showPthat ϕq0 ,q0 (x, x0 ) is expressible in PAD. Consider a linear
expression M = a0 + x∈X\{y} ax x, where a0 is the number of instructions i in
the cycle such that Φi = DECy and ax is the number of instructions i such that Φi =SUBy,x . Each time around the cycle, y decreases by M . Thus, for some n ∈ N we have
y 0 = y − nM , or equivalently
nM = y − y 0
The formula ϕq0 ,q0 can be defined as follows:
ϕq0 ,q0 := M | (y − y 0 ) ∧ y 0 ≤ y ∧^x0 = x.

x∈X\{y}Handling unary Presburger guards: Recalling our reduction for the case with regularconstraints from Section 4 reveals that we also need unary Presburger guards on the
counters. We will show how to extend Lemma 3 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 C = (X, Q, ∆) has Q = {q0 , . . . , qn−1 }, and thecontrol structure is a simple cycle of length n, i.e., the transitions in ∆ are precisely(qi , Φi , qi+1 (mod n) ) for some Presburger formula Φi (x̄, x̄0 ), for each i ∈ [n − 1]. We
say that C is 1-variable-reducing with unary Presburger guards if there exists a countery ∈ X such that each Φi is of the form θi ∧ ψi , where θi is either SUBy,z (with z
a variable distinct from y) or DECy , and ψi is a conjunction of formulas of the formx ∈ Ai ∪ (A0i + bN), where both Ai and A0i are finite sets of natural numbers andx ∈ X. For each counter x ∈ X, we use ψi,x to denote the set of conjuncts in ψi thatrefers to the counter x.
Lemma 4. There exists a polynomial-time algorithm which given a 1-variablereducing cycle with unary Presburger guards C = (X, Q, ∆) and two states p, q ∈ Qcomputes an formula λp,q (x̄, x̄0 ) in existential Presburger arithmetic with divisibility
such that (p, v) →∗C (q, w) iff λp,q (v, w) is satisfiable.
Unlike Lemma 3, this lemma does not immediately follow from the results of [7] onflat parametric counter automata. To prove this, let us first take the formula ϕp,q (x̄, x̄0 )from Lemma 3 applied to C 0 , which is obtained from C by first removing the unary
Presburger guards. We can insert these unary Presburger guards to ϕp,q , but this is notenough because we need to make sure that all “intermediate” values of y have to alsosatisfy the Presburger guards corresponding to y on that control state. More precisely,
let the counter decrement
Pn−1in θi be αi (which can either be a variable x distinct from yor 1). Write f (x̄) = i=0 αi . Then, we can write
λq0 ,q0 := x̄0 = x̄ ∨ϕq0 ,q0 ∧n−1^!
ψi (x̄) ∧ ηq0 ,q0i=0

ηq0 ,q0 := ∀k : y 0 + (k + 1)f (x̄) ≤ y −→


n−1
^
^

y 0 + kf (x̄) + αi ∈ A ∪ (A0 + bN)i=0 (αi ∈A∪A0 +bN)∈ψi,yOwing to the constraint ϕq0 ,q0 , the premise y 0 + (k + 1)f (x̄) ≤ y in ηq0 ,q0 could havebeen rewritten to y 0 + (k + 1)f (x̄) = y. As we shall soon see, the former will be more
useful for completing our proof of Lemma 4. The formula λq0 ,q0 is a correct expressionthat captures the reachability relation (q0 , w) →∗C (q0 , w0 ), but the problem is that it hasa universal quantifier and therefore is not a formula of existential Presburger arithmetic
with divisibility. To fix this problem, we will need to exploit the semilinear structure ofunary Presburger guards. To this end, we first notice that, by taking the big conjunction
over i and the big conjuncton over αi out, the formula ηq0 ,q0 is equivalent to:ηq0 ,q0 ≡

n−1
^

^

∀k : y 0 + (k + 1)f (x̄) ≤ y −→i=0 (αi ∈A∪A0 +bN)∈ψi,y(y 0 + kf (x̄) + αi ∈ A ∪ (A0 + bN))
Therefore, it suffices to rewrite each conjunct C(x̄) := ∀k : y 0 + (k + 1)f (x̄) ≤ y −→(y 0 + kf (x̄) + αi ∈ A ∪ (A0 + bN) as an existential Presburger formula, for each i andconstraint (αi ∈ A ∪ A0 + bN). To this end, let a := max A and let N denote |A0 |. Weclaim that ϕq0 ,q0 entails
C(x̄) ⇔a^y 0 + (i + 1)f (x̄) ≤ y → y 0 + if (x̄) + αi ∈ A ∪ (A0 + bN)

i=0

∧

a+N
^+1

y 0 + (i + 1)f (x̄) ≤ y → y 0 + if (x̄) + αi ∈ A0 + bN.

i=a+1

Simply put, we distinguish the cases when y 0 + if (x̄) + αi is “small” (i.e., less thanthe 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 anonzero period). To prove this equivalence, it suffices to show that if y 0 + kf (x̄) + αi ∈/A ∪ (A0 + bN) with k > a + N + 1 and y 0 + (k + 1)f (x̄) ≤ y (i.e. y 0 + kf (x̄) + αi ≤ ysince y 0 = y + hf (x̄) for some h because of ϕq0 ,q0 ), then we can find k 0 ≤ a + N + 1
such that y 0 + k 0 f (x̄) + αi ∈/ A ∪ (A0 + bN). Suppose to the contrary that such k 0
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 a0 + bN and two different
numbers a + 1 ≤ j1 < j2 ≤ a + N + 1 such that y 0 + jh f (x̄) + αi ∈ a0 + bN,
for h = 1, 2. Let d := (j2 − j1 ). Note that df (x̄) denotes the difference between
y 0 + j1 f (x̄) + αi and y 0 + j2 f (x̄) + αi , and this difference is of the form mb, forsome positive integer m. We now find a number j ∈ [a + 1, a + N ] with j + qd = k
for some positive integer q. Since y 0 + jf (x̄) + αi ∈ a00 + bN for some a00 ∈ A0 , itmust be the case that y 0 + (j + qd)f (x̄) + αi ∈ a00 + bN for q ∈ N, contradicting thaty 0 + kf (x̄) + αi ∈/ A ∪ (A0 + bN).
We have proven correctness, and what remains is to analyse the size of the formula
λq0 ,q0 . To this end, it suffices to show that each formula C(x̄) is of polynomial size.
This is in fact the case since there are at most polynomially many numbers in A and A0
and that the size of all numbers in A ∪ A0 ∪ {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 4. There exists a polynomial-time algorithm which, given a flat Presburger
counter system C = (X, Q, ∆), each of whose simple cycle is 1-variable-reducing withunary Presburger guards and two states p, q ∈ Q, computes an formula λp,q (x̄, x̄0 )in existential Presburger with divisibility such that (p, v) →∗C (q, w) iff λp,q (v, w) issatisfiable.
Indeed, to prove this theorem, we can simply use Lemma 4 to accelerate all cycles andthe fact that transition relations expressed in existential Presburger with divisibility isclosed under composition.

5.3

Application to word equations with length constraints

Theorem 4 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 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 4. In this section, we show completeness of this method
for the class of regular-oriented word equations recently defined in [10], which can beextended with regular constraints given as 1-weak NFA [2]. A word equation is regular
if each variable x ∈ V occurs at most once on each side of the equation. Observe thatxy = yx is regular, but xxyy = zz is not. It is easy to see that a regular word equationis 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 = w1 αw2 βw3 for some w1 , w2 , w3 ∈ (A ∪ V )∗and α, β ∈ V , then α < β. Observe that xy = yz (i.e. that x and z are conjugates)
is oriented, but xy = yx is not oriented. It was shown in [10] that the satisfiability for
regular-oriented word equations is NP-hard. We show satisfiability for this class withlength constraints is decidable.
Theorem 5. 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,in which each variable occurs precisely once on each side, was proven in [9]. For thissubcase, it was shown that Presburger Arithmetic is sufficient, but the decidability forthe general class of regular-oriented word equations with length constraints remained
open. Theorem 5 shows the problem is decidable.
We start with a simple lemma that ⇒ preserves regular-orientedness. Its proof canbe found in the full version.
Lemma 5. If E ⇒ E 0 and E is regular-oriented, then E 0 is also regular-oriented.
Next, we show a bound on the lengths of cycles and paths of the counter systemassociated with a regular-oriented word equation.
Lemma 6. Given a regular-oriented word equation E, the counter system C(E) is flat.
Moreover, the length of each simple cycle (resp. path) in the control structure of C(E)
is of length O(|E|) (resp. O(|E|2 )).
Let E := L = R. We first show that the length of a simple cycle in the control
structure of C(E) is of length at most N = max{|L|, |R|} − 1. Given a simple cycle
E0 ⇒ E1 ⇒ · · · ⇒ En with n > 0 (i.e. E0 = En and Ei 6= Ej for all 0 ≤ 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 |E0 | = |E1 | = · · · = |En |.
Let Ei := Li = Ri with Li = αi wi and Ri = βi wi0 . Let us assume that E1 be
w0 [α0 β0 /β0 ] = β0 w00 [α0 β0 /β0 ]; the case with E1 be α0 w0 [β0 α0 /α0 ] = w00 [β0 α0 /α0 ]will be easily seen to be symmetric. This assumption implies that β0 is a variable y,and that L0 = uyv for some words u, v ∈ (A ∪ V )∗ (for, otherwise, |E1 | < |E0 |because of regularity of E). Furthermore, it follows that, for each i ∈ [n − 1], Ei+1 is
wi [αi y/] = ywi0 and βi = y, i.e., the counter system C(E) applies either SUBy,x (in thecase when x = αi ) or DECy (in the case when αi ∈ A). For, otherwise, taking a minimali ∈ [1, n − 1] with Ei+1 being αi wi [yαi /αi ] = wi0 [yαi /αi ] for some variable x = αishows that Ei is of the form x...y... = y...x... (since |Ei+1 | = |Ei |) contradicting that
Ei is oriented. Consequently, we have
– Ri = Rj for all i, j, and– Li = cyci (u)yv for all i ∈ [n]implying that the length of the cycle is at most |L0 | − 1 ≤ |L| − 1.
Consider the control structure C(E) as a dag of SCCs. In this dag, each edge fromone 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: First, we note that the length abstraction of regularoriented word equations with regular constraints is already not Presburger-definable ingeneral (see full version for proof):
Proposition 4. The regular-oriented word equation xy = yz over the alphabet{a, b, #}, together with regular constraints x, y ∈ #(a + b)∗ has non-Presburgerdefinable length abstraction.
It is difficult to extend Theorem 5 to the case with regular constraints because
they may introduce nestings of cycles (which breaks the flat control structure) evenfor regular-oriented word equation. However, we can show that restricting to regularconstraints given by 1-weak NFA [2] (i.e. a dag of SCCs, each with at most one state)preserves the flat control structure. A 1-weak regular constraint is of the form x ∈ L
where L is accepted by a 1-weak NFA. The class of 1-weak automata is in fact quite
powerful, e.g., when considered as recognisers of languages of ω-words, they capture
the subclass of LTL with operators F and G [2]. They have also been used to obtain adecidable extension of infinite-state concurrent systems in term rewriting systems, e.g.,see [17, 30]. Note that the regular constraint in Proposition 4 is accepted by a 1-weak#a,b

NFA: the NFA has two states q0 and q1 , and transitions q0 −→ q1 and q1 −→ q1 , whereq0 is an initial state and q1 a final state.
Theorem 6. The satisfiability problem of regular-oriented word equations with 1-weakregular 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 C(E, S) = (X, Q, ∆) be the corresponding countersystem. Let M (S) denote the maximum number of states ranging over all NFA in S.
Lemma 7. The counter system C(E, S) is flat. Moreover, the length of each simple
cycle in the control structure of C(E, S) is of length O(|E|), while the length of eachsimple path is of length O(|E|2 |V ||S|M (S)3 ).

By virtue of Theorem 4, this lemma implies decidability of Theorem 6, but it does NOT
imply the nondeterministic exponential time T
upper bound since each unary Presburger
guard in C(E) will be of the form x ∈ L EN( (x∈L)∈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 canbe found in the full version.
Remark 1. Our proof of Theorem 6 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.

6

Future WorkOne research direction is to study extensions of our techniques to deal with the classof 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 withlength constraints. We also conjecture that the length abstractions of general quadratic
word equations can be effectively captured by existential Presburger with divisibility.
Acknowledgment. We thank Jatin Arora, Dmitry Chistikov, Volker Diekert, Matthew
Hague, Artur Jeż, Philipp Rümmer, and James Worrell for the helpful discussions. This
research was partially funded by the ERC Starting Grant AV-SMP (grant agreement no.
759969) and the ERC Synergy Grant IMPACT (grant agreement no. 610150).

References
1. P. A. Abdulla, M. F. Atig, Y. Chen, L. Holı́k, A. Rezine, P. Rümmer, and J. Stenman. String
constraints for verification. In CAV, pages 150–166, 2014.
2. T. Babiak, V. Rehák, and J. Strejcek. Almost linear Büchi automata. Mathematical Structuresin Computer Science, 22(2):203–235, 2012.
3. S. Bardin, A. Finkel, J. Leroux, and L. Petrucci. FAST: acceleration from theory to practice.
STTT, 10(5):401–424, 2008.
4. S. Bardin, A. Finkel, J. Leroux, and P. Schnoebelen. Flat acceleration in symbolic model
checking. In ATVA, pages 474–488, 2005.
5. M. Berzish, V. Ganesh, and Y. Zheng. Z3str3: A string solver with theory-aware heuristics.
In FMCAD, pages 55–59, 2017.
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. M. Chrobak. Finite automata and unary languages. Theor. Comput. Sci., 47(3):149–158,
1986.
9. J. D. Day et al. The satisfiability of extended word equations: The boundary between decidability and undecidability. CoRR, abs/1802.00523, 2018.

10. J. D. Day, F. Manea, and D. Nowotka. The hardness of solving simple word equations. In
MFCS, pages 18:1–18:14, 2017.
11. 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.
12. 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.
13. V. Ganesh et al. Word equations with length constraints: what’s decidable? In Hardware andSoftware: Verification and Testing, pages 209–226. Springer, 2013.
14. L. Holı́k, P. Janku, A. W. Lin, P. Rümmer, and T. Vojnar. String constraints with concatenation and transducers solved efficiently. PACMPL, 2(POPL):4:1–4:32, 2018.
15. A. Jéz. Recompression: a simple and powerful technique for word equations. In STACS
2013, LIPIcs, Vol. 20, pages 233–244, 2013.
16. A. Kiezun et al. HAMPI: A solver for word equations over strings, regular expressions, andcontext-free grammars. ACM Trans. Softw. Eng. Methodol., 21(4):25, 2012.
17. M. Kretı́nský, V. Rehák, and J. Strejcek. Reachability is decidable for weakly extended
process rewrite systems. Inf. Comput., 207(6):671–680, 2009.
18. A. Lechner, J. Ouaknine, and J. Worrell. On the complexity of linear arithmetic with divisibility. In LICS 15: Logic in Computer Science. IEEE, 2015.
19. A. Lentin. Equations dans les Monoides Libres. Gauthier-Villars, Paris, 1972.
20. 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.
21. T. Liang, A. Reynolds, C. Tinelli, C. Barrett, and M. Deters. A DPLL(T) theory solver for atheory of strings and regular expressions. In CAV, pages 646–662, 2014.
22. A. W. Lin and P. Barceló. String solving with word equations and transducers: towards a
logic for analysing mutation XSS. In POPL, pages 123–136, 2016.
23. L. Lipshitz. The Diophantine problem for addition and divisibility. Transactions of theAmerican Mathematical Society, 235:271–283, 1976.
24. G. S. Makanin. The problem of solvability of equations in a free semigroup. Sbornik:
Mathematics, 32(2):129–198, 1977.
25. A. Martinez. Efficient computation of regular expressions from unary NFAs. In In DFCS,
pages 174–187, 2002.
26. Y. Matiyasevich. A connection between systems of words-and-lengths equations andHilberts tenth problem. Zapiski Nauchnykh Seminarov POMI, 8:132–144, 1968.
27. R. Parikh. On context-free languages. J. ACM, 13(4):570–581, 1966.
28. P. Saxena, D. Akhawe, S. Hanna, F. Mao, S. McCamant, and D. Song. A symbolic execution
framework for JavaScript. In S&P, pages 513–528, 2010.
29. A. W. To. Unary finite automata vs. arithmetic progressions. Inf. Process. Lett.,
109(17):1010–1014, 2009.
30. A. W. To and L. Libkin. Algorithmic metatheorems for decidable LTL model checking overinfinite systems. In FOSSACS, 2010.
31. M. Trinh, D. Chu, and J. Jaffar. S3: A symbolic string solver for vulnerability detection in
web applications. In CCS, pages 1232–1243, 2014.
32. 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.
33. 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.