On Multiphase-Linear Ranking Functions
arXiv:1703.07547v2 [] 23 Mar 2017

Amir M. Ben-Amram∗1 and Samir Genaim†2
1

The Academic College of Tel-Aviv Yaffo
2
Complutense University of Madrid
March 24, 2017

Abstract
Multiphase ranking functions (MΦRFs) were proposed as a means to prove
the termination of a loop in which the computation progresses through a number of “phases”, and the progress of each phase is described by a different linear
ranking function. Our work provides new insights regarding such functions for
loops described by a conjunction of linear constraints (single-path loops). We
provide a complete polynomial-time solution to the problem of existence and of
synthesis of MΦRF of bounded depth (number of phases), when variables range
over rational or real numbers; a complete solution for the (harder) case that variables are integer, with a matching lower-bound proof, showing that the problem
is coNP-complete; and a new theorem which bounds the number of iterations for
loops with MΦRFs. Surprisingly, the bound is linear, even when the variables involved change in non-linear way. We also consider a type of lexicographic ranking
functions, LLRF , more expressive than types of lexicographic functions for which
complete solutions have been given so far. We prove that for the above type of
loops, lexicographic functions can be reduced to MΦRFs, and thus the questions
of complexity of detection and synthesis, and of resulting iteration bounds, are
also answered for this class.
∗
†

amirben@mta.ac.il
samir.genaim@fdi.ucm.es

1

1

Introduction

Proving that a program will not go into an infinite loop is one of the most fundamental
tasks of program verification, and has been the subject of voluminous research. Perhaps
the best known, and often used, technique for proving termination is the ranking function. This is a function f that maps program states into the elements of a well-founded
ordered set, such that f (s) > f (s′ ) holds whenever states s′ follows state s. This implies
termination since infinite descent in a well-founded order is impossible. Unlike termination of programs in general, which is the fundamental example of undecidability, the
algorithmic problems of detection (deciding the existence) or generation (synthesis) of
a ranking function can well be solvable, given certain choices of the program representation, and the class of ranking function. Numerous researchers have proposed such
classes, with an eye towards decidability; in some cases the algorithmic problems have
been completely settled, and efficient algorithms provided, while other cases remain as
open problems. Thus, in designing ranking functions, we look for expressivity (to capture more program behaviors) but also want (efficient) computability. Besides proving
termination, some classes of ranking functions also serve to bound the length of the
computation (an iteration bound ), which is useful in applications such as cost analysis (related terms: execution-time analysis, resource analysis) and loop optimization
[13, 2, 1, 6].
We focus on single-path linear-constraint loops (SLC loops for short), where a state
is described by the values of a finite set of numerical variables, and the effect of a
transition (one iteration of the loop) is described by a conjunction of linear constraints.
We consider the setting of integer-valued variables, as well as rational-valued (or realvalued) variables1 . Here is an example of this loop representation (a formal definition
is in Section 2); primed variables x′ , y ′, . . . refer to the state following the transition.
while (x ≥ −z) do x′ = x + y, y ′ = y + z, z ′ = z − 1

(1)

Note that by x′ = x + y we mean an equation, not an assignment statement; it is a
standard procedure to compile sequential code into such equations (if the operations
used are linear), or to approximate it using various techniques.
This constraint representation may be extended to represent branching in the loop
body, a so-called multiple-path loop; in the current work we do not consider such loops.
However, SLC loops are important already, in particular in approaches that reduce a
question about a whole program to questions about simple loops [15, 19, 12, 9, 10]; see
[21] for references that show the importance of +such loops in other fields. We assume
1

For the results in this paper, the real-number case is equivalent to the rational-number case, and
in the sequel we refer just to rationals.

2

the “constraint loop” to be given, and do not concern ourselves with the orthogonal
topic of extracting a loop representation from an actual program (note that in some applications, such as analyzing dynamical systems of various kinds, we may start not with
a computer program but with a model, expressed by its creator as a set of constraints).
Types of ranking functions. Several types of ranking functions have been suggested; linear ranking functions (LRFs) are probably the most widely used and wellunderstood. In this case, we seek a function f (x1 , . . . , xn ) = a1 x1 + · · · + an xn + a0 ,
with the rationals as a co-domain, such that (i) f (x̄) ≥ 0 for any valuation x̄ that
satisfies the loop constraints (i.e., an enabled state); and (ii) f (x̄) − f (x̄′ ) ≥ 1 for any
transition leading from x̄ to x̄′ . Technically, the rationals are not a well-founded set
under the usual order, but we can refer to the partial order a  b if and only if a ≥ 0
and a ≥ b + 1, which is well-founded. Given a linear-constraint loop, it is possible
to find a linear ranking function (if one exists) using linear programming (LP). This
method was found by multiple researchers in different places and times and in some
alternative versions [13, 25, 8, 22]. Since LP has a polynomial-time complexity, most of
these methods yield polynomial-time algorithms. This method is sound (any ranking
function produced is valid), and complete (if there is a ranking function, it will find
one), when variables are assumed to range over the rationals. When variables range
over the integers, treating the domain as Q is safe, but completeness is not guaranteed.
Consider the following loop:
while (x2 − x1 ≤ 0, x1 + x2 ≥ 1) do x′2 = x2 − 2x1 + 1, x′1 = x1

(2)

and observe that it does not terminate over the rationals at all (try x1 = x2 = 12 );
but it has a LRF that is valid for all integer valuations, e.g., f (x1 , x2 ) = x1 + x2 .
Several authors noted this issue, and finally the complexity of a complete solution for
the integers was settled by [4], who proved that the detection problem is coNP-complete
and gave matching algorithms.
However, not all terminating loops have a LRF; and to handle more loops, one
may resort to an argument that combines several LRFs to capture a more complex
behavior. Two types of such behavior that re-occur in the literature on termination are
lexicographic ranking and multiphase ranking.
Lexicographic ranking. One can prove the termination of a loop by considering a
tuple, say a pair hf1 , f2 i of linear functions, such that either f1 decreases, or f1 does not
change and f2 decreases. There are some variants of the definition [5, 2, 4, 17] regarding
whether both functions have to be non-negative at all times, or “just when necessary.”
The most permissive definition allows any component to be negative, and technically,
it ranks states in the lexicographic extension of the order  mentioned above. We refer
3

to this class as LLRFs, and are only aware of one work where this class is used in its
full generatlity [17]. For example, the following loop
while (x ≥ 0, y ≤ 10, z ≥ 0, z ≤ 1) do x′ = x + y + z − 10, y ′ = y + z, z ′ = 1 − z (3)
has the LLRF h4y, 4x − 4z + 1i, which is valid only according to the defintion of [17],
since it allows the first component to be negative for transitions that are ranked by the
second component.
Multiphase ranking. Consider loop (1) above. Clearly, the loop goes through three
phases — in the first, z descends, while the other variables may increase; in the second
(which begins once z becomes negative), y decreases; in the last phase (beginning when
y becomes negative), x decreases. Note that since there is no lower bound on y or on z,
they cannot be used in a LRF ; however, each phase is clearly finite, as it is associated
with a value that is non-negative and decreasing during that phase. In other words,
each phase is linearly ranked. We shall say that this loop has the multiphase ranking
function (MΦRF) hz + 1, y + 1, xi. The general definition (Section 2) allows for an
arbitrary number d of linear components; we refer to d as depth, intuitively it is the
number of phases.
Some loops have multiphase behavior which is not so evident as in the last example.
Consider the following loop, that we will discuss further in Section 6, with MΦRF
hx − 4y, x − 2y, x − yi
while (x ≥ 1, y ≥ 1, x ≥ y, 4y ≥ x) do x′ = 2x, y ′ = 3y

(4)

