Multiphase-Linear Ranking Functions and their Relation to Recurrent Sets
share
Multiphase ranking functions (MΦRFs) are tuples 〈 f_1,...,f_d 〉 of linear functions that are often used to prove termination of loops in which the computation progresses through a number of "phases". Our work provides new insights regarding such functions for loops described by a conjunction of linear constraints (Single-Path Constraint loops). The decision problem existence of a MΦRF asks to determine whether a given SLC loop admits a MΦRF, and the corresponding bounded decision problem restricts the search to MΦRFs of depth d, where the parameter d is part of the input. The algorithmic and complexity aspects of the bounded problem have been completely settled in a recent work. In this paper we make progress regarding the existence problem, without a given depth bound. In particular, we present an approach that reveals some important insights into the structure of these functions. Interestingly, it relates the problem of seeking MΦRFs to that of seeking recurrent sets (used to prove non-termination). It also helps in identifying classes of loops for which MΦRFs are sufficient. Our research has led to a new representation for single-path loops, the difference polyhedron replacing the customary transition polyhedron. This representation yields new insights on MΦRFs and SLC loops in general. For example, a result on bounded SLC loops becomes straightforward.
READ FULL TEXT