Ranking Templates for Linear Loops

TL;DR

This paper introduces a flexible, template-based method for synthesizing termination proofs for linear loops, expanding the types of ranking functions that can be automatically generated.

Contribution

It generalizes existing approaches by enabling the use of various affine-linear ranking templates and combining them for more powerful termination arguments.

Findings

Supports multiphase, nested, piecewise, parallel, and lexicographic ranking functions

Uses Motzkin's transposition theorem for constraint transformation

Enhances the automation of termination proofs for linear loops

Abstract

We present a new method for the constraint-based synthesis of termination arguments for linear loop programs based on linear ranking templates. Linear ranking templates are parameterized, well-founded relations such that an assignment to the parameters gives rise to a ranking function. Our approach generalizes existing methods and enables us to use templates for many different ranking functions with affine-linear components. We discuss templates for multiphase, nested, piecewise, parallel, and lexicographic ranking functions. These ranking templates can be combined to form more powerful templates. Because these ranking templates require both strict and non-strict inequalities, we use Motzkin's transposition theorem instead of Farkas' lemma to transform the generated $\exists\forall$-constraint into an $\exists$-constraint.