Technically, under which ordering is a MΦRF a ranking function? It is quite easy to
see that the pairs used in the examples above descend in the lexicographic extension
of . This means that MΦRFs are a sub-class of LLRFs. Note that, intuitively, a
lexicographic ranking function also has “phases”, namely, steps where the first component decreases, steps where the second component decreases, etc.; but these phases
may alternate an unbounded number of times.
Complete solutions and complexity. Complete solutions for MΦRFs (over the
rationals) appear in [18, 20]. Both use non-linear constraint solving, and therefore do
not achieve a polynomial time complexity. [3] study “eventual linear ranking functions,”
which are MΦRFs of depth 2, and pose the question of a polynomial-time solution as
an open problem, as well as the problem of a complete solution for the integers.
In this paper, we provide complete solutions to the existence and synthesis problems
for both MΦRFs and LLRFs, for rational and integer SLC loops, where the algorithm
is parameterized by a depth bound. Over the rationals, the decision problem is PTIME
4

and the synthesis can be done in polynomial time; over the integers, the existence
problem is coNP-complete, and our synthesis procedure is deterministic exponentialtime.
While such algorithms would be a contribution in itself, we find it even more interesting that our results are mostly based on discovering unexpected equivalences between
classes of ranking functions. We prove two such results: Theorem 4.4 in Section 4
shows that LLRFs are not stronger than MΦRFs for SLC loops. Thus, the complete
solution for LLRFs is just to solve for MΦRFs (for the loop (3), we find the MΦRF
h4y + x − z, 4x − 4z + 4i). Theorem 3.4 in Section 3 shows that one can further reduce
the search for MΦRFs to a proper sub-class, called nested MΦRFs. This class was
introduced in [18] because its definition is simpler and allows for a polynomial-time
solution (over Q). Thus, our equivalence result immediately implies a polynomial-time
solution for MΦRFs.
Our complete solution for the integers is also a reduction—transforming the problem
so that solving over the rationals cannot give false alarms. The transformation consists
of computing the integer hull of the transition polyhedron. This transformation is wellknown in the case of LRFs [13, 11, 4], so it was a natural approach to try, however its
proof in the case of MΦRFs is more involved.
We also make a contribution towards the use of MΦRFs in deriving iteration bounds.
As the loop (1) demonstrates, it is possible for the variables that control subsequent
phases to grow (at a polynomial rate) during the first phase. Nonetheless, we prove
that any MΦRF implies a linear bound on the number of iterations for a SLC loop (in
terms of the initial values of the variables). Thus, it is also the case that any LLRF
implies a linear bound.
An open problem raised by our work is whether one can precompute a bound on the
depth of a MΦRF for a given loop (if there is one); for example [4] prove a depth bound
of n (the number of variables) on their notion of LLRFs (which is more restrictive);
however their class is known to be weaker than MΦRFs and LLRFs. In Section 6 we
discuss this problem.
The rest of this article is organized as follows. Section 2 gives precise definitions
and some technical background necessary for this work. Sections 3 and 4 give our
equivalence results for different types of ranking functions (over the rationals) and the
algorithmic implications. Section 5 covers the integer setting, Section 6 discusses depth
bounds, Section 7 discusses the iteration bound, and Section 8 concludes.

5

2

Preliminaries

In this section we give the fundamental definitions for this paper: we define the class
of loops we study, the type of ranking functions, and recall some definitions regarding
(integer) polyhedra. We also mention some important properties of these definitions.

2.1

Single-Path Linear-Constraint Loops

A single-path linear-constraint loop (SLC for short) over n variables x1 , . . . , xn has the
form
 
x
(5)
while (Bx ≤ b) do A ′ ≤ c
x
where x = (x1 , . . . , xn )T and x′ = (x′1 , . . . , x′n )T are column vectors, and for some
p, q > 0, B ∈ Qp×n , A ∈ Qq×2n , b ∈ Qp , c ∈ Qq . The constraint Bx ≤ b is called the
loop condition (a.k.a. the loop guard) and the other constraint is called the update. We
say that the loop is a rational loop if x and x′ range over Qn , and that it is an integer
loop if they range over Zn . One could also allow variables to take any real-number
values, but as long as the constraints are expressed by rational numbers this makes no
difference from the rational case.
We say that there is a transition from a state x ∈ Qn to a state x′ ∈ Qn , if
x satisfies the condition and x and x′ satisfy the update. A transition can be seen
as a point xx′ ∈ Q2n , where its first n components correspond to x and its last n
components to x′ . For ease of notation, we denote xx′ by x′′ . The set of all transitions
x′′ ∈ Q2n , of a given SLC loop, will be denoted by Q and is specified by the set of
inequalities A′′ x′′ ≤ c′′ where

 

b
B 0
′′
′′
c =
A =
c
A
We call Q the transition polyhedron (for definitions regarding polyhedra see Sect. 2.3).
For the purpose of this article, the essence of the loop is this polyhedron, even if the
loop is presented in a more readable form as (5).

2.2

Multi-Phase Ranking Functions

An affine function f : Qn → Q is of the form f (x) = ~a · x + a0 where ~a ∈ Qn is a row
vector and a0 ∈ Q. For a given function f , we define the function ∆f : Q2n 7→ Q as
∆f (x′′ ) = f (x) − f (x′ ).

6

Definition 2.1 (MΦRF). Given a set of transitions T ⊆ Q2n , we say that τ =
hf1 , . . . , fd i is a MΦRF (of depth d) for T if for every x′′ ∈ T there is an index i ∈ [1, d]
such that:
∀j ≤ i . ∆fj (x′′ ) ≥ 1 ,
fi (x) ≥ 0 ,
∀j < i .
fj (x) ≤ 0 .

(6)
(7)
(8)

We say that x′′ is ranked by fi (for the minimal such i).
It is not hard to see that this definition, for d = 1, means that f1 is a linear ranking
function, and for d > 1, it implies that as long as f1 (x) ≥ 0, transition x′′ must be
ranked by f1 , and when f1 (x) < 0, hf2 , . . . , fd i becomes a MΦRF. This agrees with the
intuitive notion of a “phases.” We further note that, for loops specifies by polyhedra,
making the inequality (8) strict results in the same class of ranking functions (we
chose the definition that is easier to work with), and, similarly, we can replace (6) by
∆fj (x′′ ) > 0, obtaining an equivalent definition (up to multiplication of the fi by some
constants). We say that τ is irredundant if removing any component invalidates the
MΦRF. Finally, it is convenient to allow an empty tuple as a MΦRF for the empty set.
The decision problem Existence of a MΦRF asks to determine whether a given
SLC loop admits a MΦRF. We denote this problem by EMΦRF(Q) and EMΦRF(Z)
for rational and integer loops respectively. The bounded decision problem, denoted by
BMΦRF(Q) and BMΦRF(Z), restricts the search to MΦRFs of depth at most d, where
the parameter d is part of the input.

2.3

Polyhedra

A rational convex polyhedron P ⊆ Qn (polyhedron for short) is the set of solutions of
a set of inequalities Ax ≤ b, namely P = {x ∈ Qn | Ax ≤ b}, where A ∈ Qm×n is
a rational matrix of n columns and m rows, x ∈ Qn and b ∈ Qm are column vectors
of n and m rational values respectively. We say that P is specified by Ax ≤ b. If
b = 0, then P is a cone. The set of recession directions of a polyhedron P specified by
Ax ≤ b, also know as its recession cone, is the set rec.cone(P) = {y ∈ Qn | Ay ≤ 0}.
For a given polyhedron P ⊆ Qn we let I(P) be P ∩ Zn , i.e., the set of integer points
of P. The integer hull of P, commonly denoted by PI , is defined as the convex hull
of I(P), i.e., every rational point of PI is a convex combination of integer points. It is
known that PI is also a polyhedron, and that rec.cone(P) = rec.cone(PI ). An integer
polyhedron is a polyhedron P such that P = PI . We also say that P is integral.
Polyhedra also have a generator representation in terms of vertices and rays, written
as P = conv.hull{x1 , . . . , xm } + cone{y1 , . . . , yt } . This means that x ∈ P iff x =
7

