Ranking Templates for Linear Loops

DOI10.2168/LMCS-11(1:16)2015MaRDI QIDQ5246721zbMATH OpenOpenAlexFDO

Authors Jan Leike, Matthias Heizmann

Publication date 22 April 2015

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1503.00193

zbMATH Keywords

Farkas' lemmalexicographic ranking functionlinear lasso programlinear loop programlinear ranking templateMotzkin's theoremmultiphase ranking functionnested ranking functionparallel ranking functionpiecewise ranking functionterminationwell-founded relation

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

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 $existsforall$-constraint into an $exists$-constraint.

Recommendations

• Ranking functions for linear-constraint loops
• On the linear ranking problem for simple floating-point loops
• Template matching with ranks
• Computer Aided Verification
• scientific article; zbMATH DE number 3882490
• Linear-Time Ranking of Permutations
• scientific article; zbMATH DE number 1701751
• On the \textsc{Linear Ranking} problem for integer linear-constraint loops
• Rank aggregation in cyclic sequences

Cited in

(14)

• Synthesizing ranking functions for loop programs via SVM
• Automatic complexity analysis of integer programs via triangular weakly non-linear loops
• \textsc{LTL} falsification in infinite-state systems
• Automatic discovery of fair paths in infinite-state transition systems
• Termination of polynomial loops
• Proving termination through conditional termination
• Linear ranking for linear lasso programs
• Multiphase-linear ranking functions and their relation to recurrent sets
• Termination analysis of programs with multiphase control-flow
• Termination of triangular polynomial loops
• Polynomial loops: beyond termination
• Targeting completeness: automated complexity analysis of integer programs
• Constraint-based relational verification
• Reflections on termination of linear loops

This page was built for publication: Ranking Templates for Linear Loops

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5246721)