Linear Ranking for Linear Lasso Programs

The general setting of this work is the constraint-based synthesis of termination arguments. We consider a restricted class of programs called lasso programs. The termination argument for a lasso program is a pair of a ranking function and an invariant. We present the---to the best of our knowledge---first method to synthesize termination arguments for lasso programs that uses linear arithmetic. We prove a completeness theorem. The completeness theorem establishes that, even though we use only linear (as opposed to non-linear) constraint solving, we are able to compute termination arguments in several interesting cases. The key to our method lies in a constraint transformation that replaces a disjunction by a sum.


Introduction
Termination is arguably the single most interesting correctness property of a program. Research on proving termination can be divided according to three (interrelated) topics, namely: practical tools [1,9,13,17,18,19,21,22], decidability questions [4,8,25], and constraint-based synthesis of termination arguments [2,3,5,6,7,10,12,14,20,23]. The work in this paper falls under the research on the third topic. The general goal of this research is to investigate how one can derive a constraint from the program text and compute a termination argument (of a restricted form) through the solution of the constraint, i.e., via constraint solving.
In this paper, we present a method for the synthesis of termination arguments for a specific class of programs that we call lasso programs. As the name indicates, the control flow graph of a lasso program is of a restricted shape: a stem followed by a loop.
Lasso programs do not appear as stand-alone programs. Lasso programs appear in practice whenever one needs a finite representation of an infinite path in a control flow graph, for example in (potentially spurious) counterexamples in a termination analysis [13,17,18,19], non-termination analysis [16], stability analysis [11,22], or cost analysis [1,15]. Importantly, the termination argument for a lasso program is a pair of a ranking function and an invariant (the rank must decrease only for states that satisfy the invariant). Figure 1 shows an example of a lasso program.
The class of lasso programs lies between two classes of programs for which constraint-based methods have been studied extensively. For the first, more specialized class, methods can be based on linear arithmetic constraint solving [2,3,10,12,20]. For the second, more general class, all known methods are based on non-linear arithmetic constraint solving [5,7]. The contribution of our method can be phrased, alternatively, as the generalization of the applicability of the 'linear methods', or as the optimization of the 'non-linear method' to a 'linear method' for a subproblem. The step from 'non-linear' to 'linear' is interesting for principled reasons (non-linear arithmetic constraint solving is undecidable in the case of integers). As we will show the step is also practically interesting.
The reader may wonder how practical tools presently handle the situation where one needs to compute termination arguments for lasso programs. One possibility is to resort to heuristics. For example, instead of computing a termination argument for the lasso program in Figure 1, one would compute the ranking function f (x) = x for the program while(x>=0){x:=x-23;}.
The key to our method is a constraint transformation that replaces a disjunction by a sum. We apply the 'or-to-plus' transformation in the context of Farkas' Lemma. Following [2,5,10,12,20], we apply Farkas' Lemma in order to eliminate the universal quantifiers in the arithmetic constraint whose solution is the termination argument. If we apply Farkas' Lemma to the constraint after the 'or-to-plus' transformation, we obtain a linear arithmetic constraint.
The effect of the 'or-to-plus' transformation to the constraint is a restriction of its solution space. The restriction seems strong; i.e., in some cases, the solution space becomes empty. We can characterize those cases. In other words, we can characterize when the 'or-to-plus' transformation leads to the loss of an termination argument, and when it does not. The characterization is formulated as a completeness theorem for which we will present the proof. This characterization allows us to establish that, even though we use only linear (as opposed to non-linear) constraint solving, we are able to compute termination arguments in several interesting cases. A possible explanation for this (perhaps initially surprising) fact is that, for synthesis, we are interested in the mere existence of a solution, and the loss of many solutions does not necessarily mean the loss of all solutions of the constraint.
We have implemented our method and we have used our implementation to illustrate the applicability and the efficiency of our method. Our implementation is available through a web interface, together with a number of example programs (including the ones used in this paper). 1 1: y := 23; 2: while( x >= 0 ) { 3: x := x -y; 4: y := y + 1; 5: } 1 2 τstem : y ′ = 23 τ loop : Example of a lasso program and its formal representation P yPositive = (τstem, τ loop ). The ranking function defined by f (x, y) = x decreases in transitions from states that satisfy the invariant y ≥ 1 (the ranking function does not decrease when y ≤ 0).