Pm

P
P
ai · xi + tj=1 bj · yj for some rationals ai , bj ≥ 0, where m
i=1 ai = 1. Note that
P
y1 , . . . , yt are the recession directions of P, i.e., y ∈ rec.cone(P) iff y = tj=1 bj · yj
for some rationals bj ≥ 0. If P is integral, then there is a generator representation in
which all xi and yj are integer.
Next we state some lemmas that are fundamental for many proofs in this article.
Given a polyhedron P, the lemmas show that if a disjunction of constraints of the form
fi > 0, or fi ≥ 0, holds over P, then a certain conic combination of these functions is
positive (or non-negative) over P. This generalizes Lemma 1 of [16]. The lemmas are
all very similar, but vary in the the use strict or non-strict inequalities.
i=1

LEMMA 2.2. Given a non-empty polyhedron P, and linear functions f1 , . . . , fk such
that
(i) x ∈ P → f1 (x) > 0 ∨ · · · ∨ fk−1 (x) > 0 ∨ fk (x) ≥ 0
(ii) x ∈ P 6→ f1 (x) > 0 ∨ · · · ∨ fk−1 (x) > 0
There exist non-negative constants µ1 , . . . , µk−1 such that
x ∈ P → µ1 f1 (x) + · · · + µk−1fk−1 (x) + fk (x) ≥ 0 .
Proof. Let P be Bx ≤ c, fi = ~ai · x − bi , then (i ) is equivalent to infeasibility of
Bx ≤ c ∧ Ax ≤ b ∧ ~ak · x < bk

(9)

where A consists of the k − 1 rows ~ai , and b of corresponding bi . However, Bx ≤
c ∧ Ax ≤ b is assumed to be feasible.
According to Motzkin’s transposition theorem [24, Corollary 7.1k, Page 94], this
implies that there are row vectors ~λ, ~λ′ ≥ 0 and a constant µ ≥ 0 such that the
following is true:
~λB + ~λ′ A + µak = 0 ∧ ~λc + ~λ′ b + µbk ≤ 0 ∧ (µ 6= 0 ∨ ~λc + ~λ′ b + µbk < 0)

(10)

Now, if (10) is true, then for all x ∈ P,
X
(
λ′i fi (x)) + µfk (x) = ~λ′ Ax − ~λ′ b + µak x − µbk
i

= −~λBx − ~λ′ b − µbk ≥ −~λc − ~λ′ b − µbk ≥ 0
where if µ = 0, the last inequality must be strict. However, if µ = 0, then ~λB + ~λ′ A = 0,
so by feasibility
of Bx ≤ c and Ax ≤ b, this implies ~λc + ~λ′ b ≥ 0, a contradiction.
P ′
Thus, ( i λi fi ) + µfk ≥ 0 on P and µ > 0. Dividing by µ we obtain the conclusion of
the lemma.
8

LEMMA 2.3. Given a non-empty polyhedron P, and linear functions f1 , . . . , fk such
that
(i) x ∈ P → f1 (x) ≥ 0 ∨ · · · ∨ fk (x) ≥ 0
(ii) x ∈ P 6→ f1 (x) ≥ 0 ∨ · · · ∨ fk−1 (x) ≥ 0
There exists non-negative constants µ1 , . . . , µk−1 such that
x ∈ P → µ1 f1 (x) + · · · + µk−1fk−1 (x) + fk (x) ≥ 0 .
Proof. Let P be Bx ≤ c, fi = ~ai x − bi , then (i ) is equivalent to infeasibility of Bx ≤
c ∧ Ax < b. According to Motzkin’s transposition theorem, this implies that there are
row vectors ~λ, ~µ ≥ 0 such that the following is true:
~λB + ~µA = 0 ∧ ~λc + ~µb ≤ 0

∧ (~µ 6= 0 ∨ ~λc + µ
~ b < 0)

(11)

Now, if (11) is true, then for all x ∈ P,
X
µi fi (x) = ~µAx − ~µb = −~λBx − ~µb ≥ −~λc − µ
~b ≥ 0
i

where if ~µ = 0, the last inequality must be strict. However, if µ
~ = 0, then ~λB = 0,
so by feasibility of P P
and feasibility of Bx ≤ c and Ax ≤ b, this implies ~λc ≥ 0, a
contradiction. Thus, i µi fi ≥ 0 on P and ~µ 6= 0. Based on assumption (ii ), such a
combination must include fk with a positive coefficient, and therefore can be normalized
to the stated form.

3

Complexity of Synthesis of MΦRFs over the Rationals

In this section we study the complexity of deciding if a given rational SLC loop has
a MΦRF of depth d, and show that this can be done in polynomial time. These
results follow from an equivalence between MΦRFs and a sub-class called nested ranking
functions [18]. In the rest of this article we assume a given SLC loop specified by a
transition polyhedron Q. The complexity results assume a constraint representation
for Q, as in Section 2.1.

9

Definition 3.1. A d-tuple τ = hf1 , . . . , fd i is a nested ranking function for Q if the
following requirements are satisfied for all x′′ ∈ Q
fd (x) ≥ 0
(∆fi (x′′ ) − 1) + fi−1 (x) ≥ 0

for all i = 1, . . . , d.

(12)
(13)

where for uniformity we define f0 ≡ 0.
It is easy to see that a nested ranking function is a MΦRF. Indeed, f1 is decreasing,
and when it becomes negative f2 starts to decrease, etc. In addition, the loop must
stop by the time that the last component becomes negative, since fd is non-negative on
all enabled states.
EXAMPLE 3.2. Consider loop (1) (on Page 2). It has the MΦRF hz + 1, y + 1, xi
which is not nested because, among other things, last component x might be negative,
e.g., for the state x = −1, y = 0, z = 1. However, it has the nested ranking function
hz + 1, y + 1, z + xi, which is MΦRF.
The above example shows that there are MΦRFs which are not nested ranking
functions, however, next we show that if a loop has a MΦRF then it has (possibly
different) nested ranking function of the same depth. We first state an auxiliary lemma,
and then prove the main result.
LEMMA 3.3. Let τ = hf1 , . . . , fd i be an irredundant MΦRF for Q, such that hf2 , . . . , fd i
is a nested ranking function for Q′ = Q ∩ {x′′ ∈ Q2n | f1 (x) ≤ 0}. Then there is a
nested ranking function of depth d for Q.
Proof. First recall that, by definition of MΦRF, we have ∆f1 (x′′ ) ≥ 1 for any x′′ ∈ Q,
and since hf2 , . . . , fd i is a nested ranking function for Q′ we have
x′′ ∈ Q′ →fd (x) ≥ 0
x′′ ∈ Q′ →(∆f2 (x′′ ) − 1) + f0 (x′′ ) ≥ 0 ∧
(∆f3 (x′′ ) − 1) + f2 (x′′ ) ≥ 0 ∧
..
.
(∆fd (x′′ ) − 1) + fd−1 (x′′ ) ≥ 0

(14)

Next we construct a nested ranking function hf1′ , . . . , fd′ i for Q, i.e., such that (12) is
′
satisfied for fd′ , and (13) is satisfied for each fi′ and fi−1
— we refer to the instance of
(13) for a specific i as (13i ).
10

