Ranking Functions for Linear-Constraint Loops
Abstract
In this paper we study the complexity of the problems: given a loop, described by linear constraints over a finite set of variables, is there a linear or lexicographical-linear ranking function for this loop? While existence of such functions implies termination, these problems are not equivalent to termination. When the variables range over the rationals (or reals), it is known that both problems are PTIME decidable. However, when they range over the integers, whether for single-path or multipath loops, the complexity has not yet been determined. We show that both problems are coNP-complete. However, we point out some special cases of importance of PTIME complexity. We also present complete algorithms for synthesizing linear and lexicographical-linear ranking functions, both for the general case and the special PTIME cases. Moreover, in the rational setting, our algorithm for synthesizing lexicographical-linear ranking functions extends existing ones, because our class of ranking functions is more general, yet it has polynomial time complexity.
Cite
@article{arxiv.1208.4041,
title = {Ranking Functions for Linear-Constraint Loops},
author = {Amir M. Ben-Amram and Samir Genaim},
journal= {arXiv preprint arXiv:1208.4041},
year = {2025}
}
Comments
This version explains (in the new Lemma 5.31) how the procedure of Lemma 5.29 can be implemented in polynomial time. This new lemma does not appear in the JACM version of this paper