Preliminaries: Linear Arithmetic
We use x to denote the vector with entries x 1 , . . . , x n , and x ⊺ to denote the transposed vector of x. As usual, the expression A·x ≤ b denotes the conjunction of linear constraints We call a relation τ (x, x ′ ) a linear relation if τ is defined by a conjunction of linear constraints over the variables x and x ′ , i.e., if there is a matrix A with m rows and 2n columns and a vector b of size m such that the following equation holds. τ is defined by an affine linear term, i.e., there is a vector r ⊺ and a number r 0 such that the following equation holds.
We call a predicate I(x) a linear predicate, if I(x) is defined by a linear inequality, i.e., there is a vector s ⊺ and a number s 0 such that following equivalence holds.
Farkas' Lemma. We use the affine version of Farkas' Lemma [24] which is also used in [2,5,12,23,20] and states the following. Given a satisfiable conjunction of linear constraints A · x ≤ b and a linear constraint c ⊺ · x ≤ δ, the following equivalence holds.

Lasso Program
To abstract away from program syntax, we define a lasso program directly by the two relations that generate its execution sequences.
Definition 1 (Lasso Program). Given a set of states Σ, a lasso program is given by the two relations τ stem ⊆ Σ × Σ and τ loop ⊆ Σ × Σ. We call τ stem the stem of P and τ loop the loop of P . An execution of the lasso program P is a possibly infinite sequence of states σ 0 , σ 1 , . . . such that the pair of the first two states is an element of the stem, i.e., (σ 0 , σ 1 ) ∈ τ stem and each other consecutive pair of states is an element of the loop, i.e., We call the lasso program P terminating if P has no infinite execution.
We use constraints over primed and unprimed variables to denote a transition relation (see Figure 1). In order to avoid cumbersome technicalities, we consider only lasso programs that have an execution that contains at least three states. This means we consider only programs where the relational composition of τ stem and τ loop is non-empty, i.e., τ stem • τ loop = ∅.
Since Turing, a termination argument is based on an ordering which does not allow infinite decreasing chains (such as ordering on the natural numbers). Here, we use the ordering over the set of positive reals which is defined by some value δ > 0, namely Ranking Function. We call a function f from the states of the lasso program P into the reals R a ranking function for P if there is a positive number δ > 0 such that for each consecutive pair of states (x i , x i+1 ) of a loop transition (i ≥ 1) in every execution of P the value of f is decreasing by at least δ, i.e., and the value of f is non-negative, i.e., If there is a ranking function for the lasso program P , then P is terminating.
Inductive Invariant. We call a state predicate I(x) an inductive invariant of the lasso program P if the predicate holds after executing the stem, i.e., and if the predicate holds before executing the loop, then the predicate holds afterwards, i.e., Ranking Function with Supporting Invariant. We call a pair of a ranking function f (x) and an inductive invariant I(x) of the lasso program P a ranking function with supporting invariant if the following holds.
-There exists a positive real number δ > 0 such that, if the inductive invariant holds then an execution of the loop decreases the value of the ranking function by at least δ, i.e., -In states in which the inductive invariant holds and the loop can be executed, the value of the ranking function is non-negative, i.e., For example, the lasso program depicted in Figure 1 has the ranking function f (x, y) = x with supporting invariant y ≥ 1.
Linear lasso programs. Linear lasso programs. For the remainder of this paper we consider only linear lasso programs, linear ranking functions, and linear inductive invariants which we will define next. The variables of the programs will range over the reals until we come to Section 9 where we turn to programs over integers.

Definition 2 (Linear Lasso Program). A linear lasso program
is a lasso program whose states are vectors over the reals, i.e. Σ = R n , and whose relations τ stem and τ loop are linear relations.

We use the expression
Linear Ranking Function. If a ranking function f : R n → R is an (affine) linear function, we call f a linear ranking function. We use r 1 , . . . , r n as coefficients of a linear ranking function, r as their vector, Linear Invariant. If an inductive invariant I(x) is a linear predicate, we call I a linear inductive invariant. We use s 1 , . . . , s n as coefficients of the term that defines the linear predicate, s as their vector,

