Symbolic decision procedure for termination of linear programs

Tiwari proved that the termination of a class of linear programs is decidable in Tiwari (Proceedings of CAV’04. Lecture notes in computer science, vol 3114, pp 70–82, 2004). The decision procedure proposed therein depends on the computation of Jordan forms. Thus, people may draw a wrong conclusion from this procedure, if they simply apply floating-point computation to compute Jordan forms. In this paper, we first use an example to explain this problem, and then present a symbolic implementation of the decision procedure. Thus, the rounding error problem is therefore avoided. Moreover, we also show that the symbolic decision procedure is as efficient as the numerical one given in Tiwari (Proceedings of CAV’04. Lecture notes in computer science, vol 3114, pp 70–82, 2004). The complexity of former is max{O(n ⁶), O(n ^m+3)}, while that of the latter is O(n ^m+3), where n is the number of variables of the program and m is the number of its Boolean conditions. In addition, for the case when the characteristic polynomial of the assignment matrix is irreducible, we design a more efficient symbolic algorithm whose complexity is max(O(n ⁶), O(mn ³)).