Witness to non-termination of linear programs

In his CAV 2004 paper, Tiwari has proved that, for a class of linear programs over the reals, termination is decidable. And Tiwari has shown that the termination of a linear program P1 whose assignment matrix A˜ is not in the Jordan canonical form is equivalent to that of a linear program J1, whose assignment matrix A is in the Jordan Canonical Form. In most cases, the method of Tiwari provides only a so-called N-nonterminating point. In this paper, we propose two new methods to decide whether Program P1 terminates or not over the reals. Our methods are based on the construction of a subset of the set NT of non-terminating points of Program J1. Any point in such a subset is a witness to non-termination of Program J1. Furthermore, it is shown that Program J1 is non-terminating if and only if such a subset is nonempty. In terms of the property, the first method is given to check whether Program J1 terminates or not. Different from the existing methods, the point obtained by our first method is a non-terminating point, rather than a N-nonterminating point. More importantly, such a subset is also proven to be ABˆ-invariant for some positive integer Bˆ. This enables us to check directly the termination of Program J1 by verifying the satisfiability of finitely many quantified formulas over the reals. This suggests our second method for checking the termination of Program J1.