Ranking Functions for Linear-Constraint Loops

TL;DR

This paper investigates the complexity of finding linear or lexicographical-linear ranking functions for linear-constraint loops, establishing coNP-completeness over integers and providing algorithms for synthesis in various cases.

Contribution

It proves the coNP-completeness of ranking function existence over integers and offers complete algorithms for synthesizing these functions, including extensions for the rational case.

Findings

Ranking function problems are coNP-complete over integers.

Polynomial-time algorithms exist for special cases.

Extended algorithms for rational ranking functions are more general and efficient.

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.