Multiphase-Linear Ranking Functions and their Relation to Recurrent Sets

Amir M. Ben-Amram, Jesús J. Doménech, Samir Genaim

Multiphase ranking functions (M$\Phi$RFs) are tuples $⟨f_1,\dots ,f_d⟩$ of linear functions that are often used to prove termination of loops in which the computation pr…