Tags:Ranking Functions, Recurrent Sets and Termination and Nontermination Analysis
Abstract:
Multiphase ranking functions (MPhiRFs) are used to prove termination of loops in which the computation progresses through a number of phases. They consist of linear functions <f1,...,fd> where fi decreases during the i-th phase. This work provides new insights regarding MPhiRFs 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 MPhiRF). The decidability and complexity of the problem, in the case that d is restricted by an input 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 MPhiRFs to that of seeking recurrent sets (used to prove nontermination). It also helps in identifying classes of loops for which MPhiRFs 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 MPhiRFs and SLC loops in general, and some results on termination and nontermination of bounded SLC loops become straightforward.
Multiphase-Linear Ranking Functions and their Relation to Recurrent Sets