Although every terminating loop has a ranking function, not every loop has a ranking function of a restricted form, such as a lexicographic tuple of polynomials over program variables. The \emph{polyranking principle} is proposed as a generalization of polynomial ranking for analyzing termination of loops. We define lexicographic polyranking functions in the context of loops with parallel transitions consisting of polynomial assertions, including inequalities, over primed and unprimed variables. Next, we address synthesis of these functions with a complete and automatic method for synthesizing lexicographic linear polyranking functions with supporting linear invariants over loops in which all assertions are linear.
In Proc. 32nd International Colloquium on Automata, Languages and Programming, Lisboa, Portugal, July 2005, Springer Verlag, LNCS 3580, pp 1349-1361.
BibTex, Postscript, PDF. © 2005, Springer Verlag.