The Or-to-Plus Method
Our constraint-based method for the synthesis of linear ranking functions for linear lasso programs consists of three main steps: Step 1. Set up four (universally quantified) constraints whose free variables are the coefficients of a linear ranking function with linear supporting invariant.
Step 2. Apply Farkas' Lemma to the four constraints to obtain equivalent constraints without universal quantification.
Step 3. Obtain solutions for the free variables by linear constraint solving.
The particularity of our four constraints in Step 1 is that the application of Farkas' Lemma in Step 2 yields constraints that are linear.
Instead of presenting our constraints immediately, we derive them in three successive transformations of constraints. We start with the four constraints (ϕ invStem ), (ϕ invLoop ), (ϕ rkDecr ), and (ϕ rkBound ). Below, we have rephrased the four constraints for the setting where the ranking function is linear and the supporting invariant is linear. We marked them (ϕ BMS 1 ), (ϕ BMS 2 ), (ϕ BMS 3 ), and (ϕ BMS 4 ) in reference to Bradley, Manna and Sipma [5] who were the first to use them in the corresponding step of their method.

The Bradley-Manna-Sipma constraints
for the special case of lasso programs and one linear supporting invariant 2 The free variables of ϕ BMS are r, r 0 , s, and s 0 .
Transformation 1: Move supporting invariant to right-hand side. We bring the conjunct s ⊺ · x + s 0 ≥ 0 in three of the four constraints (ϕ BMS 1 ), (ϕ BMS 2 ), (ϕ BMS 3 ), and (ϕ BMS 4 ) to the right-hand side of the implication, according to the following scheme.
We obtain the following constraints.
Transformation 2: Drop supporting invariant in fourth constraint. We strengthen the fourth constraint (ψ 4 ) by removing the disjunct −s ⊺ · x − s 0 > 0. A solution for the strengthened constraint defines a ranking function whose value is bounded from below for all states (and not just those that satisfy the supporting invariant).
Transformation 3: Replace disjunction by sum. We replace the disjunction on the right-hand side of the implication in constraints (ψ 2 ) and (ψ 3 ) by a single inequality, according to the scheme below. (It is the disjunction which prevents us from applying Farkas' Lemma to the constraints (ψ 2 ) and (ψ 3 ).) In the second constraint (ψ 2 ), we replace the disjunction In the third constraint (ψ 3 ), we replace the disjunction We obtain the following four constraints.
Since we consider linear lasso programs, the relations τ stem and τ loop are given as conjunctions of linear constraints.
We have now finished the description for the three transformation steps that lead us to the the or-to-plus constraints. We are now ready to introduce our method.
The Or-to-Plus Method Input: linear lasso program P . Output: coefficients r, r 0 , s, and s 0 of a linear ranking function with linear supporting invariant 1. Set up the or-to-Plus constraints ϕ 1 , ϕ 2 , ϕ 3 , and ϕ 4 for P .
After setting up the four or-to-plus constraints ϕ 1 , ϕ 2 , ϕ 3 , ϕ 4 in Step 1, we apply Farkas' Lemma to each of the four constraints in Step 2. We obtain four linear constraints. E.g., by applying Farkas' Lemma to the constraint (ϕ 3 ) we obtain the following linear constraint.
We apply linear constraint solving in Step 3. We obtain a satisfying assignment for the free variables in the resulting constraints. The values obtained for r, r 0 , s and s 0 are the coefficients of a linear ranking function f (x) with linear supporting invariant I(x).
The or-to-plus method inherits its soundness from method of Bradley-Manna-Sipma.
Step 1 is an equivalence transformation on the Bradley-Manna-Sipma constraints, Step 2 and Step 3 strengthen the constraints, and the application of Farkas' Lemma is an equivalence transformation. Thus, a satisfying assignment of the or-to-plus constraints obtained after the application of Farkas' Lemma is also a satisfying assignment of the Bradley-Manna-Sipma constraints.

Completeness of the Or-to-Plus Method
In the tradition of constraint-based synthesis for verification, we will formulate completeness according to the following scheme: the method X applied to a program P in the class Y computes (the coefficients of) a correctness argument of the form Z whenever one exists (i.e., whenever a correctness argument of the form Z exists for the program P ). Here, X is the or-to-plus method, Y is the class of lasso programs, and Z is a termination argument consisting of a linear ranking function and an invariant of a form that we we define next.

Definition 3 (Non-decreasing linear inductive invariant). We call a linear inductive invariant s
⊺ · x + s 0 ≥ 0 of the lasso program P non-decreasing if the loop implies that the value of the term s ⊺ · x + s 0 does not decrease when executing the loop, i.e., In Section 6 we give examples which may help to convey some intuition about the meaning of 'non-decreasing', examples of those terminating programs that do have a linear ranking function with a non-decreasing linear supporting invariant, and examples of those that don't.
Theorem 1 (Completeness). The or-to-plus method applied to the linear lasso program P succeeds and computes the coefficients of a linear ranking function with non-decreasing linear supporting invariant whenever one exists.
To prove this theorem we use the following lemma.
then there exists a constant µ ≥ 0 such that Proof (of Lemma 1).
defined by a weighted sum is a rotation of H around the intersection Z of the boundary of H and the boundary of H ′ . If a polyhedron X is contained in the union H ∪ H ′ , then there is a half-space Hµ defined by a weighted sum that contains X. By assumption, (1) does not imply (3), so A·x ≤ b ∧ h ⊺ ·x+h 0 ≤ 0 is satisfiable, and by Farkas' Lemma this formula is equivalent to and thus Because A · x ≤ b is satisfiable by assumption, Farkas' Lemma can be applied again to yield Theorem 1). Let f (x) =r ⊺ · x +r 0 be a ranking function with nondecreasing supporting invariant I(x) ≡s ⊺ · x +s 0 ≥ 0 for the lasso program P . Since executions of our lasso programs comprise at least three states, there can be no supporting invariant that contradicts the loop, i.e.
is not valid. From (ϕ rkBound ) it follows that and hence the implication is valid. By (1) and Lemma 1 there is a µ 1 ≥ 0 such that is valid. If we assign r →r − µ 1 ·s, r 0 →r 0 − µ 1 ·s 0 , then (ϕ 4 ) is satisfied.
Because I(x) ≡s · x +s 0 ≥ 0 is a non-decreasing invariant, and hence, since µ 1 ≥ 0, From (ϕ rkDecr ) we know that and hence equivalently With (2) we obtain validity of the following formula.
By (1) and Lemma 1 there exists a µ 2 ≥ 0 such that We pick the assignment r →r − µ 1 ·s, r 0 →r 0 − µ 1 ·s 0 , s → µ 2 ·s, s 0 → µ 2 ·s 0 , which hence satisfies (ϕ 3 ). We already argued that it satisfies (ϕ 4 ), and from µ 2 ≥ 0 and the fact that I(x) is a non-decreasing inductive invariant it follows that the assignment also satisfies (ϕ 1 ) and (ϕ 2 ). Hence, the ranking function (r − µ 1 ·s) ⊺ · x +r 0 − µ 1 ·s 0 with supporting invariant (µ 2 ·s) ⊺ · x + µ 2 ·s 0 ≥ 0 can be found by the or-to-plus method. Our three transformations strengthened the Bradley-Manna-Sipma constraints, hence the solution space of the or-to-plus constraints is smaller than the solution space of the Bradley-Manna-Sipma constraints. This can be seen e.g., in the example depicted in Figure 4. The program P bound has the linear ranking function f (x, y) = x with linear supporting invariant y ≥ 23, but the coefficients of this ranking function and supporting invariant are no solution of the or-to-plus constraints; the constraint ϕ 4 is violated. Does this mean that our method will not succeed? No, it does not. By Theorem 1, in fact, we do know that the method will succeed. I.e., since we know of some linear ranking function with non-decreasing supporting invariant (in this case, f (x, y) = x and y ≥ 23), even if it is not a solution, we know that there exists one which is a solution (here, for example, f (x, y) = x − y with the (trivial) supporting invariant 0 ≥ 0). The prerequisite of Theorem 1 is the existence of a non-decreasing supporting invariant. There are linear lasso programs that have a linear ranking function with linear supporting invariant, but do not have a linear ranking function with a non-decreasing linear supporting invariant. E.g., for the lasso programs depicted in Figure 5 and Figure 6 our or-to-plus method is not able to synthesize a ranking function for these programs.
The linear lasso program P zeno depicted in Figure 5 has the linear ranking function f (x, y) = x with the linear supporting invariant y ≥ 1. However this inductive invariant is not non-decreasing; while executing the loop the value of the variable y converges to 1 in the following sequence. The statement havoc y; in the lasso program P wild is a nondeterministic assignment to the variable y. The relations τ stem and τ loop of this lasso program are given by the constraints y ′ ≥ 1 and x ≥ 0 ∧ x ′ = x − y ∧ y ′ ≥ 1. P wild has the ranking function f (x, y) = x with the supporting invariant y ≥ 1, however this inductive invariant is not non-decreasing in each execution of the loop the variable y can get any value greater than or equal to one.
The next example shows that nondeterministic updates are no general obstacle for our or-to-plus method. In the linear lasso program P array the loop iterates over an array of positive integers. The index accessed in the next