We start with the condition (12). If fd is non-negative over Q we let fd′ = fd ,
otherwise, clearly
x′′ ∈ Q → fd (x) ≥ 0 ∨ f1 (x) > 0 .
Then, by Lemma 2.2 there is a constant µd > 0 such that
x′′ ∈ Q → fd (x) + µd f1 (x) ≥ 0
and we define fd′ (x) = fd (x) + µd f1 (x). Clearly (12) holds for fd′ .
Next, we handle the conditions (13i ) for i = d, . . . , 3 in this order. When we handle
′
condition (13i ), we shall define fi−1
(x) = fi−1 (x) + µi−1 f1 (x) for some µi−1 ≥ 0. Note
′
that fd has this form as well.
Suppose we have computed fd′ , . . . , fi′ . We show how to ensure that (13i ) holds over
′
Q by constructing fi−1
. From (14) we know that
x′′ ∈ Q′ → (∆fi (x′′ ) − 1) + fi−1 (x′′ ) ≥ 0 .
Now since fi′ (x) = fi (x) + µi f1 (x), and ∆f1 (x′′ ) ≥ 1 over Q, we have
x′′ ∈ Q′ → (∆fi′ (x′′ ) − 1) + fi−1 (x′′ ) ≥ 0 .
′
= fi−1 . Otherwise,
Now if (∆fi′ (x′′ ) − 1) + fi−1 (x′′ ) ≥ 0 holds over Q as well, we let fi−1
we have
x′′ ∈ Q → (∆fi′ (x′′ ) − 1) + fi−1 (x) ≥ 0 ∨ f1 (x) > 0 ,

and by Lemma 2.2 there is µi−1 > 0 such that
x′′ ∈ Q → (∆fi′ (x′′ ) − 1) + fi−1 (x) + µi−1 f1 (x) ≥ 0 .
′
In this case, we let fi−1
(x) = fi−1 (x) + µi−1 f1 (x). Clearly (13i ) holds.
Next we proceed to (132 ). From (14) we know that

x′′ ∈ Q′ → (∆f2 (x′′ ) − 1) + f1 (x′′ ) ≥ 0 .
Since f2′ = f2 + µ2 f1 and ∆f1 (x′′ ) ≥ 1 we have
x′′ ∈ Q′ → (∆f2′ (x′′ ) − 1) + f1 (x′′ ) ≥ 0 .
Next, by definition of Q′ and the lemma’s assumption we have
x′′ ∈ Q → (∆f2′ (x′′ ) − 1) ≥ 0 ∨ f1 (x) > 0
11

and we also know that (∆f2′ (x′′ ) − 1) ≥ 0 does not hold over Q, because then f1 would
be redundant. Now by Lemma 2.2 there is µ1 > 0 such that
x′′ ∈ Q → (∆f2′ (x′′ ) − 1) + µ1 f1 (x) ≥ 0 .
We let f1′ (x) = µ1 f1 (x). For (131 ) we need to show that ∆f1′ (x′′ ) − 1 ≥ 0 holds over
Q, which clearly true if µ1 ≥ 1 since ∆f1 ≥ 1, otherwise we multiply all fi′ by µ11 which
does not affect any (13i ) and makes (131 ) true.
THEOREM 3.4. If Q has a MΦRF of depth d, then it has a nested ranking function
of depth at most d.
Proof. The proof is by induction on d. We assume a MΦRF hf1 , . . . , fd i for Q. For
d = 1 there is no difference between a general MΦRF and a nested one. For d > 1,
we consider hf2 , . . . , fd i as a MΦRF for Q′ = Q ∩ {x′′ ∈ Q2n | f1 (x) ≤ 0}, we apply
the induction hypothesis to turn hf2 , . . . , fd i into a nested ranking function. Either f1
becomes redundant, or we can apply Lemma 3.3.
The above theorem give us a complete algorithm for the synthesis of MΦRFs of a
given depth d for Q, i.e., for rational SLC loops, namely, we synthesize a nested ranking
function.
THEOREM 3.5. BMΦRF (Q) ∈ PTIME.
Proof. We describe, in some detail, how to synthesize a nested ranking function in
polynomial time (this actually appears in [18]). Due to Theorem 3.4, this yields a
complete decision procedure for MΦRFs. Given Q, our goal is to find f1 , . . . , fd such
that (12,13) hold. If we take just one of the conjuncts, our task is to find coefficients for
the functions involved (fd , or fi and fi−1 ), such that the desired inequality is implied by
Q. Using Farkas’ lemma [24], this problem can be formulated as a LP problem, where
the coefficients we seek are unknowns. By conjoing all these LP problems, we obtain
a single LP problem, of polynomial size, whose solution—if there is one—provides the
coefficients of all fi ; and if there is no solution, then no nested ranking function exists.
Since LP is polynomial-time, this procedure has polynomial time complexity.
Clearly, if d is considered as constant, then BMΦRF (Q) is polynomial in the bit-size
of the input Q. When considering d as variable, then the complexity is polynomial in
the bit-size of Q plus d—equivalently, it is polynomial in the bit-size of the input if we
assume that d is given in unary representation (which is a reasonable assumption since
d describes the number of components of the MΦRF sought). The same observation
applies to our classification of BMΦRF (Z) (Section 5).
12

4

Multiphase vs Lexicographic-Linear Ranking Functions

MΦRFs are similar to LLRFs, and a natural question is: which one is more powerful
for proving termination of SLC loops? In this section we show that they have the same
power, by proving that an SLC has a MΦRF if and only if it has a LLRF . We first
note that there are several definitions for LLRFs [5, 2, 4, 17]. The following is the most
general one [17].
Definition 4.1. Given a set of transitions T ⊆ Q2n , we say that hf1 , . . . , fd i is a LLRF
(of depth d) for T if for every x′′ ∈ T there is an index i such that:
∀j < i . ∆fj (x′′ ) ≥ 0 ,
∆fi (x′′ ) ≥ 1 ,
fi (x) ≥ 0 ,

(15)
(16)
(17)

We say that x′′ is ranked by fi (for the minimal such i).
Regarding other definitions: [4] requires (17) to hold for all fj with j ≤ i, and [2]
requires (17) to hold for all components. They are clearly more restrictive. Actually [2]
shows that an SLC loop has a LLRF according to their definition if and only if it has
a LRF , which is not the case of [4]. The definition of [5] is equivalent to a LRF when
considering SLC loops, as their main interest is in multipath loops.
It is easy to see that a MΦRF is also a LLRF as in Definition 4.1. Next we show
that for SLC loops any LLRF can be converted to a MΦRF, proving that these classes
of ranking functions have the same power for SLC loops. We start with an auxiliary
lemma.
LEMMA 4.2. Let f be a non-negative linear function over Q. If Q′ = Q ∩ {x′′ |
∆f (x′′ ) ≤ 0} has a MΦRF of depth d, then Q has a MΦRF of depth at most d + 1.
Proof. Note that simply appending f to a MΦRF τ of Q′ does not always produce a
MΦRF, since the components of τ are not guaranteed to decrease over Q \ Q′ . Let
τ = hg1 , . . . , gd i be a MΦRF for Q′ , we show how to construct a MΦRF hg1′ , . . . , gd′ , f i.
If g1 is decreasing over Q, we define g1′ (x) = g1 (x), otherwise we have
x′′ ∈ Q → ∆f (x′′ ) > 0 ∨ ∆g1 (x′′ ) ≥ 1,
then by Lemma 2.2 we can construct g1′ (x) = g1 (x) + µf (x) such that x′′ ∈ Q →
∆g1′ (x′′ ) ≥ 1. Moreover, since f is non-negative g1′ is non-negative on the transitions
13

