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 parametrized, well-founded relations such that an assignment to the parameters gives rise to a ranking function. This approach generalizes existing methods and enables us to use templates for many different ranking functions with affine-linear components. We discuss templates for multiphase, piecewise, and lexicographic ranking functions. 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 ∃∀-constraint into an ∃-constraint. © 2014 Springer-Verlag.
Cite
CITATION STYLE
Leike, J., & Heizmann, M. (2014). Ranking templates for linear loops. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8413 LNCS, pp. 172–186). Springer Verlag. https://doi.org/10.1007/978-3-642-54862-8_12
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
