Size-change termination with difference constraints

lem of inferring termination from such abstract information is not the halting problem for programs and may well be decidable. If this is the case, the decision algorithm forms a "back end" of a termination verifier and it is interesting to find out the computational complexity of the problem. A restriction of the problem described above, that only uses monotonicity information (but not difference bounds), is already known to be decidable. We prove that the unrestricted problem is undecidable, which gives a theoretical argument for studying restricted cases. We consider a case where the termination proof is allowed to make use of at most one bound per target variable in each transition. For this special case, which we claim is practically significant, we give (for the first time) an algorithm and show that the problem is in PSPACE, in fact that it is PSPACEcomplete. The algorithm is based on combinatorial arguments and results from the theory of integer programming not previo...

• Type: Journal
• Year: 2008
• Where: TOPLAS
• Authors: Amir M. Ben-Amram
• Keywords: Algorithms, Halting Problem, Termination Verifier, TOPLAS 2008