on which g1 is non-negative. If d > 1, we proceed with Q(1) = Q ∩ {x′′ | g1′ (x) ≤ (−1)}.
Note that these transitions must be ranked, in Q′ , by hg2 , . . . , gdi. If g2 is decreasing
over Q(1) , let g2′ = g2 , otherwise
x′′ ∈ Q(1) → ∆f (x′′ ) > 0 ∨ ∆g2 (x′′ ) ≥ 1,
and again by Lemma 2.2 we can construct the desired g2′ . In general for any j ≤ d we
′
′
construct gj+1
such that ∆gj+1
≥ 1 over
Q(j) = Q ∩ {x′′ ∈ Q2n | g1′ (x) ≤ (−1) ∧ · · · ∧ gj′ (x) ≤ (−1)}
and x′′ ∈ Q ∧ gj (x) ≥ 0 → gj′ (x) ≥ 0. Finally we define
Q(d) = Q ∩ {x′′ ∈ Q2n | g1′ (x) ≤ (−1) ∧ gd′ (x) ≤ (−1)},
each transition x′′ ∈ Q(d) must satisfy ∆f (x′′ ) > 0, and in such case ∆f (x′′ ) must have
a minimum c > 0 since Q(d) is a polyhedron. Without loss of generality we assume
c ≥ 1, otherwise take 1c f instead of f . Now τ ′ = hg1′ + 1, . . . , gd′ + 1, f i is a MΦRF for
Q. Note that if we arrive to Q(j) that is empty, we can stop since we already have a
MΦRF.
In what follows, by a weak LLRF we mean the class of ranking functions obtained
by changing condition (16) to ∆fi (x′′ ) > 0. Clearly it is more general than LLRFs,
and as we will see next it suffices guarantees termination since we show how to convert
them to MΦRFs. We prefer to use this class as it simplifies the proof of the integer
case that we present in Section 5.
LEMMA 4.3. Let hf1 , . . . , fd i be a weak LLRF for Q. There is a linear function g
that is positive over Q, and decreasing on (at least) the same transitions of fi , for some
1 ≤ i ≤ d.
Proof. If any fi is positive over Q, we take g = fi . Otherwise, we have x′′ ∈ Q →
f1 (x) ≥ 0∨· · ·∨fd (x) ≥ 0 since every transition is ranked by some fi . If thisPimplication
satisfies the conditions of Lemma 2.3 then we can construct g(x) = fd (x)+ d−1
i=1 µi fi (x)
that is non-negative over Q, and, moreover, decreases on the transitions that are ranked
by fd . If the conditions of Lemma 2.3 are not satisfied, then the second condition must
be false, that is, x′′ ∈ Q → f1 (x) ≥ 0 ∨ · · · ∨ fd−1 (x) ≥ 0. Now we repeat the
same reasoning as above for this implication. Eventually we either construct g that
corresponds for some fi as above, or we arrive to x′′ ∈ Q → f1 (x) ≥ 0, and then take
g = f1 .
14

THEOREM 4.4. If Q has a weak LLRF of depth d, it has a MΦRF of depth d.
Proof. Let hf1 , . . . , fd i be a weak LLRF for Q. We show how to construct a corresponding MΦRF.
The proof is by induction on the depth d of the LLRF . For d = 1 it is clear since
it is an LRF . Now let d > 1, by Lemma 4.3 we can find g that is positive over Q and
decreasing at least on the same transitions as fi . Now hf1 , . . . , fi−1 , fi+1 , fd i is a weak
LLRF of depth d − 1 for Q′ = Q ∩ {x′′ | ∆g(x′′ ) ≤ 0}. By the induction hypothesis we
can construct a weak MΦRF for Q′ of depth d − 1, and then by Lemma 4.2 we can lift
this MΦRF to one of depth d for Q.
EXAMPLE 4.5. Let Q be the transition polyhedron of the loop (3) (on Page 4),
which admits the LLRF h4y, 4x − 4z + 4i, and note that it is not a MΦRF. Following
the proof of above theorem, we can convert it to the MΦRF h4y + x − z, 4x − 4z + 4i.

5

MΦRFs and LLRFs Over the Integers

The procedure described in Section 3 for synthesizing MΦRFs, i.e., use linear programming to synthesize a nested ranking function, is complete for rational loops but not for
integer loops. That is because it might be the case that I(Q) has a MΦRF but Q does
not.
EXAMPLE 5.1. Consider the loop
while (x2 − x1 ≤ 0, x1 + x2 ≥ 1, x3 ≥ 0) do x′2 = x2 − 2x1 + 1; x′3 = x3 + 10x2 + 9
When interpreted over the integers, this loop has the MΦRF h10x2 , x3 i. However, when
interpreted over the rationals, the loop does not even terminate — consider the point
( 21 , 12 , 0).
For LRFs, completeness for the integer case was achieved by reducing the problem
to the rational case, using the integer hull QI [11, 4]. In fact, it is quite easy to see why
this reduction works for LRFs, as the requirements that a LRF has to satisfy are a
conjunction of linear inequalities and if they are satisfied by I(Q), they will be satisfied
by convex combinations of such points, i.e., QI .
Since we have reduced the problem of finding a MΦRF to finding a nested ranking
function, and the requirements from a nested ranking function are conjunctions of linear
inequalities that should be implied by Q, it is tempting to assume that this argument
applies also for MΦRFs. However, to justify the use of nested functions, specifically in
proving Lemma 3.3, we relied on Lemma 2.2, which we applied to Q (it is quite easy
15

to see that the lemma fails if instead of quantifying over a polyhedron, one quantifies
only on its integer points). This means that we did not prove that the existence of a
MΦRF for I(Q) implies the existence of a nested ranking function over I(Q). A similar
observation also holds for the results of Section 4, where we proved that any (weak)
LLRF can be converted to a MΦRF. Those results are valid only for rational loops,
since in the corresponding proofs we used Lemma 2.2.
In this section we show that reduction of the integer case to the rational one, via
the integer hull, does work also for MΦRFs, and for converting LLRFs to MΦRFs, thus
extending the result of sections 3 and 4 to integer loops. We do so by showing that if
I(Q) has a LLRF , then QI has a weak LLRF .
THEOREM 5.2. Let hf1 , f2 , . . . , fd i be a weak LLRF for I(Q). Then there are constants c1 , . . . , cd such that hf1 + c1 , . . . , fd + cd i is a weak LLRF for QI (over the rationals).
Proof. The proof is by induction on d. The base case, d = 1, concerns a LRF , and as
already mentioned, is trivial (and c1 = 0). For d > 1, define:
Q′ = QI ∩ {x′′ ∈ Q2n | f1 (x) ≤ −1},
Q′′ = QI ∩ {x′′ ∈ Q2n | ∆f1 (x′′ ) = 0}

(18)
(19)

Note that Q′ includes only integer points of QI that are not ranked at the first component, due to violating f1 (x) ≥ 0. By changing the first component into f1 + 1, we take
care of points where −1 < f1 (x) < 0. Thus we will have that for every integer point
x′′ ∈ Q, if it is not in Q′ , then the first component is non-negative, and otherwise x′′
is ranked by hf2 , . . . , fd i. Similarly Q′′ includes all the integer points of QI that are
not ranked by the first component due to violating ∆f1 (x′′ ) > 0. Note also that Q′′ is
integral, since it is a face of QI . On the other hand, Q′ is not necessarily integral, so
we have to distinguish Q′I from Q′ . By the induction hypothesis there are
• c′2 , . . . , c′d such that hf2 + c′2 , . . . , fd + c′d i is a weak LLRF for Q′I ; and
• c′′2 , . . . , c′′d such that hf2 + c′′2 , . . . , fd + c′′d i is a weak LLRF for Q′′I .
Next we prove that f1 has a lower bound on QI \ Q′I , i.e., there is a constant c1 ≥ 1
such that f1 + c1 is non-negative on this set. Before proceeding to the proof, note that
this implies that
hf1 + c1 , f2 + max(c′2 , c′′2 ), . . . , fd + max(c′d , c′′d )i

16

is a weak LLRF for QI . To see this, take any rational x′′ ∈ QI , then either x′′ is ranked
by the first component, or x′′ ∈ Q′′ or x′′ ∈ Q′I ; in the last two cases, it is ranked by a
component fi + max(c′i , c′′i ) for i > 1.
It remains to prove that f1 has a lower bound on QI \ Q′I . We assume that Q′I is
non-empty, since otherwise, by the definition of Q′ , it is easy to see that f1 ≥ −1 over
all of QI . Thus, we consider Q′I in an irredundant constraint representation:
Q′I = {x′′ ∈ Q2n | ~ai · x′′ ≤ bi , i = 1, . . . , m},

(20)

