Multiphase-Linear Ranking Functions and Their Relation to Recurrent Sets

Multiphase ranking functions (M Phi RFs) are used to prove termination of loops in which the computation progresses through a number of phases. They consist of linear functions < f(1), ... , f(d)> where f(i) decreases during the ith phase. This work provides new insights regarding MFRFs for loops described by a conjunction of linear constraints (SLC loops). In particular, we consider the existence problem (does a given SLC loop admit a M Phi RF). The decidability and complexity of the problem, in the case that d is restricted by an in(p)ut parameter, have been settled in recent work, while in this paper we make progress regarding the existence problem without a given depth bound. Our new approach, while falling short of a decision procedure for the general case, reveals some important insights into the structure of these functions. Interestingly, it relates the problem of seeking M Phi RFs to that of seeking recurrent sets (used to prove nontermination). It also helps in identifying classes of loops for which M Phi RFs are sufficient, and thus have linear runtime bounds. For the depth-bounded existence problem, we obtain a new polynomial-time procedure that can provide witnesses for negative answers as well. To obtain this procedure we introduce a new representation for SLC loops, the difference polyhedron replacing the customary transition polyhedron. We find that this representation yields new insights on M Phi RFs and SLC loops in general, and some results on termination and nontermination of bounded SLC loops become straightforward.