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 P-1 whose assignment matrix (A) over tilde is not in the Jordan canonical form is equivalent to that of a linear program J(1) 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 P-1 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 J(1.) Any point in such a subset is a witness to non termination of Program J(1). Furthermore, it is shown that Program J(1) 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 J(1) 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 A((B) over cap)-invariant for some positive integer (B) over cap. This enables us to check directly the termination of Program J(1) by verifying the satisfiability of finitely many quantified formulas over the reals. This suggests our second method for checking the termination of Program J(1). (C) 2017 Elsevier B.V. All rights reserved.