and define
Pi = QI ∩ {x′′ ∈ Q2n | ~ai · x′′ > bi }
(21)
′
′′
2n
′′
Pi = QI ∩ {x ∈ Q | ~ai · x ≥ bi }
(22)
S
for i = 1, . . . , m. Then, clearly, QI \ Q′I ⊆ m
i=1 Pi . It suffices to prove that f1 has a
lower bound over Pi , for every i. Fix i for the rest of the argument, such that Pi is not
empty. It is important to note that, by construction, all integer points of Pi are also in
QI \ Q′I .
Let H be the half-space {x′′ | ~ai ·x ≤ bi }. We first claim that Pi = Pi′ \H contains an
integer point. Equivalently, there is an integer point of QI not contained in H. There
has to be such a point, for otherwise, QI , being integral, would be contained in H, and
Pi would be empty. Let x′′0 be such a point.
Next, assume (by way of contradiction) that f1 is not lower bounded on Pi . Express
f1 as f1 (x) = ~λ · x + λ0 , then ~λ · x is not lower bounded on Pi and thus not on Pi′ .
This means that Pi′ is not a polytope, and thus can be expressed as O + C, where O is
a polytope and C is a cone. It is easy to see that there must be a rational y′′ ∈ C such
that ~λ · y < 0, since otherwise f1 would be bounded on Pi′ .
For k ∈ Z+ , consider the point x′′0 + ky′′ . Clearly it is in Pi′ . Since y′′ ∈ C, we have
~ai · y′′ ≥ 0; Since x′′0 ∈ Pi , we have ~ai · x′′0 > bi ; adding up, we get ~ai · (x′′0 + ky′′ ) > bi for
all k. We conclude that the set S = {x′′0 + ky′′ | k ∈ Z+ } is contained in Pi . Clearly, it
includes an infinite number of integer points. Moreover f1 obtains arbitrarily negative
values on S (the larger k, the smaller the value), in particular on its integer points.
Recall that these points are included QI \ Q′I , thus f1 is not lower bounded on the
integer points of QI \ Q′I , a contradiction to the way Q′I was defined.
Corollary 5.3. If I(Q) has a weak LLRF of depth d, then QI has a MΦRF, of depth
at most d.
Proof. By Theorem 5.2 we know that QI has a weak LLRF (of the same depth), which
in turn can be converted to a MΦRF by Theorem 4.4.
17

Since MΦRFs are also weak LLRF , we get
Corollary 5.4. If I(Q) has a MΦRF of depth d, then QI has a MΦRF of depth at
most d.
The above corollary provides a complete procedure for synthesizing MΦRFs over
the integers, simply by seeking a nested ranking function for QI .
EXAMPLE 5.5. For the loop of Example 5.1, computation of the integer hull results
in the addition of the constraint x1 ≥ 1. Now seeking a MΦRF as in Section 3 we
find, for example, h10x2 + 10, x3 i. Note that h10x2 , x3 i, which a MΦRF for I(Q), is
not a MΦRF for QI according to Definition 2.1, e.g., for any 0 < ε < 1 the transition
(1 + ε, −ε, 0, 1, −3ε − 1, −10ε + 9) ∈ QI is not ranked, since 10x2 < 0 and x3 − x′3 =
10ε − 9 < 1.
The procedure described above has exponential-time complexity, because computing
the integer hull requires exponential time. However, it is polynomial for the cases in
which the integer hull can be computed in polynomial time [4, Sect. 4]. The next
theorem shows that the exponential time complexity is unavoidable for the general case
(unless P = NP).
THEOREM 5.6. BMΦRF (Z) is coNP-complete.
The proof repeats the arguments in the coNP-completes proof for linear ranking
functions [4, Sect. 3]. We omit the details.

6

The Depth of a MΦRF

A wishful thought: If we could pre-compute an upper bound on the depth of optimal MΦRFs, and use it to bound the recursion, we would obtain a complete decision
procedure for MΦRFs in general, since we can seek a MΦRF, as in Section 3, of this
specific depth. This thought is motivated by results for lexicographic ranking functions,
for example, [4] shows that the number of components in such functions is bounded
by the number of variables in the loop. For MΦRFs, we were not able to find a similar upper bound, and we can show that the problem is more complicated than in the
lexicographic case as a bound, if one exists, must depend not only on the number of
variables or constraints, but also on the values of the coefficients in the loop constraints.
THEOREM 6.1. For integer B > 0, the following loop QB
while (x ≥ 1, y ≥ 1, x ≥ y, 2B y ≥ x) do x′ = 2x, y ′ = 3y
needs at least B + 1 components in any MΦRF.
18

Proof. Define Ri = {(2i c, c, 2i+1 c, 3c) | c ≥ 1} and note that for i = 0 . . . B, we have
Ri ⊂ QB . Moreover, Ri 6= Rj for different i and j. Next we prove that in any MΦRF
hf1 , . . . , fd i for QB , and Ri with i = 0 . . . B, there must be a component fk such that
x′′ ∈ Ri → fk (x) − f (0, 0) ≥ 0 ∧ ∆fk (x′′ ) > 0. To prove this, fix i. We argue by the
pigeonhole principle that, for some k, fk (2i c, c) = cfk (2i , 1) + (1 − c)fk (0, 0) ≥ 0 and
fk (2i c, c) − fk (2i+1 c, 3c) = c(fk (2i , 1) − fk (2i+1 , 3)) > 0 for infinite number of values of
c, and thus fk (2i , 1) − fk (0, 0) ≥ 0, and fk (2i , 1) − fk (2i+1 , 3) > 0, leading to the above
statement. We say that Ri is “ranked” by fk .
If d < B + 1, then, by the pigeonhole principle, there are different Ri and Rj that
are “ranked” by the same fk . We show that this leads to a contradiction. Consider Ri
and Rj , with j > i, and assume that they are “ranked” by fk (x, y) = a1 x + a2 y + a0 .
Applying the conclusion of the last paragraph to Ri and Rj , we have:
fk (2i , 1) − fk (2i+1 , 3) = −a1 2i − a2 2 > 0
j

fk (2 , 1) − fk (2

j+1

j

, 3) = −a1 2 − a2 2 > 0

fk (2i , 1) − fk (0, 0) = a1 2i + a2
j

j

fk (2 , 1) − fk (0, 0) = a1 2 + a2

(23)
(24)

≥0

(25)

≥0

(26)

Adding 12 ·(24) to (26) we get a1 2j−1 > 0. Thus, a1 must be positive. From the sum
of 12 ·(24) and (25), we get a1 (2i − 2j−1 ) > 0, which implies j > i + 1, and a1 < 0, a
contradiction. We conclude that d must be at least B + 1.
The bound B + 1 in the above theorem is tight. This is confirmed by the MΦRF
hx − 2B y, x − 2B−1 y, x − 2B−2 y, . . . , x − yi.

7

Iteration Bounds from MΦRFs

Automatic complexity analysis techniques are often based on bounding the number
of iterations of loops, using ranking functions. Thus, it is natural to ask if a MΦRF
implies a bound on the number of iterations of a given SLC loop. For LRFs, the implied
bound is trivially linear, and in the case of SLC loops, it is known to be linear also for
a class of lexicographic ranking functions [4]. In this section we show that MΦRFs, too,
imply a linear iteration bound, despite the fact that the variables involved may grow
non-linearly during the loop.
EXAMPLE 7.1. Consider the following loop
while (x ≥ 0) do x′ = x + y, y ′ = y − 1
19

