On ranking functions for single-path linear-constraint loops

Abstract

Program termination is a fundamental research topic in program analysis. In this paper, we present a new complete polynomial-time method for the existence problem of linear ranking functions for single-path loops described by a conjunction of linear constraints, when variables range over the reals (or rationals). Unlike existing methods, our method does not depend on Farkas’ Lemma and provides us with counterexamples to existence of linear ranking functions, when no linear ranking function exists. In addition, we extend our results established over the rationals to the setting of the integers. This deduces an alternative approach to deciding whether or not a given SLC loop has a linear ranking function over the integers. Finally, we prove that the termination of bounded single-path linear-constraint loops is decidable over the reals (or rationals).

1 Introduction

Proving termination of loops in programs is an important problem whose solutions can broadly improve software reliability. A standard technique to prove the termination of a loop is to find a ranking function, which maps program states to elements of some well-founded ordered set, such that the value descends whenever the loop completes an iteration. Several methods for synthesizing ranking functions have been suggested [2, 4, 5, 8, 10,11,12,13, 17, 20, 22, 26]. And the complexity of the linear ranking function problem for linear-constraint loops is discussed in [3, 5].

In this paper, we focus on single-path linear-constraint loops (SLC loops for short), which are specified by a conjunction of linear constraints. For SLC loops, inequalities in their loop bodies may arise due to abstraction. We now take an example from [5] to describe such loops. The loop with two integer variables $x_1,x_2$,

$$\begin{aligned} {\hbox {while}}\;&( 4x_1\ge x_2 \wedge x_2\ge 1)\; {\hbox {do}}\; \\&\{ x_1:=(2x_1+1)/5; x_2:=x_2 \}, \end{aligned}$$

whose loop body consists of deterministic update statements, can be represented by linear constraints:

$$\begin{aligned} {\hbox {while}}\;&(4x_1\ge x_2 \wedge x_2\ge 1)\; {\hbox {do}} \nonumber \\&\{5x'_1\le 2x_1+1; 5x'_1\ge 2x_1-3; x'_2=x_2\}. \end{aligned}$$

(1)

The latter is usually called an SLC loop, where the loop body is interpreted as expressing a relation between the new values $(x'_1,x'_2)$ and the previous values $(x_1,x_2)$. Generally, this representation allows nondeterminism. Obviously, the above SLC loop is specified by a system of linear inequalities:

$$\begin{aligned} \{4x_1\ge x_2 , x_2\ge 1,5x'_1\le 2x_1+1, 5x'_1\ge 2x_1-3, x'_2=x_2\}. \end{aligned}$$

More examples of programs with nondeterministic update statements can be found in [2, 5, 8, 13].

As a special class of ranking functions, linear ranking functions (LRFs) are widely used in termination analysis of SLC loops. In this case, such a function has the form $\rho (x_1,\ldots ,x_n)=a_1x_1+\cdots +a_nx_n+a_0.$ A formal definition will be given in Sect. 2.3. It is well known that for a given SLC loop, if it has an LRF, then the loop must be terminating [15, 26, 29]. And the problem of synthesizing LRFs can be reduced to a linear programming (LP) problem. Algorithms to synthesize LRFs of SLC loops using linear programming are given in [2, 11, 15, 26, 29]. However, not all terminating loops have LRFs. Lexicographic ranking functions [4, 5, 8] and multiphase ranking functions [4, 20] are natural extension of LRFs, which can be used to handle loops having no LRF. Bagnara and Mesnard [2] describes the notion of eventual linear ranking functions (ELRFs) and establishes algorithms to detect such ranking functions. In fact, ELRFs are multiphase ranking functions (with up to two phases) [4].

Existing methods, relying on Farkas’ Lemma, usually decide the existence of LRFs by attempting to construct one. However, if one just wants to decide the existence of LRFs but not to get an LRF, it is not necessary to synthesize LRFs. Especially, when a given SLC loop has no LRF, the methods based on Farkas’ Lemma cannot provide us with counterexamples, i.e., evidences to why LRFs cannot exist for the loop. In the paper, we focus on the existence problem of LRFs for SLC loops and present a new complete method for checking if an SLC loop has LRFs over the reals, the rationals and the integers. The new approach enables us to decide the existence of LRFs without computing a concrete LRF. Unlike the existing methods based on the famous Farkas’ Lemma, our method does not depend on Farkas’ Lemma. Besides, we prove that for bounded SLC loops, i.e., each variable occurring in SLC loops is bounded, their termination problem over the reals (or rationals) can be determined by checking if such loops have fixed points. In [21], Leike et al. establish a similar result too, which relates the termination of a bounded SLC loop to its fixed points, by constructing a Cauchy sequence. However, our proof is completely distinct from theirs. This will be discussed in Theorem 8 and its corollaries.

The rest of the paper is organized as follows. Section 2 gives some basic background necessary for this work. Section 3 gives a new complete polynomial-time method for deciding if a given SLC loop has an LRF, presents an alternative method for deciding existence of LRFs over the integers and shows that a bounded SLC loop is nonterminating over the reals (or rationals) iff it has a fixpoint. Section 4 concludes.

2 Preliminaries

In this section, some basic definitions on polyhedra, Farkas’ Lemma and linear ranking functions will be introduced.

2.1 Polyhedra

The following concepts of polyhedron, cone and polytope can be found in [28].

Polyhedra A convex polyhedron ${{\mathscr {P}}}\subseteq {\mathbb {R}}^n$ is the set of solutions of a system of linear inequalities $A{\mathbf {x}}\ge {\mathbf {b}},$ i.e., ${\mathscr {P}}=\{{\mathbf {x}}\in {\mathbb {R}}^n :\; A{\mathbf {x}}\ge {\mathbf {b}}\}$. In other words, convex polyhedra defined as above are the intersection of finitely many closed half-spaces. This means that convex polyhedra are closed. In addition, if $A{\mathbf {x}}\ge {\mathbf {b}}$ has real solutions, we say that ${\mathscr {P}}$ is defined by $A{\mathbf {x}}\ge {\mathbf {b}}$. Especially, when $A\in {\mathbb {Q}}^{m\times n}$ is a rational matrix of n columns and m rows, ${\mathbf {x}}\in {\mathbb {Q}}^n$ and ${\mathbf {b}}\in {\mathbb {Q}}^m$ are column vectors of n and m rational values, respectively, for convenience, we call ${\mathscr {P}}_{{\mathbb {Q}}}=\{{\mathbf {x}}\in {\mathbb {Q}}^n :\; A{\mathbf {x}}\ge {\mathbf {b}}\}$ the rational polyhedron. It is well known that

Proposition 1

For a given polyhedron ${\mathscr {P}}\subseteq {\mathbb {R}}^n$ specified by a rational matrix A and a rational vector ${\mathbf {b}}$, ${\mathscr {P}}\ne \emptyset$ if and only if its corresponding rational polyhedron ${\mathscr {P}}_{{\mathbb {Q}}}\ne \emptyset .$

Proposition 1 tells us that for a given system of linear inequalities with rational coefficients, it has a real solution if and only if it has a rational solution.

For a given rational polyhedron ${\mathscr {P}}_{{\mathbb {Q}}}\subseteq {\mathbb {Q}}^n$, let $I({\mathscr {P}}_{{\mathbb {Q}}})=\{{\mathbf {x}}\in {\mathbb {Z}}^n:\; {\mathbf {x}}\in {\mathscr {P}}_{{\mathbb {Q}}}\},$ which is exactly the set of integer points of ${\mathscr {P}}_{{\mathbb {Q}}}$. For a rational polyhedron ${\mathscr {P}}_{{\mathbb {Q}}}$ defined as above, the integer hull of ${\mathscr {P}}_{{\mathbb {Q}}}$, denoted by ${\mathscr {P}}^{{\mathrm{Int}}}_{{\mathbb {Q}}}$, is defined as the convex hull of $I({\mathscr {P}}_{{\mathbb {Q}}})$.

Proposition 2

([5, 19]) With the above notion. We have

• (1) Every rational point of ${\mathscr {P}}^{{\mathrm{Int}}}_{{\mathbb {Q}}}$ is a convex combination of integer points;

• (2) ${\mathscr {P}}^{{\mathrm{Int}}}_{{\mathbb {Q}}}$ is also a rational polyhedron;

• (3) ${\mathscr {P}}^{{\mathrm{Int}}}_{{\mathbb {Q}}}\subseteq {\mathscr {P}}_{{\mathbb {Q}}}$;

• (4) $I({\mathscr {P}}^{{\mathrm{Int}}}_{{\mathbb {Q}}})=I({\mathscr {P}}_{{\mathbb {Q}}})$.

Especially, an integer polyhedron is a rational polyhedron ${\mathscr {P}}_{{\mathbb {Q}}}$ such that ${\mathscr {P}}_{{\mathbb {Q}}}={\mathscr {P}}^{{\mathrm{int}}}_{{\mathbb {Q}}}$. In that case, we say that ${\mathscr {P}}_{{\mathbb {Q}}}$ is integral.

Cones A nonempty set ${\mathscr {C}}$ of points in an Euclidean space is called a cone if $u{\mathbf {x}}+v{\mathbf {y}}\in {\mathscr {C}}$ whenever ${\mathbf {x}},{\mathbf {y}}\in {\mathscr {C}}$ and $u,v\ge 0.$ A cone ${\mathscr {C}}$ is polyhedral if ${\mathscr {C}}=\{{\mathbf {x}}\in {\mathbb {R}}^n: A{\mathbf {x}}\ge {\mathbf {0}}\}$ for some matrix A. Clearly, any polyhedral cone contains the origin.

Recession directions Given a nonempty convex set ${\mathscr {D}},$ a vector d is a recession direction, if the following condition is satisfied:

$$\begin{aligned} {\mathbf {x}}+\lambda d\in {\mathscr {D}},\quad \forall {\mathbf {x}}\in {\mathscr {D}}, \forall \lambda \ge 0. \end{aligned}$$

Denote by ${\mathscr {R}}_{{\mathscr {D}}}$ the set of recession directions of ${\mathscr {D}}.$ In particular, the set of recession directions of a polyhedron ${\mathscr {P}}$ defined by $A{\mathbf {x}}\ge {\mathbf {b}}$ is the set ${\mathscr {R}}_{{\mathscr {P}}}=\{{\mathbf {y}}\in {\mathbb {R}}^n: A{\mathbf {y}}\ge {\mathbf {0}}\}.$ It is easy to see that ${\mathscr {R}}_{{\mathscr {P}}}$ is a polyhedral cone.

Polytopes A set ${\mathscr {Q}}$ of vectors is a convex polytope if it is the convex hull of finitely many vectors.

Theorem 1

([28] Decomposition theorem for polyhedra) A set ${\mathscr {P}}$ of vectors in Euclidean space is a convex polyhedron if and only if ${\mathscr {P}}={\mathscr {Q}}+{\mathscr {C}}$ for some convex polytope ${\mathscr {Q}}$ and some polyhedral cone ${\mathscr {C}}$.

Remark 1

In Formula ${\mathscr {P}}={\mathscr {Q}}+{\mathscr {C}}$, ${\mathscr {P}}$ is called an algebraic sum of ${\mathscr {Q}}$ and ${\mathscr {C}}$. Here, we define the algebraic sum $A+B$ to be $\{a+b: a\in A, b\in B\}$ for subsets A and B of a vector space. Since ${\mathscr {C}}$ is a polyhedral cone, ${\mathscr {C}}$ contains the origin. So, we have that ${\mathscr {Q}}\subseteq {\mathscr {P}}.$ Especially, the decomposition theorem is also true for a rational polyhedron ${\mathscr {P}}_{{\mathbb {Q}}}\subseteq {\mathbb {Q}}^n$ [28].

Theorem 1 implies the following generator representation of convex polyhedra.

Generator representation Convex polyhedra can also be expressed by vertices and rays, as follows:

$$\begin{aligned} {\mathscr {P}}= {\hbox {convhull}}\{{\mathbf {x}}_1,\ldots ,{\mathbf {x}}_m\} +{\hbox {cone}}\{{\mathbf {y}}_1,\ldots ,{\mathbf {y}}_t\} \end{aligned}$$

(2)

where ${\mathbf {x}}_i\in {\mathbb {R}}^n$ are vertices and ${\mathbf {y}}_i \in {\mathbb {R}}^n$ are rays. Formula (2) shows that ${\mathscr {P}}$ specified by $A{\mathbf {x}}\ge {\mathbf {b}}$ can be generated by the points ${\mathbf {x}}_1,\ldots ,{\mathbf {x}}_m\in {\mathscr {P}}$ and by the recession directions ${\mathbf {y}}_1,\ldots ,{\mathbf {y}}_t\in {\mathscr {R}}_{{\mathscr {P}}},$ where $m<+\infty , t<+\infty .$ That is, $\mathscr {P}={\mathscr {Q}}+{\mathscr {R}}_{{\mathscr {P}}}$, where ${\mathscr {Q}}\triangleq {\hbox {convhull}}\{{\mathbf {x}}_1,\ldots ,{\mathbf {x}}_m\}$ and ${\mathscr {R}}_{{\mathscr {P}}}\triangleq {\hbox {cone}}\{{\mathbf {y}}_1,\ldots ,{\mathbf {y}}_t\}$. In other words, ${\mathbf {x}}\in {\mathscr {P}}$ if and only if ${\mathbf {x}}={\mathbf {x}}_B+d_{\mathbf {x}}$ where ${\mathbf {x}}_B\in {\mathscr {Q}}$ and $d_{\mathbf {x}}\in {\mathscr {R}}_{{\mathscr {P}}}$. Furthermore, ${\mathbf {x}}\in {\mathscr {P}}(\triangleq A{\mathbf {x}}\ge {\mathbf {b}})$ if and only if ${\mathbf {x}}=\sum ^{m}_{i=1}u_i\cdot {\mathbf {x}}_i+\sum ^{t}_{j=1}v_j\cdot {\mathbf {y}}_j$ for some $u_i,v_j\ge 0$, where $\sum ^{m}_{i=1}u_i=1.$ By the above arguments, we get that

(3)

Note that ${\mathscr {P}}_{{\mathbb {Q}}}$ and ${\mathscr {P}}^{{\mathrm{int}}}_{{\mathbb {Q}}}$ have the similar Generator Representation as in (3), as follows:

(4)

where ${\mathbf {x}}_i\in {\mathbb {Q}}^n$ is vertex for $i=1,\ldots ,m$ and ${\mathbf {y}}_j\in {\mathbb {Q}}^n$ is ray for $j=1,\ldots ,t$ and ${\mathbb {Q}}^+$ is the set of nonnegative rational numbers, and

(5)

where ${\mathbf {x}}_i\in {\mathbb {Z}}^n$ is vertex for $i=1,\ldots ,m$ and ${\mathbf {y}}_j\in {\mathbb {Z}}^n$ is ray for $j=1,\ldots ,t$.

The following theorem tells us that convex polytopes are bounded.

Theorem 2

([28] Finite basis theorem for polytopes). A set ${\mathscr {Q}}$ is a convex polytope if and only if ${\mathscr {Q}}$ is a bounded convex polyhedron.

For a convex polyhedron ${\mathscr {P}}={\mathscr {Q}}+{\mathscr {C}},$ we know ${\mathscr {Q}}$ is a closed, bounded and convex set, i.e., compact convex set. Moreover, since ${\mathscr {C}}={\mathscr {R}}_{{\mathscr {P}}}$ and ${\mathscr {R}}_{{\mathscr {P}}}=\{{\mathbf {y}}\in {\mathbb {R}}^n: A{\mathbf {y}}\ge {\mathbf {0}}\}$ which is closed and convex, by the above arguments, we have

Proposition 3

Let ${\mathscr {P}}={\mathscr {Q}}+{\mathscr {C}}$ be a convex polyhedron. We have ${\mathscr {Q}}$ is a compact convex set and ${\mathscr {C}}$ is a closed convex set.

2.2 Single-path linear-constraint loops

A single-path linear-constraint loop (SLC for short) over n variables $x_1,\ldots ,x_n$ has the form

$$\begin{aligned} {\hbox {while}}\; ( {B}{\mathbf {x}}\ge {\mathbf {c}})\; {\hbox {do}}\; H{\mathbf {x}}+H'{\mathbf {x}}'\ge {\mathbf {v}}, \end{aligned}$$

(6)

where ${\mathbf {x}},{\mathbf {x}}'\in {\mathbb {R}}^n,$ $B\in {\mathbb {Q}}^{p\times n},{\mathbf {c}}\in {\mathbb {Q}}^p,$ $H\in {\mathbb {Q}}^{q\times n}$, $H'\in {\mathbb {Q}}^{q\times n},$ ${\mathbf {v}}\in {\mathbb {Q}}^q.$ The constraints ${B}{\mathbf {x}}\ge {\mathbf {c}}$ and $H{\mathbf {x}}+H'{\mathbf {x}}'\ge {\mathbf {v}}$ are the loop condition and the loop body, respectively. And the loop body is interpreted as expressing a relation between the new values ${\mathbf {x}}'$ and the previous values ${\mathbf {x}}.$ The update is called deterministic if for a given ${\mathbf {x}}$ (satisfying the loop condition), there is at most one ${\mathbf {x}}'$ satisfying the update constraint. Otherwise, such update is called nondeterministic. For example, the affine linear update ${\mathbf {x}}'=D{\mathbf {x}}+b$ is a deterministic update, since when the value of ${\mathbf {x}}$ is fixed, ${\mathbf {x}}'$ has only one value. It is easy to see that the single-path linear-constraint loop defined as in (6) can always be characterized by the system of linear inequalities

$$\begin{aligned} A {\mathbf {x}}+A' {\mathbf {x}}'\ge {\mathbf {b}}, \end{aligned}$$

(7)

where $A=\left( \begin{array}{c}B\\ H \end{array} \right) \in {\mathbb {Q}}^{(p+q)\times {n}}$, $A'=\left( \begin{array}{c}{\mathbf {0}}\\ H' \end{array} \right) \in {\mathbb {Q}}^{(p+q)\times {n}}$, ${\mathbf {b}}=\left( \begin{array}{c}{\mathbf {c}}\\ {\mathbf {v}} \end{array} \right) \in {\mathbb {Q}}^{(p+q)}$.

An SLC loop as in (6) can be identified with its corresponding system of linear inequalities. In what follows, for convenience, we always write SLC loops with their corresponding systems of linear inequalities.

Transition For an SLC loop defined by (7), we say that there is a transition from a state (current state) ${\mathbf {x}}$ to a state (next state) ${\mathbf {x}}'$, if $({\mathbf {x}},{\mathbf {x}}')$ satisfies the system $A {\mathbf {x}}+A' {\mathbf {x}}'\ge {\mathbf {b}}.$ For simplifying the presentation, define