Lasso Programs over the Integers
In the preceding sections we considered lasso programs over the reals. In this section we discuss the applicability of the or-to-plus method to linear lasso programs over the integers, i.e., programs where the set of states Σ is a subset of Z n . We still use real-valued ranking functions. We obtain the constraints for coeffi-cients of a linear ranking function with linear supporting invariant by restricting the range of the universal quantification in the constraints ϕ 1 , ϕ 2 , ϕ 3 , and ϕ 4 to the integers. E.g., the constraint ϕ 3 for linear lasso programs over the integers is where the domain of the coefficients r, r 0 , s, and s 0 and the quantified variable δ are the reals. Now, Farkas' lemma is not an equivalence transformation, its application results in weaker formulas. This means the or-to-plus method is still sound, but we loose the completeness result of Theorem 1. An example for this is assume 2*y >= 1; while( x >= 0 ) { x := x -2*y + 1; } the program P nonIntegral , depicted in Figure 8 that has the following transition relations.
Over integer variables, P nonIntegral1 has the linear ranking function f (x, y) = x with the linear supporting invariant y ≥ 1. Over real-valued variables, P nonIntegral1 does not terminate. If we add the additional constraint y ′ ≥ 1 to τ stem , the programs' semantics over the integers is not changed, but we are able to synthesize a linear ranking function with a linear supporting invariant. Adding this additional constraint gives the constraints a property that we formally define as follows.
Integral constraints. A conjunction of linear constraints A·x ≤ b is called integral if the set of satisfying assignments over the reals S := {r ∈ R n | A · r ≤ b} coincides with the integer hull of S (the convex hull of all integer vectors in S).
For each conjunction of m linear constraints there is an equivalent conjunction of at most 2 m linear constraints that is integral [24]. We add an additional step to the or-to-plus method in which we make the constraints in the stem transition τ stem and loop transition τ loop integral.
The Or-to-Plus Method (Int) Input: linear lasso program P with integer variables Output: coefficients r, r 0 , s, and s 0 of linear ranking function with linear supporting invariant Lemma 2 (Integral version of Farkas' Lemma). Given a conjunction of linear constraints A · x ≤ b which is satisfiable and integral, and a linear constraint c ⊺ · x ≤ δ, Proof. We write this statement as a linear programming problem.
Because the constraints A · x ≤ b are integral, there is an integral vector x ∈ Z n such that c ⊺ · x is the optimum solution to (P). Thus the optimum over integers is ≤ δ if and only if the optimum of the reals is. The statement now follows from the real version of Farkas' Lemma.
⊓ ⊔ assume 2*y >= z; while( x >= 0 && z == 1 ) { x := x -2*y + 1; } However, even if τ stem and τ loop are integral, our method is not complete over the integers. In the completeness proof for the reals we applied Farkas' Lemma to conjunctions of a polyhedron A · x ≤ b and an inequality h ⊺ · x + h 0 ≤ 0. This inequality contains free variables, namely the coefficients of the supporting invariant s ⊺ · x + s 0 ≥ 0. Even if τ stem and τ loop are integral, this conjunction might not be integral and we cannot apply the integer version of Farkas' lemma in this case.
A counterexample to completeness of our integer version of the or-to-plus method is the linear lasso program P nonIntegral2 depicted in Figure 9.

Conclusion
We have presented a constraint-based synthesis method for a class of programs that was not investigated before for the synthesis problem. The class is restricted (though less restricted than the widely studied class of simple while programs) but still requires the combined synthesis of not only a ranking function but also an invariant. We have formulated and proven a completeness theorem that gives us an indication on the extent of power of a method that does without nonlinear constraint solving.
We implemented the or-to-plus method as plugin of the Ultimate software analysis framework. A version that allows one to 'play around' with lasso programs is available via a web interface at the following URL. http://ultimate.informatik.uni-freiburg.de/LassoRanker As mentioned in the introduction, the class of lasso programs is motivated by the fact that they are a natural way (and, it seems, the only way) to represent an (infinite) counterexample path in a control flow graph. It is a topic of future research to explore the different scenarios in practical tools that use a module to find a ranking function and a supporting invariant for a lasso program (e.g., in [1,13,15,16,17,21,22]) and to compare the performance of ourtheoretically motivated-synthesis method in comparison with the existingheuristically motivated-approach used presently in the module.