with the corresponding MΦRF hy + 1, xi. Let us consider an execution starting from
positive values x0 and y0 . It is easy to see that when y + 1 reaches 0, i.e., when moving
from that first phase to the second phase, the value of x would be x0 + y0 + (y0 − 1) +
. . . + 1 + 0 − 1 = x0 + y0 (y20 +1) − 1, which is polynomial in the input. It may seem that
the next phase would be super-linear, since the second phase is ranked by x, however,
note that x decreases first by 1, then by 2, then by 3, and so on. This means that the
quantity y0 (y20 +1) is eliminated in y0 iterations, and then in at most x0 − 1 iteration the
remaining value x0 − 1 is eliminated as well. Thus, the total runtime is linear.
In what follows we generalize the observation of the above example. We consider
an SLC loop Q, and a corresponding irredundant MΦRF τ = hf1 , . . . , fd i. Let us start
with an outline of the proof. We first define a function Fk (t) that corresponds to the
value of fk after iteration t. We then bound each Fk by some expression UBk (t), and
observe that for t greater than some number Tk , that depends linearly on the input,
UBk (Tk ) becomes negative. This means that Tk is an upper bound on the time in which
the k-th phase ends; the whole loop must terminate before maxk Tk iterations.
Let xt be the state after iteration t, and define Fk (t) = fk (xt ), i.e., the value
of the k-th component fk after t iterations. For the initial state x0 , we let M =
max(f1 (x0 ), . . . , fd (x0 ), 1). Note that M is linear in kx0 k∞ (i.e., in the maximum
absolute value of the components of x0 ). We first state an auxiliary lemma and then a
lemma that bounds Fk .
LEMMA 7.2. For all 1 < k ≤ d, there are µ1 , . . . , µk−2 ≥ 0 and µk−1 > 0 such that
x′′ ∈ Q → µ1 f1 (x) + · · · + µk−1fk−1 (x) + (∆fk (x′′ ) − 1) ≥ 0.
Proof. From the definition of MΦRF we have
x′′ ∈ Q → f1 (x) ≥ 0 ∨ · · · ∨ fk−1(x) ≥ 0 ∨ ∆fk (x′′ ) ≥ 1.
Moreover the conditions of Lemma 2.3 hold since fk is not redundant, thus there are
non-negative constants µ1 , . . . , µk−1 such that
x′′ ∈ Q → µ1 f1 (x) + · · · + µk−1 fk−1 (x) + (∆fk (x′′ ) − 1) ≥ 0.
Moreover, at least µk−1 must be non-zero, otherwise it means that ∆fk (x′′ ) ≥ 1 holds
already when f1 , . . . , fk−2 are negative, so fk−1 would be redundant.
It is not hard to see that the coefficients described in the above lemma can be
computed explicitly, if desired. Similarly, the constants in the next lemma, and consequently the linear iteration bound we claim, can be computed explicitly, in polynomial
time.
20

LEMMA 7.3. For all 1 ≤ k ≤ d, there are constants ck , dk > 0 such that Fk (t) ≤
ck Mtk−1 − dk tk , for all t ≥ 1.
Proof. The proof is by induction. For the base case, k = 1, we take c1 = d1 = 1 and
get F1 (t) ≤ M − t, which is trivially true. For k ≥ 2 we assume that the lemma holds
for smaller indexes and show that it holds for k. First note that the change in the value
of Fk (t) in the i-th iteration is fk (xi+1 ) − fk (xi ) = −∆fk (x′′i ). By Lemma 7.2 and the
definition of Fk , we have µ1 , . . . , µk−2 ≥ 0 and µk−1 > 0 such that (over Q)
fk (xi+1 ) − fk (xi ) < µ1 F1 (i) + · · · + µk−1Fk−1 (i) .

(27)

Now we bound Fk (explanation follows):
Fk (t) = fk (x0 ) + Σt−1
i=0 (fk (xi+1 ) − fk (xi ))
t−1
< M + Σi=0 (µ1 F1 (i) + · · · + µk−1 Fk−1 (i))
≤ M(1 + µ) + Σt−1
i=1 (µ1 F1 (i) + · · · + µk−1 Fk−1 (i))

k−1
j−1
≤ M(1 + µ) + Σt−1
− µj dj ij
i=1 Σj=1 µj cj Mi
≤ M(1 + µ) + Σt−1
i=1


k−1
(Σj=1
µj cj Mij−1 ) − µk−1 dk−1ik−1

k−1
M(Σj=1
µj cj )ik−2 − µk−1 dk−1ik−1

≤ M(1 + µ) +

Σt−1
i=1

= M(1 + µ) +