$$\begin{aligned} \varOmega =\{({\mathbf {x}},{\mathbf {x}}')\in {\mathbb {R}}^{2n}:\;A {\mathbf {x}}+A' {\mathbf {x}}'\ge {\mathbf {b}}\}. \end{aligned}$$

Obviously, $\varOmega$ is a convex polyhedron. It is also closed. Let

$$\begin{aligned} \varOmega _{{\mathbb {Q}}}=\{({\mathbf {x}},{\mathbf {x}}')\in {\mathbb {Q}}^{2n}:\;A {\mathbf {x}}+A' {\mathbf {x}}'\ge {\mathbf {b}}\} \end{aligned}$$

be the rational polyhedron.

2.3 Linear ranking functions

It is well known that termination problem is undecidable. The dominant method for termination analysis is based on the synthesis of ranking functions. For a given loop, the existence of ranking functions implies that the loop is terminating. Let $\pi _{{\mathbf {x}}}:\; {\mathbb {K}}^{2n}\rightarrow {\mathbb {K}}^n$, ${\mathbb {K}}\in \{{\mathbb {R}},{\mathbb {Q}},{\mathbb {Z}}\},$ be a projection mapping, i.e., $\pi _{{\mathbf {x}}}({\mathbf {x}},{\mathbf {x}}')={\mathbf {x}}.$ Clearly, $\pi _{{\mathbf {x}}}$ is a linear mapping. The definitions of termination, nontermination and linear ranking functions are as follows.

Definition 1

(Termination and nontermination) Given an SLC loop P specified by $\varOmega \subseteq {\mathbb {R}}^{2n}$, we say that Loop P is terminating over the reals, if there does not exist an infinite sequence $\{{\mathbf {x}}_i\}^{+\infty }_{i=0} \subseteq {\mathbb {R}}^n$ such that $A{{\mathbf {x}}_i}+A'{{\mathbf {x}}_{i+1}}\ge {\mathbf {b}}$ for any $i\ge 0.$ We say that Loop P is nonterminating over the reals, if such an infinite sequence exists.

Definition 2

Given an SLC loop P defined by $\varOmega$, let $\rho ({\mathbf {x}})={\mathbf {a}}^T{\mathbf {x}}+c$ be a linear function, where ${\mathbf {a}}\in {\mathbb {Q}}^n$ and $c\in {\mathbb {Q}}.$ Then, $\rho ({\mathbf {x}})$ is a linear ranking function over the reals for P if the following formula holds

$$\begin{aligned} \forall ({\mathbf {x}},{\mathbf {x}}')\in \varOmega \Rightarrow (\rho ({\mathbf {x}})\ge 0\wedge \rho ({\mathbf {x}})-\rho ({\mathbf {x}}')\ge 1). \end{aligned}$$

(8)

Remark 2

Note that $\forall ({\mathbf {x}},{\mathbf {x}}')\in \varOmega \Rightarrow \rho ({\mathbf {x}})\ge 0$ is equivalent to $\forall {\mathbf {x}}\in \pi _{{\mathbf {x}}}(\varOmega ) \Rightarrow \rho ({\mathbf {x}})\ge 0,$ where $\pi _{{\mathbf {x}}}$ is a projection mapping from ${\mathbb {R}}^{2n}$ to ${\mathbb {R}}^n$. It is very easy to see that if we replace $\varOmega$ in Formula (8) with $\varOmega _{{\mathbb {Q}}}$ (resp. $I(\varOmega _{{\mathbb {Q}}})$), then we get the definition of ranking functions over the rationals (resp. the integers).

Proposition 4

Given an SLC loop P defined by $\varOmega ,$ there exists a linear ranking function over the reals for P if and only if there exists a linear ranking function over the rationals for P.

Proof

It is clear that P has an LRF over the reals implies that P has an LRF over the rationals. We next show the converse is true. Suppose that P has an LRF over the rationals, i.e.,

$$\begin{aligned} \forall ({\mathbf {x}},{\mathbf {x}}')\in \varOmega _{{\mathbb {Q}}} \Rightarrow (\rho ({\mathbf {x}})\ge 0\wedge \rho ({\mathbf {x}})-\rho ({\mathbf {x}}')\ge 1). \end{aligned}$$

(9)

Since $\varOmega$ is closed, $\varOmega _{\mathbb {Q}}\subseteq \varOmega$ and the rationals are dense in the reals, for any $({\hat{\mathbf {x}}},{\hat{\mathbf {x}}}')\in \varOmega$, there exists a sequence $\{({\mathbf {x}}_j,{\mathbf {x}}'_j)\}^{\infty }_{j=0}\subseteq \varOmega _{\mathbb {Q}}$, such that $({\mathbf {x}}_j,{\mathbf {x}}'_j) \rightarrow ({\mathbf {x}},{\mathbf {x}}'),$ as j goes to infinity. By (9), we have $\rho ({\mathbf {x}}_j)\ge 0\wedge \rho ({\mathbf {x}}_j)-\rho ({\mathbf {x}}'_j)\ge 1$ for all $j=1,2,3,\ldots$. Therefore, when j tends to infinity, we get $\rho ({\hat{\mathbf {x}}})\ge 0\wedge \rho ({\hat{\mathbf {x}}})-\rho ({\hat{\mathbf {x}}}')\ge 1$. Since $({\hat{\mathbf {x}}},{\hat{\mathbf {x}}}')$ is taken arbitrarily from $\varOmega$, we get Formula (8) is true. $\square$

Remark 3

Proposition 4 tells us that seeking a linear ranking function over $\varOmega \subseteq {{\mathbb {R}}^{2n}}$ is equivalent to seeking an LRF over $\varOmega _{{\mathbb {Q}}}\subseteq {\mathbb {Q}}^{2n}$.

Farkas’ Lemma plays an important role in termination analysis, especially in the synthesis of LRFs for linear-constraint loops. It is known that Farkas’ Lemma is true not only over the reals, but also over the rationals. So, it can be used to synthesize ranking functions not only over the reals, but also over the rationals. Existing methods of synthesizing LRFs for linear-constraint loops usually utilize Farkas’ Lemma to transform the generated $\exists \forall$-constraint into an $\exists$-constraint. Let $I\subseteq {\mathbb {R}}^n$ (or ${\mathbb {Q}}^n$) be a nonempty set defined by a system of linear inequalities, i.e.,

$$\begin{aligned} I:\;\; \left\{ \begin{array}{cccccccc} a_{11}x_1&{}+&{}\cdots &{}+&{}a_{1n}x_n&{}+&{}b_1&{}\ge 0\\ \cdots &{}+&{}\cdots &{}+&{}\cdots &{}+&{}\cdots &{}\ge 0\\ a_{m1}x_1&{}+&{}\cdots &{}+&{}a_{mn}x_n&{}+&{}b_m&{}\ge 0 \end{array} \right. \end{aligned}$$

Farkas’ Lemma states that the equivalence of

$$\begin{aligned} \forall (x_1,\ldots ,x_n )\in I \Rightarrow c_1x_1+\cdots +c_nx_n+d\ge 0 \end{aligned}$$

and

$$\begin{aligned} \begin{aligned}&\exists \lambda _1\ge 0,\ldots ,\exists \lambda _m\ge 0 \\&\quad \left( \left( d\ge \sum ^{m}_{i=1}\lambda _ib_i\right) \wedge \bigwedge ^{n}_{j=1} \left( c_j=\sum ^{m}_{i=1}\lambda _ia_{ij}\right) \right) . \end{aligned} \end{aligned}$$

We next take an example to illustrate how to decide if an SLC loop has an LRF via the existing methods depending on Farkas’ Lemma.

Example 1

Consider the SLC loop

$$\begin{aligned} {\hbox {Loop}}: \{x_1\ge 0, x_1-x_2\ge 1, x'_1=x_1-1,x'_2\le x_1\} \end{aligned}$$

(10)

Let $\varOmega =\{(x_1,x_2,x'_1,x'_2)\in {\mathbb {R}}^{4}:\;x_1\ge 0, x_1-x_2\ge 1, x'_1=x_1-1,x'_2\le x_1\}$. Predefine an LRF template $\rho (x_1,x_2)=ax_1+bx_2+c.$ By Definition 2, we need to check if the following $\exists \forall$-constraint (11) is satisfiable,

$$\begin{aligned}&\exists a\exists b \exists c\forall {(x_1,x_2,x'_1,x'_2)}\in \varOmega \Rightarrow ax_1+bx_2+c\ge 0 \nonumber \\&\quad \wedge \, a(x_1-x'_1)+b(x_2-x'_2)\ge 1. \end{aligned}$$

(11)

By Farkas’ Lemma, one can extract the $\exists$-constraint below,

$$\begin{aligned}&\exists a\exists b\exists c.\nonumber \\&\quad \left\{ \begin{array}{ll} &{}a=\lambda _{11}+\lambda _{12}+\lambda _{13}-\lambda _{14}+\lambda _{15}\\ &{}b=-\lambda _{12}\\ &{}0=-\lambda _{13}+\lambda _{14}\\ &{}0=-\lambda _{15}\\ &{}c\ge -\lambda _{12}-\lambda _{13}+\lambda _{14}\\ &{}a=\lambda _{21}+\lambda _{22}+\lambda _{23}-\lambda _{24}+\lambda _{25}\\ &{}b=-\lambda _{22}\\ &{}-a=-\lambda _{23}+\lambda _{24}\\ &{}-b=-\lambda _{25}\\ &{}-1\ge -\lambda _{22}-\lambda _{23}+\lambda _{24}\\ &{}\lambda _{1i}\ge 0,\lambda _{2i}\ge 0, i=1,\ldots ,5 \end{array}\right\} \end{aligned}$$

(12)

from the $\exists \forall$-constraint in (11). Next, it remains to determine if $\exists$-constraint (12) is satisfiable. Solving (12) by LP solver, we obtain a solution:

$$\begin{aligned}&a=1,b=0,c=0, \lambda _{11}=1,\lambda _{12}=0, \lambda _{13}=0, \lambda _{14}=0,\\&\lambda _{15}=0, \lambda _{21}=0, \lambda _{22}=0, \lambda _{23}=1, \lambda _{24}=0, \lambda _{25}=0. \end{aligned}$$

This immediately implies that the loop in (10) indeed has an LRF $\rho (x_1,x_2)=x_1$. Therefore, the loop is terminating.

From the above arguments, we can see that the existing methods usually convert the existence problem of LRFs to a synthesis problem of LRFs, since solving the $\exists$-constraint obtained by Farkas’ Lemma implies an LRF can be constructed if the constraint derived is feasible. In Sect. 3, we will present a new method to extract an $\exists$-constraint from a given SLC loop. Such the $\exists$-constraint obtained by our method has two features:

• an SLC loop has an LRF iff the $\exists$-constraint obtained by our method is not feasible

• when the $\exists$-constraint obtained by our method is feasible, one can construct a set of witnesses for nonexistence of LRFs from the $\exists$-constraint.

The above two features are clearly distinct from the $\exists$-constraint derived by the existing methods depending on Farkas’ Lemma. This is because, for an SLC loop, the corresponding $\exists$-constraint obtained by Farkas’ Lemma is feasible iff the loop has an LRF. More importantly, once the $\exists$-constraint generated by Farkas’ Lemma is not feasible, one just knows that the loop has no LRF, but does not know the reason why it has no LRF. In Sect. 3, we will discuss this issue.

3 Termination of SLC loops

In this section, we consider the termination of SLC loops defined in (7). We first give a new complete method for checking if an SLC loop has an LRF over the reals. Such method can be naturally extended to the setting of the rationals, according to Propositions 1 and 4. And then, we present an alternative approach to decide if an SLC loop has an LRF over the integers. Especially, for a bounded SLC loop, we show that it is nonterminating over the reals (or rationals) if and only if it has a fixed point.

Let us restrict the considered field to be the field ${\mathbb {R}}$ of real numbers. That is, we first restrict our attention to the termination over the reals of SLC loops. This is because, the separating hyperplane theorem is built over ${\mathbb {R}}$, which is very useful for us to establish the desired results on termination analysis of SLC loops. By Proposition 4, for an SLC loop, it has an LRF over the reals if and only if it has an LRF over the rationals. However, it should be pointed out that an SLC loop that is nonterminating over the reals may be terminating over the integers. For instance, let us consider Loop (1) from Sect. 1. The loop is clearly nonterminating on the point $(\frac{1}{4},1)$. But, the loop is indeed terminating over the integers, since it has an LRF $\rho (x_1,x_2)=x_1-1$ over the integers [5]. For the existence problem of LRFs over the integers for SLC loops, more details will be given later.

Let P be an SLC loop specified by $\varOmega$. Let

$$\begin{aligned} Fix_\varOmega =\{({\mathbf {x}},{\mathbf {x}}')\in {\mathbb {R}}^{2n}: A{{\mathbf {x}}}+A'{{\mathbf {x}}'}\ge {\mathbf {b}}, {\mathbf {x}}={\mathbf {x}}'\}. \end{aligned}$$

Let $\pi _{{\mathbf {x}}}(Fix_\varOmega )=\{{\mathbf {x}}\in {\mathbb {R}}^n:\; A{{\mathbf {x}}}+A'{{\mathbf {x}}'}\ge {\mathbf {b}} , {\mathbf {x}}={\mathbf {x}}'\},$ where $\pi _{{\mathbf {x}}}$ is the projection mapping defined as before.

Definition 3

(Fixed points of SLC loops) For Loop P defined by $\varOmega$, if $\pi _{{\mathbf {x}}}(Fix_{\varOmega })$ is not empty, then each point of $\pi _{{\mathbf {x}}}(Fix_\varOmega )$ is called a fixed point of P. We call $\pi _{{\mathbf {x}}}(Fix_\varOmega )$ the set of fixed points of P.

Definition 4

(Bounded SLC loops) Let P be an SLC loop specified by $\varOmega$. We say that Loop P is a bounded SLC loop, if each variable occurring in $\varOmega$ is bounded, i.e., there exists a positive number $\gamma$, such that for all $({\mathbf {x}},{\mathbf {x}}')\in \varOmega$, $(-\gamma ,\ldots ,-\gamma )\le {\mathbf {x}},{\mathbf {x}}'\le (\gamma ,\ldots ,\gamma )$.

In general, the image of a closed set under a linear mapping is not necessarily closed. This can be seen by the following example.

Example 2

Let $D=\{(x_1,x_2)\in {\mathbb {R}}^2_{+}:\; x_1x_2\ge 1\}$, and let $T(x_1,$ $x_2)=x_1$, where ${\mathbb {R}}_{+}$ is the set of nonnegative real numbers. Clearly, D is closed and T is a linear mapping. But the image $T(D)={\mathbb {R}}_{++}$ of D under T is open, where ${\mathbb {R}}_{++}$ is the set of positive real numbers.

However, in the following, we will show that for a linear mapping T and a convex polyhedron ${\mathscr {P}}$ defined as before, the image $T({\mathscr {P}})$ of ${\mathscr {P}}$ under T is a closed convex set. This result will be used in the proof of Theorem 4.

Proposition 5

Let $T:{\mathbb {R}}^u \rightarrow {\mathbb {R}}^v$ be a linear mapping. Let ${\mathscr {P}}={\mathscr {Q}}+{\mathscr {C}}$ be a convex polyhedron. The image $T({\mathscr {P}})$ of ${\mathscr {P}}$ under the linear mapping T is a closed convex set.

Proof

Since ${\mathscr {P}}$ is a convex polyhedron, by Formula (3), we have

Since T is a linear mapping, by its linearity, we get

(13)

By Formula (13), the image $T({\mathscr {P}})$ is generated by the vertices $T({\mathbf {x}}_i)$’s and the rays $T({\mathbf {y}}_j)$’s. By Theorem 1 and generator representation of polyhedra, we know the image $T({\mathscr {P}})$ is a convex polyhedron. Therefore, $T({\mathscr {P}})$ is clearly a closed convex set. $\square$

Lemma 1

[7] Let U and V be two convex sets of ${\mathbb {R}}^n$, which do not intersect, i.e., $U\cap V=\emptyset .$ Then there exist ${\mathbf {a}}\ne {\mathbf {0}}$ and b such that ${\mathbf {a}}^{\mathrm{T}}{\mathbf {x}}\le b$ for all ${\mathbf {x}}\in U$ and ${\mathbf {a}}^{\mathrm{T}}{\mathbf {x}}\ge b$ for all ${\mathbf {x}}\in V$.

By Lemma 1, if U and V are two disjoint nonempty convex subsets, then there exists an affine function ${\mathbf {a}}^{\mathrm{T}}{\mathbf {x}}-b$ that is nonpositive on U and nonnegative on V. Such a hyperplane $\{{\mathbf {x}}:\;{\mathbf {a}}^{\mathrm{T}}{\mathbf {x}}={b}\}$ is called a separating hyperplane for U and V. Additionally, we say that the affine function ${\mathbf {a}}^{\mathrm{T}}{\mathbf {x}}-b$ strictly separates U and V, if ${\mathbf {a}}^{\mathrm{T}}{\mathbf {x}}< b$ for all ${\mathbf {x}}\in U$ and ${\mathbf {a}}^{\mathrm{T}}{\mathbf {x}}> b$ for all ${\mathbf {x}}\in V$. Although disjoint convex sets cannot necessarily be strictly separated by a hyperplane, the following lemma tells us that in the special case when U is a closed convex set and V is a single-point set, there indeed exists a hyperplane which can strictly separate U and V.

Lemma 2

[7] Let $U\subseteq {\mathbb {R}}^u$ be a closed convex set and ${\mathbf {x}}_0\not \in U$. Then, there exists a hyperplane that strictly separates ${\mathbf {x}}_0$ from U.

Lemma 3

[19] Let $f:{\mathbb {R}}^u\rightarrow {\mathbb {R}}$ be a linear mapping, and let $U\subseteq {\mathbb {R}}^u$ be a nonempty convex polyhedron. Let $\delta :={\hbox {sup}}\{f({\mathbf {u}}):\; {\mathbf {u}}\in U\}< \infty$. Then, there exists a vector ${\mathbf {z}}\in U$ with $f({\mathbf {z}})=\delta$.

Lemma 3 shows us that if the supremum of the linear function $f({\mathbf {u}})$ over a nonempty polyhedron is finite, then its supremum can be attained. By Lemma 3, we have

Lemma 4

Let $f:{\mathbb {R}}^u\rightarrow {\mathbb {R}}$ be a linear mapping, and let $U\subseteq {\mathbb {R}}^u$ be a nonempty convex polyhedron. If $f({\mathbf {u}})\ne 0$ for all ${\mathbf {u}}\in U,$ then there exists a positive number $\delta$ such that either $f({\mathbf {u}})\ge \delta$ for all ${\mathbf {u}}\in U,$ or $f({\mathbf {u}})\le -\delta$ for all ${\mathbf {u}}\in U.$

Proof

Since U is a closed connected set and $f({\mathbf {u}})\ne 0$ for all ${\mathbf {u}}\in U,$ there will be two cases: (i) $f({\mathbf {u}})< 0$ for all ${\mathbf {u}}\in U.$ (ii) $f({\mathbf {u}})> 0$ for all ${\mathbf {u}}\in U.$ Next, we will show that if Case (i) occurs, i.e., $f({\mathbf {u}})<0$ for all ${\mathbf {u}}\in U$, then there exists a positive number $\delta$ such that $f({\mathbf {u}})\le -\delta$ for all ${\mathbf {u}}\in U$. For Case (i), set $\gamma ={\hbox {sup}}\{f({\mathbf {u}}):{\mathbf {u}}\in U\}$. Since $f({\mathbf {u}})<0$ for all ${\mathbf {u}}\in U$, we have $\gamma \le 0.$ Next, we further show that $\gamma \ne 0.$ Suppose that $\gamma =0$. Then, since $\gamma \le 0<\infty ,$ by Lemma 3, there must exist ${\mathbf {z}}\in U,$ such that $f({\mathbf {z}})=\gamma =0$. This clearly contradicts with the hypothesis that $f({\mathbf {u}})\ne 0$ for all ${\mathbf {u}}\in U$. Hence, $\gamma <0.$ Let $\delta =-\gamma >0.$ Then, we have $f({\mathbf {u}})\le -\delta$ for all ${\mathbf {u}}\in U.$ For Case (ii), let $g=-f.$ Then, an similar analysis as above is applicable to Case (ii). $\square$

In the following, we will consider the existence problem of LRFs, and further show that if P has no LRFs, then there must exist a subset of $\varOmega$ which makes P have no LRF. So, any point in such subset is a witness for nonexistence of LRFs. More importantly, such subset can be characterized by a certain system of linear inequalities. This also naturally relates the existence of LRFs for SLC loops to feasibility of systems of linear inequalities. Next, we first establish the following result.

Theorem 3

Let $\varOmega =\{({\mathbf {x}},{{\mathbf {x}}'})\in {\mathbb {R}}^{2n}: A{\mathbf {x}}+A'{{\mathbf {x}}'}\ge 0 \}$ be a convex polyhedron and let $\varOmega _{H}=\{(d_{\mathbf {x}},d_{{\mathbf {x}}'})\in {\mathbb {R}}^{2n}: Ad_{\mathbf {x}}+A'd_{{\mathbf {x}}'}\ge 0 \}$ be the set of recession directions of $\varOmega$. Then

$$\begin{aligned} \exists k(\forall ({\mathbf {x}},{\mathbf {x}}')\in \varOmega \Rightarrow ({\mathbf {a}}^{\mathrm{T}}{\mathbf {x}}\ge k \wedge {\mathbf {a}}^{\mathrm{T}}({\mathbf {x}}-{\mathbf {x}}')\ge 1 )) \end{aligned}$$

(14)

is equivalent to

$$\begin{aligned} (\forall ({\mathbf {x}},{\mathbf {x}}')\in \varOmega , \forall (d_{\mathbf {x}},d_{{\mathbf {x}}'})\in \varOmega _{H} )\Rightarrow {\mathbf {a}}^{\mathrm{T}}({\mathbf {x}}-{\mathbf {x}}'+d_{{\mathbf {x}}})\ge 1.\nonumber \\ \end{aligned}$$

(15)

Proof

(14)$\Rightarrow$ (15). Because $\varOmega _H$ is the set of recession directions of $\varOmega$, by the property of recession directions mentioned in Sect. 2.1, for any $(d_{\mathbf {x}},d_{{\mathbf {x}}'})\in \varOmega _H$, any $({\mathbf {x}},{\mathbf {x}}')\in \varOmega$, and any $\lambda \ge 0$, we have

$$\begin{aligned} ({\mathbf {x}},{\mathbf {x}}')+\lambda (d_{\mathbf {x}},d_{{\mathbf {x}}'})\in \varOmega . \end{aligned}$$

(16)

By (14) and (16), since ${\mathbf {a}}^{\mathrm{T}}{\mathbf {x}}\ge k$ for all $({\mathbf {x}},{\mathbf {x}}')\in \varOmega$ and $({\mathbf {x}}+\lambda d_{\mathbf {x}},{\mathbf {x}}'+\lambda d_{{\mathbf {x}}'})\in \varOmega$ for any $(d_{\mathbf {x}},d_{{\mathbf {x}}'})\in \varOmega _H$, any $({\mathbf {x}},{\mathbf {x}}')\in \varOmega$, and any $\lambda \ge 0$, it follows that

$$\begin{aligned} {\mathbf {a}}^{\mathrm{T}}({\mathbf {x}}+\lambda d_{\mathbf {x}})\ge k \end{aligned}$$

(17)

for any $(d_{\mathbf {x}},d_{{\mathbf {x}}'})\in \varOmega _H$, any $({\mathbf {x}},{\mathbf {x}}')\in \varOmega$, and any $\lambda \ge 0$. Next, we will show that Formula (17) implies that

$$\begin{aligned} {\mathbf {a}}^Td_{{\mathbf {x}}} \ge 0 \end{aligned}$$

(18)

for any $(d_{\mathbf {x}},d_{{\mathbf {x}}'})\in \varOmega _H$. Suppose that there exists a recession direction $(\hat{d}_{\mathbf {x}},\hat{d}_{{\mathbf {x}}'})\in \varOmega _H$ such that ${\mathbf {a}}^{\mathrm{T}}\hat{d}_{{\mathbf {x}}} < 0$. Then, take arbitrarily a point $({\hat{\mathbf {x}}},{\hat{\mathbf {x}}}')$ from $\varOmega$. Clearly,

$$\begin{aligned} ({\hat{\mathbf {x}}}+\lambda \hat{d}_{{\mathbf {x}}},{\hat{\mathbf {x}}}'+\lambda \hat{d}_{{\mathbf {x}}'})\in \varOmega \end{aligned}$$

(19)

for any $\lambda \ge 0,$ since $(\hat{d}_{\mathbf {x}},\hat{d}_{{\mathbf {x}}'})$ is a recession direction. In addition, since ${\mathbf {a}}^{\mathrm{T}}{\mathbf {x}}\ge k$ for all $({\mathbf {x}},{\mathbf {x}}')\in \varOmega$, by (19), we get ${\mathbf {a}}^{\mathrm{T}}({\hat{\mathbf {x}}}+\lambda \hat{d}_{{\mathbf {x}}})\ge k$ for any $\lambda \ge 0.$ But, as $\lambda \rightarrow +\infty ,$ ${\mathbf {a}}^{\mathrm{T}}({\hat{\mathbf {x}}}+\lambda \hat{d}_{{\mathbf {x}}})\rightarrow -\infty$, since ${\mathbf {a}}^{\mathrm{T}}\hat{d}_{{\mathbf {x}}} < 0$. This contradicts Formula (17). Therefore, Formula (18) holds for any $(d_{\mathbf {x}},d_{{\mathbf {x}}'})\in \varOmega _H$. Moreover, by Formula (14), for all $({\mathbf {x}},{\mathbf {x}}')\in \varOmega$, we have

$$\begin{aligned} {\mathbf {a}}^{\mathrm{T}}({\mathbf {x}}-{\mathbf {x}}')\ge 1. \end{aligned}$$

(20)

Hence, adding Formulas (18)–(20), we get that Formula (15) is true.

(15)$\Rightarrow$ (14). By Formula (15), we know ${\mathbf {a}}^{\mathrm{T}}({\mathbf {x}}-{\mathbf {x}}'+d_{{\mathbf {x}}})\ge 1$ for any $({\mathbf {x}},{{\mathbf {x}}'})\in \varOmega$, and any $(d_{\mathbf {x}},d_{{\mathbf {x}}'})\in \varOmega _H.$ Since $({\mathbf {0}},{\mathbf {0}})\in \varOmega _H,$ we have

$$\begin{aligned} {\mathbf {a}}^{\mathrm{T}}({\mathbf {x}}-{\mathbf {x}}'+{\mathbf {0}}) ={\mathbf {a}}^{\mathrm{T}}({\mathbf {x}}-{\mathbf {x}}')\ge 1 \end{aligned}$$

(21)

for any $({\mathbf {x}},{{\mathbf {x}}'})\in \varOmega$. So, the remaining thing is to prove that ${\mathbf {a}}^{\mathrm{T}}{\mathbf {x}}\ge k$ for all $({\mathbf {x}},{\mathbf {x}}') \in \varOmega .$ Because the set $\varOmega _H$ of recession directions of $\varOmega$ is a cone, we get $\lambda (d_{\mathbf {x}},d_{{\mathbf {x}}'})\in \varOmega _H$ for any $\lambda \ge 0$ and any $(d_{\mathbf {x}},d_{{\mathbf {x}}'})\in \varOmega _H$. Hence, by Formula (15), it follows that ${\mathbf {a}}^{\mathrm{T}}({\mathbf {x}}-{\mathbf {x}}'+\lambda d_{\mathbf {x}})\ge 1$ for any $({\mathbf {x}},{{\mathbf {x}}'})\in \varOmega$, any $\lambda \ge 0$ and any $(d_{\mathbf {x}},d_{{\mathbf {x}}'})\in \varOmega _H.$ We next will claim that

$$\begin{aligned} {\mathbf {a}}^{\mathrm{T}} d_{{\mathbf {x}}}\ge 0 \end{aligned}$$

(22)

for any $(d_{{\mathbf {x}}},d_{{\mathbf {x}}'})\in \varOmega _H.$ Suppose that there exists $(\check{d}_{{\mathbf {x}}},\check{d}_{{\mathbf {x}}'})\in \varOmega _H$ such that ${\mathbf {a}}^{\mathrm{T}} \check{d}_{{\mathbf {x}}}< 0$. Then, take arbitrarily a point $({\check{\mathbf {x}}},{\check{\mathbf {x}}}')$ from $\varOmega$. Since $\lambda (\check{d}_{{\mathbf {x}}},\check{d}_{{\mathbf {x}}'})\in \varOmega _H$ for any $\lambda \ge 0,$ in terms of Formula (15), we have

$$\begin{aligned} {\mathbf {a}}^{\mathrm{T}}({\check{\mathbf {x}}}-{\check{\mathbf {x}}}'+\lambda \check{d}_{{\mathbf {x}}})\ge 1 \end{aligned}$$

(23)

for any $\lambda \ge 0$. But, since ${\mathbf {a}}^{\mathrm{T}} \check{d}_{{\mathbf {x}}}< 0,$ when $\lambda \rightarrow +\infty ,$ we have ${\mathbf {a}}^{\mathrm{T}}({\check{\mathbf {x}}}-{\check{\mathbf {x}}}'+\lambda \check{d}_{{\mathbf {x}}})\rightarrow -\infty ,$ which clearly contradicts Formula (15). Therefore, Formula (22) holds for any $(d_{{\mathbf {x}}},d_{{\mathbf {x}}'})\in \varOmega _H.$ Finally, we will show that there exists a constant k such that ${\mathbf {a}}^{\mathrm{T}}{\mathbf {x}}\ge k$ for any $({\mathbf {x}},{{\mathbf {x}}'})\in \varOmega .$ Since $\varOmega$ is convex polyhedron, by Theorem 1 and Generator Representation, we have $\varOmega ={\mathscr {Q}}+{\mathscr {R}}_{\varOmega },$ where ${\mathscr {Q}}={\hbox {convhull}}\{{\mathbf {x}}_1,\ldots ,{\mathbf {x}}_m\}$, ${\mathbf {x}}_i\in \varOmega$ for $i=1,\ldots ,m,$ is a convex polytope and ${\mathscr {R}}_{\varOmega }=\varOmega _H.$ By Theorem 2 and Proposition 3, ${\mathscr {Q}}$ is a closed, bounded and convex set. Since $\varOmega ={\mathscr {Q}}+{\mathscr {R}}_{\varOmega },$ by the definition of algebraic sum, $({\mathbf {x}}^{\mathrm{T}},{\mathbf {x}}'^{\mathrm{T}})^{\mathrm{T}}\in \varOmega$ if and only if there exist $({\mathbf {x}}^{\mathrm{T}}_B,{{\mathbf {x}}'}^{\mathrm{T}}_B)^{\mathrm{T}}\in {\mathscr {Q}}$ and $(d^{\mathrm{T}}_{\mathbf {x}},d^{\mathrm{T}}_{{\mathbf {x}}'})^{\mathrm{T}}\in \varOmega _H$ such that

$$\begin{aligned} \left( \begin{array}{c}{\mathbf {x}}\\ {\mathbf {x}}'\end{array}\right) =\left( \begin{array}{c}{\mathbf {x}}_B\\ {\mathbf {x}}'_B\end{array}\right) +\left( \begin{array}{c}d_{\mathbf {x}}\\ d_{{\mathbf {x}}'}\end{array}\right) \end{aligned}$$

(24)

Let us construct an auxiliary linear function

$$\begin{aligned}\ell ({\mathbf {z}},{\mathbf {z}}')=({\mathbf {a}}^{\mathrm{T}},{\mathbf {0}})\left( \begin{array}{c} {\mathbf {z}}\\ {\mathbf {z}}' \end{array}\right) . \end{aligned}$$

Since $\ell ({\mathbf {z}},{\mathbf {z}}')$ is continuous and ${\mathscr {Q}}$ is a bounded and closed set, there must exist a constant k, such that $\ell ({\mathbf {x}}_B,{\mathbf {x}}'_B)\ge k$ for all $({\mathbf {x}}_B,{\mathbf {x}}'_B)\in {\mathscr {Q}}.$ Furthermore, by (22), since ${\mathbf {a}}^{\mathrm{T}} d_{{\mathbf {x}}}\ge 0$ for any $(d_{{\mathbf {x}}},d_{{\mathbf {x}}'})\in \varOmega _H,$ we get

$$\begin{aligned} \ell (d_{{\mathbf {x}}},d_{{\mathbf {x}}'})=({\mathbf {a}}^{\mathrm{T}},{\mathbf {0}}) \left( \begin{array}{c} d_{{\mathbf {x}}}\\ d_{{\mathbf {x}}'} \end{array}\right) \ge 0 \end{aligned}$$

for all $(d_{{\mathbf {x}}},d_{{\mathbf {x}}'})\in \varOmega _H$. By the above arguments and Formula (24), for any $({\mathbf {x}},{\mathbf {x}}')\in \varOmega ,$

$$\begin{aligned} \ell ({\mathbf {x}},{\mathbf {x}}')=\ell ({\mathbf {x}}_B,{\mathbf {x}}'_B) +\ell (d_{{\mathbf {x}}},d_{{\mathbf {x}}'})\ge k. \end{aligned}$$

This means that ${\mathbf {a}}^{\mathrm{T}}{\mathbf {x}}\ge k$ for all $({\mathbf {x}},{\mathbf {x}}') \in \varOmega .$ Hence, Formula (14) is true. This completes the proof of the theorem. $\square$

Remark 4

Note that in Formula (15), $\forall ({\mathbf {x}},{\mathbf {x}}')\in \varOmega , \forall (d_{\mathbf {x}},d_{{\mathbf {x}}'})\in \varOmega _{H}$ can also be rewritten as $\forall ({\mathbf {x}},{\mathbf {x}}',d_{\mathbf {x}},d_{{\mathbf {x}}'})\in \varOmega \times \varOmega _{H}$.

Theorem 3 establishes an equivalence relation between Formulas (14) and (15), when $\varOmega$ is a convex polyhedron. In particular, for an SLC loop P defined by $\varOmega$, Formula (14) indicates $\rho ({\mathbf {x}})={\mathbf {a}}^{\mathrm{T}}{\mathbf {x}}-k$ is exactly an LRF for P. Hence, Theorem 3 tells us that P has an LRF $\rho ({\mathbf {x}})={\mathbf {a}}^{\mathrm{T}}{\mathbf {x}}-k$ over the reals if and only if ${\mathbf {a}}^{\mathrm{T}}({\mathbf {x}}-{\mathbf {x}}'+d_{{\mathbf {x}}})\ge 1$ for all $({\mathbf {x}},{\mathbf {x}}',d_{\mathbf {x}},d_{{\mathbf {x}}'})\in \varOmega \times \varOmega _{H}\subseteq {\mathbb {R}}^{4n}.$

Let $(\varOmega \times \varOmega _{H})_{{\mathbb {Q}}}=\{({\mathbf {x}},{\mathbf {x}}',d_{\mathbf {x}},d_{{\mathbf {x}}'})\in {\mathbb {Q}}^{4n}: A{{\mathbf {x}}}+A'{{\mathbf {x}}'}\ge {\mathbf {b}}, A{d_{\mathbf {x}}}+A'{d_{\mathbf {x}}'}\ge 0 \}.$ By the proof of Proposition 4, we know Formula (14) is equivalent to

$$\begin{aligned} \exists k(\forall ({\mathbf {x}},{\mathbf {x}}')\in \varOmega _{{\mathbb {Q}}} \Rightarrow ({\mathbf {a}}^{\mathrm{T}}{\mathbf {x}}\ge k \wedge {\mathbf {a}}^{\mathrm{T}}({\mathbf {x}}-{\mathbf {x}}')\ge 1 )). \end{aligned}$$

(25)

In addition, adopting the similar strategy in the proof of Proposition 4, we get that Formula (15) is equivalent to

$$\begin{aligned} (\forall ({\mathbf {x}},{\mathbf {x}}',d_{\mathbf {x}},d_{{\mathbf {x}}'})\in (\varOmega \times \varOmega _{H} )_{{\mathbb {Q}}}\Rightarrow {\mathbf {a}}^{\mathrm{T}}({\mathbf {x}}-{\mathbf {x}}'+d_{{\mathbf {x}}})\ge 1.\nonumber \\ \end{aligned}$$

(26)

By the above arguments, we have

Corollary 1

Let $\varOmega$, $\varOmega _{{\mathbb {Q}}}$, $\varOmega \times \varOmega _{H}$ and $(\varOmega \times \varOmega _{H} )_{{\mathbb {Q}}}$ be defined as before. We have (25) $\Leftrightarrow$ (26).

Proof

Since (14) is equivalent to (25) and (15) is equivalent to (26), by Theorem 3, (25) is equivalent to (26). $\square$

Theorem 4

Let $\varOmega$ be defined as before. Let $\varOmega _H$ be the set of recession directions of $\varOmega$, and let P be an SLC loop defined by $\varOmega$. Define

$$\begin{aligned} \varDelta \triangleq {\mathbf {x}}-{\mathbf {x}}'+d_{{\mathbf {x}}}={\mathbf {0}}\wedge \underbrace{Ad_{\mathbf {x}}+A'd_{{\mathbf {x}}'}\ge {\mathbf {0}}}_{\varOmega _H} \wedge \underbrace{A{\mathbf {x}}+A'{\mathbf {x}}'\ge {\mathbf {b}}}_{\varOmega } \end{aligned}$$

to be a system of inequalities. Then, the system $\varDelta$ has no real solutions if and only if P has a linear ranking function over the reals.

Proof

Suppose that $\varDelta$ has no real solutions. Let

$$\begin{aligned} U({\mathbf {x}},{\mathbf {x}}',d_{\mathbf {x}},d_{{\mathbf {x}}'})={\mathbf {x}}-{\mathbf {x}}'+d_{{\mathbf {x}}}. \end{aligned}$$

Clearly, U is a linear mapping from ${\mathbb {R}}^{4n}$ to ${\mathbb {R}}^n$. Let $\varOmega \times \varOmega _{H}=\{({\mathbf {x}},{\mathbf {x}}',d_{\mathbf {x}},d_{{\mathbf {x}}'}):\; A{\mathbf {x}}+A'{\mathbf {x}}'\ge {\mathbf {b}}\wedge Ad_{{\mathbf {x}}}+A'd_{{\mathbf {x}}'}\ge {\mathbf {0}} \}.$ Obviously, the set $\varOmega \times \varOmega _{H}\subseteq {\mathbb {R}}^{4n}$ is a convex polyhedron. Let $U(\varOmega \times \varOmega _{H})=\{U({\mathbf {x}},{\mathbf {x}}',d_{\mathbf {x}},d_{{\mathbf {x}}'}): ({\mathbf {x}},{\mathbf {x}}',d_{\mathbf {x}},d_{{\mathbf {x}}'})\in \varOmega \times \varOmega _{H}\}.$ Thus, since $U({\mathbf {x}},{\mathbf {x}}',d_{\mathbf {x}},d_{{\mathbf {x}}'})$ is a linear mapping and $\varOmega \times \varOmega _{H}$ is a convex polyhedron, by Proposition 5, the image $U(\varOmega \times \varOmega _{H})$ of $\varOmega \times \varOmega _{H}$ under the linear mapping U is also a closed convex set. Thus, $\varDelta$ has no real solutions, is equivalent to,

$$\begin{aligned} (\forall ({\mathbf {x}},{\mathbf {x}}')\in \varOmega , \forall (d_{\mathbf {x}},d_{{\mathbf {x}}'})\in \varOmega _H )\Rightarrow {\mathbf {x}}-{\mathbf {x}}'+d_{{\mathbf {x}}}\ne {\mathbf {0}}. \end{aligned}$$

This clearly implies that ${\mathbf {0}}\not \in U(\varOmega \times \varOmega _{H}).$ Because $U(\varOmega \times \varOmega _{H})$ is a closed convex set and ${\mathbf {0}}\not \in U(\varOmega \times \varOmega _{H})$, in terms of Lemma 2, there exists a hyperplane ${\mathbf {a}}^{\mathrm{T}}{\mathbf {u}}=e$ strictly separating the origin ${\mathbf {0}}\in {\mathbb {R}}^n$ from $U(\varOmega \times \varOmega _{H})\subseteq {\mathbb {R}}^n.$ That is, ${\mathbf {a}}^{\mathrm{T}}{\mathbf {u}}\ne e$ for any ${\mathbf {u}}\in U(\varOmega \times \varOmega _{H}).$ Since ${\mathbf {a}}^{\mathrm{T}}{\mathbf {u}}=e$ strictly separates the origin ${\mathbf {0}}$ from $U(\varOmega \times \varOmega _{H})$, the hyperplane ${\mathbf {a}}^{\mathrm{T}}{\mathbf {u}}=0$ passing through the origin and parallel to ${\mathbf {a}}^{\mathrm{T}}{\mathbf {u}}=e$, must be disjoint from $U(\varOmega \times \varOmega _{H})$. Therefore, we have ${\mathbf {a}}^{\mathrm{T}}{\mathbf {u}}\ne 0$ for any ${\mathbf {u}}\in U(\varOmega \times \varOmega _{H})$. By the definition of $U(\varOmega \times \varOmega _{H})$, we further have that ${\mathbf {a}}^{\mathrm{T}}({\mathbf {x}}-{\mathbf {x}}'+d_{{\mathbf {x}}})\ne 0$ for any $({\mathbf {x}},{\mathbf {x}}')\in \varOmega$ and any $(d_{\mathbf {x}},d_{{\mathbf {x}}'})\in \varOmega _H$ (i.e., any $({\mathbf {x}},{\mathbf {x}}',d_{\mathbf {x}},d_{{\mathbf {x}}'})\in \varOmega \times \varOmega _{H}$ ), since ${\mathbf {u}}$ is taken from $U(\varOmega \times \varOmega _{H})$. Let $f({\mathbf {x}},{\mathbf {x}}',d_{{\mathbf {x}}},d_{{\mathbf {x}}'})={\mathbf {a}}^{\mathrm{T}}({\mathbf {x}}-{\mathbf {x}}'+d_{{\mathbf {x}}})$. Since f is linear, $\varOmega \times \varOmega _{H}$ is a convex polyhedron and ${\mathbf {a}}^{\mathrm{T}}({\mathbf {x}}-{\mathbf {x}}'+d_{{\mathbf {x}}})\ne 0$ for all $({\mathbf {x}},{\mathbf {x}}',d_{\mathbf {x}},d_{{\mathbf {x}}'})\in \varOmega \times \varOmega _{H}$, according to Lemma 4, there must exist a positive number $\delta$ such that either (i) ${\mathbf {a}}^{\mathrm{T}}({\mathbf {x}}-{\mathbf {x}}'+d_{{\mathbf {x}}})\ge \delta$ for all $({\mathbf {x}},{\mathbf {x}}',d_{\mathbf {x}},d_{{\mathbf {x}}'})\in \varOmega \times \varOmega _{H}$, or (ii) ${\mathbf {a}}^{\mathrm{T}}({\mathbf {x}}-{\mathbf {x}}'+d_{{\mathbf {x}}})\le -\delta$ for all $({\mathbf {x}},{\mathbf {x}}',d_{\mathbf {x}},d_{{\mathbf {x}}'})\in \varOmega \times \varOmega _{H}$. If Case (i) occurs, then $\frac{{\mathbf {a}}^{\mathrm{T}}}{\delta }({\mathbf {x}}-{\mathbf {x}}'+d_{{\mathbf {x}}})\ge 1$ for all $({\mathbf {x}},{\mathbf {x}}',d_{\mathbf {x}},d_{{\mathbf {x}}'})\in \varOmega \times \varOmega _{H}$. Then, by Theorem 3, we have

$$\begin{aligned} \forall ({\mathbf {x}},{\mathbf {x}}')\in \varOmega \Rightarrow \left( \frac{{\mathbf {a}}^{\mathrm{T}}}{\delta }{\mathbf {x}}\ge k \wedge \frac{{\mathbf {a}}^{\mathrm{T}}}{\delta }({\mathbf {x}}-{\mathbf {x}}')\ge 1 \right) \end{aligned}$$

(27)

for a certain constant k. This indicates that $\rho ({\mathbf {x}})=\frac{{\mathbf {a}}^{\mathrm{T}}}{\delta }{\mathbf {x}}$ is exactly an LRF for P. If Case (ii) occurs, then $-\frac{{\mathbf {a}}^{\mathrm{T}}}{\delta }({\mathbf {x}}-{\mathbf {x}}'+d_{{\mathbf {x}}})\ge 1$ for all $({\mathbf {x}},{\mathbf {x}}',d_{\mathbf {x}},d_{{\mathbf {x}}'})\in \varOmega \times \varOmega _{H}$. This implies

$$\begin{aligned} \forall ({\mathbf {x}},{\mathbf {x}}')\in \varOmega \Rightarrow \left( -\frac{{\mathbf {a}}^{\mathrm{T}}}{\delta }{\mathbf {x}}\ge k \wedge -\frac{{\mathbf {a}}^{\mathrm{T}}}{\delta }({\mathbf {x}}-{\mathbf {x}}')\ge 1 \right) \end{aligned}$$

(28)

according to Theorem 3. That is, $\rho ({\mathbf {x}})=-\frac{{\mathbf {a}}^{\mathrm{T}}}{\delta }{\mathbf {x}}$ is an LRF for P. To sum up, if the system $\varDelta$ has no real solutions, then P has an LRF.

The remaining thing is to show that if the system $\varDelta$ has real solutions, then P has no LRF. It is trivial to prove this. This is because, once the system $\varDelta$ has real solutions, i.e., there exists a point $({\tilde{\mathbf {x}}},{\tilde{\mathbf {x}}}',\tilde{d}_{\mathbf {{x}}},\tilde{d}_{\mathbf {{x}}'})\in \varOmega \times \varOmega _H$, such that ${\tilde{\mathbf {x}}}-{\tilde{\mathbf {x}}}'+\tilde{d}_{{\mathbf {x}}}={\mathbf {0}},$ we have ${\mathbf {a}}^{\mathrm{T}}({\tilde{\mathbf {x}}}-{\tilde{\mathbf {x}}}'+{\tilde{d}}_{\mathbf {{x}}})\equiv 0 \ngeq 1$ for any vector ${\mathbf {a}}^{\mathrm{T}}\in {\mathbb {R}}^n.$ Hence, Formula (15) cannot hold for any fixed vector ${\mathbf {a}}^{\mathrm{T}} \in {\mathbb {R}}^n.$ This means that Formula (14) cannot hold for any fixed vector ${\mathbf {a}}^{\mathrm{T}} \in {\mathbb {R}}^n$ and any $k\in {\mathbb {R}}$ by Theorem 3. Therefore, by Theorem 3 and its remark, P has no LRF. This completes the proof of the theorem. $\square$

Remark 5

Theorem 4 provides us with a new method for determining the existence of LRFs of SLC loops without synthesizing an LRF. Let ${\hbox {Sol}}(\varDelta )\subseteq {\mathbb {R}}^{4n}$ be the solution set of the system $\varDelta$. Let $\pi _{ {\mathbf {x}} }({\hbox {Sol}}(\varDelta ))$ be the projection on ${\mathbf {x}}$ of the polyhedron ${\hbox {Sol}}(\varDelta )$. It is easy to see that $\pi _{ {\mathbf {x}} }({\hbox {Sol}}(\varDelta ))\ne \emptyset$ iff ${\hbox {Sol}}(\varDelta )\ne \emptyset$. And each point in $\pi _{ {\mathbf {x}} }({\hbox {Sol}}(\varDelta ))$ is a witness for nonexistence of LRFs, when $\pi _{ {\mathbf {x}} }({\hbox {Sol}}(\varDelta ))$ is not empty.

For a given SLC loop P defined by $\varOmega$, one can establish an $\exists$-constraint below by Theorem 4,

$$\begin{aligned}&\exists {\mathbf {x}}\exists {\mathbf {x}}'\exists d_{\mathbf {x}}\exists d_{{\mathbf {x}}'} \nonumber \\&\quad ({\mathbf {x}}-{\mathbf {x}}'+d_{{\mathbf {x}}}={\mathbf {0}}\wedge Ad_{\mathbf {x}}+A'd_{{\mathbf {x}}'}\ge {\mathbf {0}} \wedge A{\mathbf {x}}+A'{\mathbf {x}}'\ge {\mathbf {b}}).\nonumber \\ \end{aligned}$$

(29)

Since the expressions in the above $\exists$-constraint are all linear, linear programming (LP) methods, which have polynomial-time complexity, can be directly applied to solve such $\exists$-constraints in polynomial time. Therefore, Theorem 4 provides a complete polynomial-time method to decide whether or not an SLC loop has LRFs over the reals. By Proposition 1, we get that $\varDelta$ has no real solution iff $\varDelta$ has no rational solution, since ${A}, A'$ and ${\mathbf {b}}$ are all rational. So, by Proposition 4 and Theorem 4, we have

Corollary 2

With the above notion. Given an SLC loop P defined by $\varOmega$, $\varDelta$ has no rational solution if and only if P has a linear ranking function over the rationals.

Remark 6

Corollary 2 tells us that $\varDelta$ has no rational solution iff there is an LRF over $\varOmega _{{\mathbb {Q}}}$. The latter means that P has an LRF over the rationals.

With the above arguments, we have the following result.

Theorem 5

Given an SLC loop P,  one can check if P has linear ranking functions over the rationals (or reals) in PTIME. Also, one can find a witness for nonexistence of LRFs in PIME, if there is no LRF for P.

We next take an example to demonstrate how to use Theorem 4 to decide the existence of LRFs of SLC loops.

Example 3

Consider the SLC loop

$$\begin{aligned} {\hbox {Loop}}: \{x\ge 0, x'\le x+y, y'\le y-1, y'\ge -2 \}. \end{aligned}$$

(30)

By the above arguments, construct the $\exists$-constraint by (29):

$$\begin{aligned} \begin{aligned}&\exists x \exists y \exists x' \exists y' \exists d_{x} \exists d_y \exists d_{x'} \exists d_{y'}. \\&( x-x'+d_x=0 \wedge y-y'+d_y=0\wedge x\ge 0 \wedge \\&x'\le x+y \wedge y'\le y-1 \wedge y'\ge -2 \wedge d_x\ge 0 \wedge \\&d_{x'}\le d_x+d_y \wedge d_{y'}\le d_y \wedge d_{y'}\ge 0). \end{aligned} \end{aligned}$$

(31)

By quantifier elimination technique, we find Formula (31) is false. This immediately implies the loop indeed has an LRF by Theorem 4.

For an SLC loop P defined by $\varOmega$, we next show how to reduce equivalently the existence of LRFs over $I(\varOmega _{{\mathbb {Q}}})$ to that of LRFs over $\varOmega ^{{\mathrm{int}}}_{{\mathbb {Q}}}$.

Theorem 6

Let $\varOmega _{{\mathbb {Q}}}\subseteq {\mathbb {Q}}^{2n}$,$I(\varOmega _{{\mathbb {Q}}})\subseteq {\mathbb {Z}}^{2n}$ be defined as before. Let $\varOmega ^{{\mathrm{int}}}_{{\mathbb {Q}}}\subseteq {\mathbb {Q}}^{2n}$ be the integer hull of $\varOmega _{{\mathbb {Q}}}$. Then, there is a linear ranking function over the set $\varOmega ^{{\mathrm{int}}}_{{\mathbb {Q}}}$ if and only if there is a linear ranking function over the set $I(\varOmega _{{\mathbb {Q}}})\subseteq {\mathbb {Z}}^{2n}$.

Proof

It is clear that if there is an LRF over $\varOmega ^{{\mathrm{int}}}_{{\mathbb {Q}}}$, then there must exist an LRF over $I(\varOmega _{{\mathbb {Q}}})$, since $I(\varOmega _{{\mathbb {Q}}})\subseteq \varOmega ^{{\mathrm{int}}}_{{\mathbb {Q}}}$. Next, we show the converse. Suppose $\rho ({\mathbf {x}})={\mathbf {a}}^{\mathrm{T}}{\mathbf {x}}-k$ is an LRF over $I(\varOmega _{{\mathbb {Q}}})$. Then, we have

$$\begin{aligned} \exists k (\forall ({\mathbf {x}},{\mathbf {x}}')\in I(\varOmega _{{\mathbb {Q}}}) \Rightarrow ({\mathbf {a}}^{\mathrm{T}}{\mathbf {x}}\ge k \wedge {\mathbf {a}}^{\mathrm{T}}({\mathbf {x}}-{\mathbf {x}}')\ge 1 )).\nonumber \\ \end{aligned}$$

(32)

By Formula (5), $\varOmega ^{{\mathrm{int}}}_{{\mathbb {Q}}}$ has the following generator representation:

$$\begin{aligned} {\varOmega }^{{\mathrm{int}}}_{{\mathbb {Q}}}\triangleq&\left\{ \sum ^{m}_{i=1}u_i\cdot ({\mathbf {x}}_i,{\mathbf {x}}'_i)+\sum ^{t}_{j=1}v_j\cdot ((d_{\mathbf {x}})_j,(d_\mathbf {x'})_j)\in {\mathbb {Q}}^{2n}:\right. \nonumber \\&\quad \left. \forall u_i,v_j\in {\mathbb {Q}}^+, \sum ^{m}_{i=1}u_i=1\right\} \end{aligned}$$

(33)

where $({\mathbf {x}}_i,{\mathbf {x}}'_i)\in {\mathbb {Z}}^{2n}$ is vertex for $i=1,\ldots ,m$ and $((d_{\mathbf {x}})_j,(d_\mathbf {x'})_j) \in {\mathbb {Z}}^{2n}$ is ray for $j=1,\ldots ,t$. Clearly, any point of the form $({\mathbf {x}}_i,{\mathbf {x}}'_i)+\lambda ((d_{{\mathbf {x}}})_j,(d_{{\mathbf {x}}'})_j)$ with integer $\lambda >0$, for $i=1,\ldots ,m$ and for $j=1,\ldots ,t$, is a point in $I(\varOmega _{{\mathbb {Q}}})$. When $\lambda$ goes to infinity, we have Formula (32) implies

$$\begin{aligned} {\mathbf {a}}^{\mathrm{T}} (d_{\mathbf {x}})_j\ge 0 \wedge {\mathbf {a}}^{\mathrm{T}} ((d_{{\mathbf {x}}})_j-(d_{{\mathbf {x}}'})_j)\ge 0, \end{aligned}$$

(34)

for $i=1,\ldots ,m$ and for $j=1,\ldots ,t$.

By Proposition 2, we know $({\mathbf {x}}_i,{\mathbf {x}}'_i)\in I(\varOmega _{{\mathbb {Q}}})$, for $i=1,\ldots ,m$, since $({\mathbf {x}}_i,{\mathbf {x}}'_i)\in I(\varOmega ^{{\mathrm{int}}}_{{\mathbb {Q}}})$ and $I(\varOmega ^{{\mathrm{int}}}_{{\mathbb {Q}}})\subseteq I(\varOmega _{{\mathbb {Q}}})$. Since $({\mathbf {x}}_i,{\mathbf {x}}'_i)\in I(\varOmega _{{\mathbb {Q}}})$, for $i=1,\ldots ,m$, by (32), it follows that

$$\begin{aligned} {\mathbf {a}}^{\mathrm{T}}{\mathbf {x}}_i\ge k\wedge {\mathbf {a}}^{\mathrm{T}}({\mathbf {x}}_i-{\mathbf {x}}'_i)\ge 1, \end{aligned}$$

(35)

for $i=1,\ldots ,m.$ So, for any point $({\mathbf {x}},{\mathbf {x}}') \in {\varOmega }^{{\mathrm{int}}}_{{\mathbb {Q}}}$, by (33), there exist nonnegative rational numbers $u_i$’s and $v_j$’s with $\sum ^{m}_{i=1}u_i=1$, such that

$$\begin{aligned} ({\mathbf {x}},{\mathbf {x}}') = \sum ^{m}_{i=1}u_i\cdot ({\mathbf {x}}_i,{\mathbf {x}}'_i)+\sum ^{t}_{j=1}v_j\cdot ((d_{\mathbf {x}})_j,(d_\mathbf {x'})_j). \end{aligned}$$

Thus, by (32), (34) and (35), we get

$$\begin{aligned} {\mathbf {a}}^{\mathrm{T}}{\mathbf {x}}= \sum ^{m}_{i=1}u_i\cdot {\mathbf {a}}^{\mathrm{T}} {\mathbf {x}}_i+\sum ^{t}_{j=1}v_j\cdot {\mathbf {a}}^{\mathrm{T}} (d_{\mathbf {x}})_j\ge k, \end{aligned}$$

(36)

for any point $({\mathbf {x}},{\mathbf {x}}') \in {\varOmega }^{{\mathrm{int}}}_{{\mathbb {Q}}}$. Likewise, (32) and (34) imply that

$$\begin{aligned} {\mathbf {a}}^{\mathrm{T}}({\mathbf {x}}-{\mathbf {x}}')= & {} \sum ^{m}_{i=1}u_i\cdot {\mathbf {a}}^{\mathrm{T}}({\mathbf {x}}_i-{\mathbf {x}}'_i)\nonumber \\&+\,\sum ^{t}_{j=1}v_j\cdot {\mathbf {a}}^{\mathrm{T}}((d_{\mathbf {x}})_j-(d_\mathbf {x'})_j)\ge 1 \end{aligned}$$

(37)

for any point $({\mathbf {x}},{\mathbf {x}}') \in {\varOmega }^{{\mathrm{int}}}_{{\mathbb {Q}}}$. So, by (36) and (37), $\rho ({\mathbf {x}})={\mathbf {a}}^{\mathrm{T}}{\mathbf {x}}-k$ is clearly an LRF over ${\varOmega }^{{\mathrm{int}}}_{{\mathbb {Q}}}$. $\square$

We notice that a result similar to Theorem 6 is mentioned already in [15]. Similar to Theorem 4, for the integer setting, we have

Theorem 7

Let $\varOmega$, $\varOmega _{{\mathbb {Q}}}$, $\varOmega ^{{\mathrm{int}}}_{{\mathbb {Q}}}$ be defined as before, and let $(\varOmega ^{{\mathrm{int}}}_{{\mathbb {Q}}})_H$ be the set of recession directions of $\varOmega ^{{\mathrm{int}}}_{{\mathbb {Q}}}$. Let P be an SLC loop defined by $\varOmega$. Define

$$\begin{aligned} \varDelta ^{{\mathrm{int}}}_{{\mathbb {Q}}}&\triangleq {\mathbf {x}}-{\mathbf {x}}'+d_{{\mathbf {x}}}=0 \wedge ({\mathbf {x}},{\mathbf {x}}')\nonumber \\&\quad \in \varOmega ^{{\mathrm{int}}}_{{\mathbb {Q}}}\wedge (d_{{\mathbf {x}}},d_{{\mathbf {x}}'}) \in (\varOmega ^{{\mathrm{int}}}_{{\mathbb {Q}}})_H. \end{aligned}$$

P has a linear ranking function over the integers if and only if $\varDelta ^{{\mathrm{int}}}_{{\mathbb {Q}}}$ has no rational solution.

Proof

Since $\varOmega ^{{\mathrm{int}}}_{{\mathbb {Q}}}$ is a rational polyhedron, by Theorem 4 and Corollary 2, there exists an LRF over $\varOmega ^{{\mathrm{int}}}_{{\mathbb {Q}}}$ if and only if $\varDelta ^{{\mathrm{int}}}_{{\mathbb {Q}}}$ has no rational solution. By Theorem 6, there exists an LRF over $\varOmega ^{{\mathrm{int}}}_{{\mathbb {Q}}}$ if and only if there exists an LRF over $I(\varOmega _{{\mathbb {Q}}}).$ So, P has an LRF over the integers if and only if $\varDelta ^{{\mathrm{int}}}_{{\mathbb {Q}}}$ has no rational solution. $\square$

Remark 7

Different from the method in [5], which equivalently reduces the nonexistence of LRFs over the integers to the unsatisfiability of a system of linear inequalities, Theorem 7 presents an alternative method, which equivalently reduces the nonexistence of LRFs over the integers to the satisfiability of a system of linear inequalities, to check if an SLC loop has an LRF over the integers. Also, $\varDelta ^{{\mathrm{int}}}_{{\mathbb {Q}}}$ characterizes the set of witnesses for nonexistence of LRFs over the integers. Both [5]’s method and ours depend heavily on the computation of integer hulls of polyhedra. Since the computation of the integer hull of a polyhedron defining an SLC loop may require exponential time, our method due to Theorem 7 is not a polynomial-time algorithm.

Example 4

Consider the integer SLC loop from [5]:

$$\begin{aligned} {\hbox {Loop}}: \{x_1\ge 0 \wedge x'_1=x_1+x_2 \wedge x'_2=x_2-1 \}. \end{aligned}$$

(38)

The generator representation of $\varOmega ^{{\mathrm{int}}}_{{\mathbb {Q}}}$ is

$$\begin{aligned} \varOmega ^{{\mathrm{int}}}_{{\mathbb {Q}}}= & {} {\hbox {conhull}}\{({\mathbf {x}}_1,{\mathbf {x}}'_1)\}\nonumber \\ \quad&+\, {\hbox {cone}}\{((d_{\mathbf {x}})_1,(d_{{\mathbf {x}}'})_1), ((d_{\mathbf {x}})_2,(d_{{\mathbf {x}}'})_2),\nonumber \\&\quad ((d_{\mathbf {x}})_3,(d_{{\mathbf {x}}'})_3)\}, \end{aligned}$$

(39)

where $({\mathbf {x}}_1,{\mathbf {x}}'_1)=(0,1,1,0)^{\mathrm{T}}$, $((d_{\mathbf {x}})_1,(d_{{\mathbf {x}}'})_1)=(0,-1,-1,-1)^{\mathrm{T}},$ $((d_{\mathbf {x}})_2,(d_{{\mathbf {x}}'})_2)=(0,1,1,1)^{\mathrm{T}}$, $((d_{\mathbf {x}})_3,(d_{{\mathbf {x}}'})_3)=(1,-1,0,-1)^{\mathrm{T}}$. By Theorem 7, the loop has an LRF over the integers iff $\varDelta ^{{\mathrm{int}}}_{{\mathbb {Q}}}$ has no rational solution. By the above generator representation,

$$\begin{aligned} ({\mathbf {x}},{\mathbf {x}}')= & {} ({\mathbf {x}}_1,{\mathbf {x}}'_1)+u_{11}((d_{\mathbf {x}})_1,(d_{{\mathbf {x}}'})_1)\nonumber \\&+\,u_{12}((d_{\mathbf {x}})_2,(d_{{\mathbf {x}}'})_2)+u_{13}((d_{\mathbf {x}})_3,(d_{{\mathbf {x}}'})_3), \end{aligned}$$

(40)

where $u_{11}, u_{12}, u_{13}\in {\mathbb {Q}}^{+}$, and

$$\begin{aligned} (d_{\mathbf {x}},d_{{\mathbf {x}}'})= & {} u_{21}((d_{\mathbf {x}})_1,(d_{{\mathbf {x}}'})_1)\nonumber \\&+\, u_{22}((d_{\mathbf {x}})_2,(d_{{\mathbf {x}}'})_2)+u_{23}((d_{\mathbf {x}})_3,(d_{{\mathbf {x}}'})_3), \end{aligned}$$

(41)

where $u_{21}, u_{22}, u_{23}\in {\mathbb {Q}}^+.$ Substituting (40) and (41) to $\varDelta ^{{\mathrm{int}}}_{{\mathbb {Q}}}$, we get :

$$\begin{aligned} S\varDelta ^{{\mathrm{int}}}_{{\mathbb {Q}}}= & {} [ { u_{13}}-1+{ u_{11}}-{ u_{12}}+{ u_{23}}=0,\\&1+2\,{ u_{12}}-{ u_{21}}+{ u_{22}}-{ u_{23}}=0,0\le { u_{11}},\\&0\le { u_{12}},0\le { u_{13}},0 \le { u_{21}},0\le { u_{22}},0\le { u_{23}}]. \end{aligned}$$

Note that $S\varDelta ^{{\mathrm{int}}}_{{\mathbb {Q}}}$ consists of linear expressions and just involves with the variables: $u_{11}, u_{12}, u_{13},u_{21}, u_{22}, u_{23}$. Therefore, to check if $\varDelta ^{{\mathrm{int}}}_{{\mathbb {Q}}}$ has a rational solution is equivalent to check if $S\varDelta ^{{\mathrm{int}}}_{{\mathbb {Q}}}$ has a rational solution. Using linear programming (LP) algorithm, we obtain $u_{11}=1, u_{12}=0, u_{13}=0,u_{21}=1, u_{22}=0, u_{23}=0,$ which means that $\varDelta ^{{\mathrm{int}}}_{{\mathbb {Q}}}$ has a rational solution. So, the loop has no LRF over the integers by Theorem 7.

Example 5

Consider Loop (1) from Sect 1. By the similar analysis as in the above example, the corresponding $S\varDelta ^{{\mathrm{int}}}_{{\mathbb {Q}}}$ is obtained as follows:

$$\begin{aligned} S\varDelta ^{{\mathrm{int}}}_{{\mathbb {Q}}}= & {} [3\,{ r_1}+{ r_2}+{ r_3}+{ r_4}+3\,{ r_5}+{ r_6}+3\,{ u_{11}}+3\,\\&{ u_{12}}+5\,{ u_{21}}+5\,{ u_{22}}=0,20\,{ u_{22}}=0,\\&{ r_1}+{ r_2}+{ r_3}+{ r_4}+{ r_5}+{ r_6}=1,\\&0\le { r_1},0\le { r_2},0\le { r_3},0\le { r_4},0\le { r_5},\\&0\le { r_6},0 \le { u_{11}},0\le { u_{12}},0\le { u_{21}},0\le { u_{22}}]. \end{aligned}$$

By verification, $S\varDelta ^{{\mathrm{int}}}_{{\mathbb {Q}}}$ has no rational solution. This implies Loop (1) has an LRF over the integers by Theorem 7.

It is a reasonable assumption in practice that the systems of linear inequalities defining SLC loops are bounded. The following result immediately follows from Theorem 4. It indicates that termination of bounded SLC loops over the reals is decidable. Let $\pi _{{\mathbf {x}}}(\varOmega )=\{{\mathbf {x}}\in {\mathbb {R}}^n: A{{\mathbf {x}}}+A'{{\mathbf {x}}'}\ge {\mathbf {b}}\}$, where $\pi _{{\mathbf {x}}}$ is a projection mapping defined as in Sect. 2.3.

Theorem 8

Let $\varOmega$ and $\varOmega _H$ be defined as before. Let P be an SLC loop defined by $\varOmega$. If $\pi _{{\mathbf {x}}}(\varOmega )$ is bounded, i.e., there exists a positive number $\gamma ,$ such that $(-\gamma ,\ldots ,-\gamma ) \le {\mathbf {x}}\le (\gamma ,\ldots ,\gamma )$ for all ${\mathbf {x}}\in \pi _{{\mathbf {x}}}(\varOmega ),$ then loop P is nonterminating over the reals iff P has at least one fixed point.

Proof

By the definition of $\varOmega _{H}$, we have $\varOmega _{H}=\{(d_{\mathbf {x}},d_{{\mathbf {x}}'}): Ad_{\mathbf {x}}+A'd_{{\mathbf {x}}'}\ge 0 \}$. Then, we will claim that for any $d=(d_{\mathbf {x}},d_{{\mathbf {x}}'})\in \varOmega _H$, $d_{\mathbf {x}}$ must be zero, i.e., $d_{{\mathbf {x}}}\equiv 0,$ when $\pi _{{\mathbf {x}}}({\varOmega })$ is bounded. First, let $(\hat{{\mathbf {x}}},\hat{{\mathbf {x}}}')$ be a point taken arbitrarily from $\varOmega$ and let ${d}=({d}_{\mathbf {x}},{d}_{{\mathbf {x}}'})$ be a recession direction taken arbitrarily from $\varOmega _H$. Then, by the definition of recession directions, for any $\lambda \ge 0,$ we have

$$\begin{aligned} (\hat{{\mathbf {x}}},\hat{{\mathbf {x}}}')+\lambda ({d}_{\mathbf {x}},{d}_{{\mathbf {x}}'})=(\hat{{\mathbf {x}}}+\lambda {d}_{\mathbf {x}},\hat{{\mathbf {x}}}'+\lambda {d}_{{\mathbf {x}}'})\in \varOmega . \end{aligned}$$

Clearly, $\hat{{\mathbf {x}}}+\lambda {d}_{\mathbf {x}}\in \pi _{{\mathbf {x}}}(\varOmega )$ for any $\lambda \ge 0$. Suppose that ${d}_{{\mathbf {x}}}\ne 0$. Then, it is easy to see that

$$\begin{aligned} |\hat{{\mathbf {x}}}+\lambda {d}_{\mathbf {x}}|\rightarrow +\infty ,\;\;(\text {as}\; \lambda \rightarrow +\infty ). \end{aligned}$$

This immediately implies $\pi _{{\mathbf {x}}}({\varOmega })$ is unbounded, which clearly contradicts with the hypothesis that $\pi _{{\mathbf {x}}}({\varOmega })$ is bounded. So, we have ${d}_{{\mathbf {x}}}=0$ for any $d\in \varOmega _{H}$. This implies that the system $\varDelta$ in Theorem 4 can be further written as

$$\begin{aligned} \varDelta \triangleq {\mathbf {x}}-{\mathbf {x}}'={\mathbf {0}}\wedge A'd_{{\mathbf {x}}'}\ge {\mathbf {0}} \wedge A{\mathbf {x}}+A'{\mathbf {x}}'\ge {\mathbf {b}} \end{aligned}$$

(42)

since $d_{{\mathbf {x}}}\equiv 0,$ when $\pi _{{\mathbf {x}}}({\varOmega })$ is bounded. More importantly, it is not difficult to see that Formula (42) has a real solution if and only if the following system

$$\begin{aligned} \tilde{\varDelta } \triangleq {\mathbf {x}}-{\mathbf {x}}'={\mathbf {0}}\wedge A{\mathbf {x}}+A'{\mathbf {x}}'\ge {\mathbf {b}} \end{aligned}$$

(43)

has a real solution. This is because, in Formula (42), one always can set $d_{{\mathbf {x}}'}=0.$ By Definition 3, we know that $\tilde{\varDelta }$ is exactly corresponding to the set $Fix_\varOmega$, whose projection $\pi _{{\mathbf {x}}}(Fix_\varOmega )$ on ${\mathbf {x}}$ is the set of fixed points of Loop P. Therefore, if $\tilde{\varDelta }$ has a real solution, then P has a fixed point, which implies P is nonterminating. Otherwise, if $\tilde{\varDelta }$ has no real solution, then $\varDelta$ has no real solution, too. This immediately means that P has an LRF over the reals, according to Theorem 4. $\square$

Theorem 8 gives a method to decide the termination problem of a class of SLC loops. Given an SLC loop P defined by $\varOmega$, compute its $\pi _{{\mathbf {x}}}(\varOmega )$ first. If $\pi _{{\mathbf {x}}}(\varOmega )$ is bounded, then by Theorem 8, to check if P terminates over the reals is equivalent to check if P has a fixed point.

It is easy to see that when P is a bounded SLC loop, $\pi _{{\mathbf {x}}}(\varOmega )$ is bounded, too. Therefore, the following corollary directly follows from Theorem 8.

Corollary 3

Let P be a bounded SLC loop specified by $\varOmega$. Then, P is nonterminating over the reals iff P has at least one fixed point.

Corollary 4

With the above notion. Let P be a bounded SLC loop specified by $\varOmega$. Then, P is nonterminating over the rationals iff P has at least one fixed point.

Proof

The proof is completely similar to the proof of Theorem 8. By Proposition 1, Formula (43) has a real solution if and only if it has a rational solution. Similarly, the same conclusion also holds for Formula (42). So, by the arguments presented in the proof of Theorem 8, we get that Formula (43) has a rational solution if and only if Formula (42) has a rational solution. Suppose P has at least one real fixed point, i.e., $\pi _{{\mathbf {x}}}(Fix_{\varOmega })\ne \emptyset$. Since $\pi _{{\mathbf {x}}}(Fix_{\varOmega })$, which is the projection of $\tilde{\varDelta }$ on ${\mathbf {x}}$, is also a polyhedron, we have $\tilde{\varDelta }$ has a real solution. It immediately implies that Formula (43) must have a rational solution by Proposition 1. This means that P has at least one rational fixed point. Hence, P is nonterminating over the rationals. Suppose P has no rational fixed point. This means that $\pi _{{\mathbf {x}}}(Fix_{\varOmega })$ has no rational solution. Furthermore, by Proposition 1, we get $\pi _{{\mathbf {x}}}(Fix_{\varOmega })$ has no real solution, i.e., $\pi _{{\mathbf {x}}}(Fix_{\varOmega })= \emptyset$. Then, we have Formula (43) has no real solution. This further implies $\varDelta$ has no real solution. By Theorem 4, P must have a LRF over the reals. This also means that P is terminating over the rationals. $\square$

Example 6

Consider the SLC loop

$$\begin{aligned} {\hbox {Loop}}:&\{2x_1-x_2\ge 1, x_2\le 1, x_1-x_2\le 0,\nonumber \\&\quad -x'_1-x_1+x'_2\ge 0, x_2-x'_2\ge 0\} \end{aligned}$$

(44)

Let $\varOmega = \{(x_1,x_2,x'_1,x'_2):2x_1-x_2\ge 1, x_2\le 1, x_1-x_2\le 0,$ $-x'_1-x_1+x'_2\ge 0, x_2-x'_2\ge 0\}$ and let $Fix_\varOmega = \{(x_1,x_2):2x_1-x_2\ge 1, x_2\le 1, x_1-x_2\le 0, -x'_1-x_1+x'_2\ge 0, x_2-x'_2\ge 0,x_1=x'_1,x_2=x'_2\}$. Eliminating $x'_1,x'_2$ from the system defining $\varOmega$ by quantifier elimination (QE) technique, we obtain $\pi _{(x_1,x_2)}(\varOmega )=\{(x_1,x_2): 2x_1-x_2-1\ge 0, x_1-x_2\le 0, x_2-1\le 0\}.$ $\pi _{(x_1,x_2)}(\varOmega )$ is indeed bounded. Therefore, by Theorem 8, determining if the SLC loop is nonterminating is equivalent to determining if it has a fixed point. To do this, we first need to compute the set $\pi _{(x_1,x_2)}(Fix_\varOmega )$ of fixed points of the loop. For the example, we get $\pi _{(x_1,x_2)}(Fix_\varOmega )=\emptyset .$ This indicates that loop P has no fixed points. Thus, P is terminating over the reals by Theorem 8. Notice that the above loop is not a bounded SLC loop, since not all variables involved can be bounded by a positive number. Hence, Corollary 3 is not applicable to the loop in (44).

By Theorem 8, we have established a necessary and sufficient criterion for the termination of a special class of SLC loops, which relates the termination problem of such SLC loops to the computation of fixed points. However, for SLC loops which do not satisfy its hypothesis, Theorem 8 is not applicable.

4 Conclusion

In this paper, we have analyzed the existence of LRFs of SLC loops and have given a new complete polynomial-time method for checking if a given SLC loop has LRFs over the reals (or rationals). Additionally, for a rational SLC loop specified by a rational polyhedron $\varOmega _{{\mathbb {Q}}}$, introducing the integer hull $\varOmega ^{{\mathrm{int}}}_{{\mathbb {Q}}}$ of $\varOmega _{{\mathbb {Q}}}$, we equivalently reduce the existence of LRFs over the integers to that of LRFs over the rationals. Finally, for a special class of SLC loops, we have shown that their termination problem is decidable over the reals (or rationals).