k−1
k−2
k−1
M(Σj=1
µj cj )(Σt−1
) − µk−1 dk−1Σt−1
i=1 i
i=1 i
tk
tk−1
k−1
) − µk−1 dk−1( − tk−1 )
M(Σj=1
µj cj )(

≤ M(1 + µ) +

k−1

= ck Mtk−1 − dk tk

k

(28)
(29)
(30)
(31)
(32)
(33)
(34)
(35)
(36)

Each step above is obtained from the previous one as follows: (29) by replacing fk (x0 )
by M, since fk (x0 ) ≤ M, and applying (27); (30) by separating
Pk−1 the term for i = 0
from the sum; this term is bounded by µM, where µ =
j=1 µj , because Fk (0) =
fk (x0 ) ≤ M by definition; (31) by applying the induction hypothesis; (32) by removing
all negative values −µj dj ij , except the last one −µk−1 dk−1ik−1 ; (33) by replacing ij−1
k−2
by an upper bound ik−2 ; (34) by opening parentheses; (35) replacing Σt−1
by an
i=1 i
k−1
k
t−1 k−1
t
t
k−1
upper bound k−1 , and Σi=1 i
by a lower bound k − t ; finally for (35), take
k−1
ck = (1 + µ) + (Σj=1 µj cj )/(k − 1) + µk−1dk−1 , and dk = µk−1 dk−1/k and note that both
are positive.
THEOREM 7.4. An SLC loop that has a MΦRF terminates in a number of iterations
bounded by O(kx0k∞ ).
Proof. Observe that for t > max{1, (ck /dk )M}, we have Fk (t) < 0, proving that the
k-th phase terminates by this time (since it remains negative after that time). Thus,
21

by the time max{1, (c1 /d1 )M, . . . , (ck /dk )M}, which is linear in kx0 k∞ since M is, all
phases must have terminated.
Note that the constants ck and dk above can be computed explicitly, if desired.
EXAMPLE 7.5. Consider the loop of Example 7.1, the corresponding MΦRF hy +
1, xi, initial positive input y0 ≥ x0 ≥ 1, and let M = max(x0 , y0 + 1) = y0 + 1. By
definition F1 (t) ≤ M − t. Let us bound F2 . First we find a bound on −∆f2 (x′′ ).
Starting from
(x, x′ , y, y ′) ∈ Q → y + 1 ≥ 0 ∨ (x − x′ ) ≥ 1
we find µ1 > 0 such that
(x, x′ , y, y ′) ∈ Q → µ1 (y + 1) + (x − x′ ) − 1 ≥ 0
which holds for µ1 = 1 (substitution x′ = x + y and µ1 = 1 we get 0 ≥ 0). Thus
−∆f2 (x′′ ) = x′ − x ≤ y (which is easy to see in this case since the update is a deterministic). Now F2 (t) ≤ c2 Mt − d2 t2 where c2 = (1 + µ) + (µ1 c1 ) + µ1 d1 = 4, and
dk = µ1 d1 /2 = 21 . Thus F2 (t) < 4Mt − 21 t2 . For t > max{1, M, 8M} we get both F1 (t)
and F2 (t) negative, which means that 8M = 8y0 + 8 is a bound for the runtime for this
input.
We remark that the above result also holds for multi-path loops if they have a nested
ranking function, but does not hold for any MΦRF.

8

Conclusion

Linear ranking functions, lexicographic and multiphase combinations of linear ranking
functions, have all been proposed in earlier work. The original purpose of this work has
been to improve our understanding of multiphase functions, and answer open problems
regarding the complexity of obtaining such functions from linear-constraint loops, the
difference between the integer case and the rational case, and the possibility of inferring
an iteration bound from such ranking functions. Similarly, we wanted to understand a
natural class of lexicographic ranking functions, which removes a restriction of previous
definitions regarding negative values. Surprisingly, it turned out that our main results
are equivalences which show that, for single-path linear-constraint loops, both MΦRFs
and LLRFs reduce to a simple kind of MΦRF, that has been known to allow polynomialtime solution (over the rationals). Thus, our result collapsed, in essence, the above
classes of ranking functions.

22

The implication of having a polynomial-time solution, which is hardly more complex
than the standard algorithm to find linear ranking functions, is that whenever one
considers using LRFs in one’s work, one should consider using MΦRFs. By controlling
the depth of the MΦRFs one trades expressivity for processing cost. We believe that
it would be sensible to start with depth 1 (i.e., seeking a LRF ) and increase the depth
upon failure. Similarly, since a complete solution for the integers is inherently more
costly (as we proved it to be coNP-complete), it makes sense to begin with the solution
that is complete over the rationals, since it is, at any rate, safe for the integer case. If
this does not work, one can also consider special cases in which the inherent hardness
can be avoided, as discussed in detail in [4, Sect. 4].
Theoretically, some tantalizing open problems remain. Is it possible to decide
whether a given loop admits a MΦRF, without a depth bound? This is related to the
question, discussed in Section 6, whether it is possible to precompute a depth bound.
What is the complexity of the MΦRF problems over multi-path loops? For such loops,
the equivalence MΦRFs, nested r.f.s and LLRFs does not hold. Finally (generalizing
the first question), we think that there is need for further exploration of single-path
loops and of the plethora of “termination witnesses” based on linear functions (a notable
reference is [18]).
We have implemented the nested ranking function procedure of Section 3, and applied it, among others, on a set of terminating and non-terminating SLC loops taken
from [14]. These examples originate mainly from [7], and they were collected as ones
that require the transition invariants techniques [23] for proving termination. For all 25
terminating loops in this set we found a MΦRF (2 have also a LLRF as defined in [4] and
6 have LRF ). The implementation can be tried at http://loopkiller.com/irankfinder,
where this set of examples is available as well.
Closely related work is already discussed in Section 1, for more details on algorithmic
and complexity aspect of linear ranking of SLC loops, we refer the reader to [4].

References
[1] Elvira Albert, Puri Arenas, Samir Genaim, and Germán Puebla. Closed-form
upper bounds in static cost analysis. J. Autom. Reasoning, 46(2):161–203, 2011.
[2] Christophe Alias, Alain Darte, Paul Feautrier, and Laure Gonnord. Multidimensional rankings, program termination, and complexity bounds of flowchart
programs. In Radhia Cousot and Matthieu Martel, editors, Static Analysis Symposium, SAS’10, volume 6337 of LNCS, pages 117–133. Springer, 2010.

23

[3] Roberto Bagnara and Fred Mesnard. Eventual linear ranking functions. In Proceedings of the 15th International Symposium on Principles and Practice of Declarative
Programming, PPDP 2013, pages 229–238. ACM Press, 2013.
[4] Amir M. Ben-Amram and Samir Genaim. Ranking functions for linear-constraint
loops. Journal of the ACM, 61(4):26:1–26:55, jul 2014.
[5] Aaron R. Bradley, Zohar Manna, and Henny B. Sipma. Linear ranking with reachability. In Kousha Etessami and Sriram K. Rajamani, editors, Computer Aided
Verification, CAV’05, volume 3576 of LNCS, pages 491–504. Springer, 2005.
[6] Marc Brockschmidt, Fabian Emmes, Stephan Falke, Carsten Fuhs, and Jürgen
Giesl. Analyzing runtime and size complexity of integer programs. ACM Trans.
Program. Lang. Syst., 38(4):13, 2016.
[7] Hong Yi Chen, Shaked Flur, and Supratik Mukhopadhyay. Termination proofs for
linear simple loops. STTT, 17(1):47–57, 2015.
[8] Michael Colón and Henny Sipma. Synthesis of linear ranking functions. In Tiziana
Margaria and Wang Yi, editors, Tools and Algorithms for the Construction and
Analysis of Systems, TACAS’01, volume 2031 of LNCS, pages 67–81. Springer,
2001.
[9] Byron Cook, Alexey Gotsman, Andreas Podelski, Andrey Rybalchenko, and
Moshe Y. Vardi. Proving that programs eventually do something good. In Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2007, Nice, France, January 17-19, 2007, pages 265–276,
2007.
[10] Byron Cook, Sumit Gulwani, Tal Lev-Ami, Andrey Rybalchenko, and Mooly Sagiv.
Proving conditional termination. In Computer Aided Verification, CAV’08, volume
5123 of Lecture Notes in Computer Science, pages 328–340. Springer, 2008.
[11] Byron Cook, Daniel Kroening, Philipp Rümmer, and Christoph M. Wintersteiger.
Ranking function synthesis for bit-vector relations. Formal Methods in System
Design, 43(1):93–120, 2013.
[12] Byron Cook, Andreas Podelski, and Andrey Rybalchenko. Termination proofs for
systems code. In Michael I. Schwartzbach and Thomas Ball, editors, Programming
Language Design and Implementation, PLDI’06, pages 415–426. ACM, 2006.

24

[13] Paul Feautrier. Some efficient solutions to the affine scheduling problem. I. Onedimensional time. International Journal of Parallel Programming, 21(5):313–347,
1992.
[14] Pierre Ganty and Samir Genaim. Proving Termination Starting from the End. In
Natasha Sharygina and Helmut Veith, editors, Proceedings of the 25th International
Conference on Computer Aided Verification, CAV 2013, volume 8044 of Lecture
Notes in Computer Science, pages 397–412. Springer, 2013.
[15] Michael Harrison. Lectures on Sequential Machines. Academic Press, 1969.
[16] Matthias Heizmann, Jochen Hoenicke, Jan Leike, and Andreas Podelski. Linear
ranking for linear lasso programs. In Dang Hung and Mizuhito Ogawa, editors,
Automated Technology for Verification and Analysis, volume 8172 of Lecture Notes
in Computer Science, pages 365–380. Springer International Publishing, 2013.
[17] Daniel Larraz, Albert Oliveras, Enric Rodrı́guez-Carbonell, and Albert Rubio.
Proving termination of imperative programs using Max-SMT. In Formal Methods
in Computer-Aided Design, FMCAD 2013, pages 218–225. IEEE, 2013.
[18] Jan Leike and Matthias Heizmann. Ranking templates for linear loops. Logical
Methods in Computer Science, 11(1):1–27, 2015.
[19] Jérôme Leroux and Grégoire Sutre. Flat counter automata almost everywhere! In
International Symposium on Automated Technology for Verification and Analysis
(ATVA 2005), volume 3707 of Lecture Notes in Computer Science, pages 489–503.
Springer, 2005.
[20] Yi Li, Guang Zhu, and Yong Feng. The L-depth eventual linear ranking functions
for single-path linear constraint loops. In 10th International Symposium on Theoretical Aspects of Software Engineering (TASE 2016), pages 30–37. IEEE, 2016.
[21] Joël Ouaknine and James Worrell. On linear recurrence sequences and loop termination. ACM SIGLOG News, 2(2):4–13, April 2015.
[22] Andreas Podelski and Andrey Rybalchenko. A complete method for the synthesis
of linear ranking functions. In Bernhard Steffen and Giorgio Levi, editors, Verification, Model Checking, and Abstract Interpretation, VMCAI’04, volume 2937 of
LNCS, pages 239–251. Springer, 2004.

25

[23] Andreas Podelski and Andrey Rybalchenko. Transition invariants. In 19th IEEE
Symposium on Logic in Computer Science, LICS 2004, pages 32–41. IEEE Computer Society, 2004.
[24] Alexander Schrijver. Theory of Linear and Integer Programming. John Wiley and
Sons, New York, 1986.
[25] Kirack Sohn and Allen Van Gelder. Termination detection in logic programs using
argument sizes. In Daniel J. Rosenkrantz, editor, Symposium on Principles of
Database Systems, pages 216–226. ACM Press, 1991.

26

