On multiphase-linear ranking functions

DOI10.1007/978-3-319-63390-9_32zbMATH Open1494.68049arXiv1703.07547OpenAlexW2605065382MaRDI QIDQ2164261FDOQ2164261

Authors: Amir M. Ben-Amram, Samir Genaim 

Publication date: 12 August 2022

Abstract: Multiphase ranking functions ($mathitMPhiRFs$) were proposed as a means to prove the termination of a loop in which the computation progresses through a number of "phases", and the progress of each phase is described by a different linear ranking function. Our work provides new insights regarding such functions for loops described by a conjunction of linear constraints (single-path loops). We provide a complete polynomial-time solution to the problem of existence and of synthesis of $mathitMPhiRF$ of bounded depth (number of phases), when variables range over rational or real numbers; a complete solution for the (harder) case that variables are integer, with a matching lower-bound proof, showing that the problem is coNP-complete; and a new theorem which bounds the number of iterations for loops with $mathitMPhiRFs$. Surprisingly, the bound is linear, even when the variables involved change in non-linear way. We also consider a type of lexicographic ranking functions, $mathitLLRFs$, more expressive than types of lexicographic functions for which complete solutions have been given so far. We prove that for the above type of loops, lexicographic functions can be reduced to $mathitMPhiRFs$, and thus the questions of complexity of detection and synthesis, and of resulting iteration bounds, are also answered for this class.

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

Recommendations

• Ranking functions for linear-constraint loops
• On the \textsc{Linear Ranking} problem for integer linear-constraint loops
• Computer Aided Verification
• Complexity of Bradley-Manna-Sipma lexicographic ranking functions
• Automata, Languages and Programming

Mathematics Subject Classification ID

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

Cited In (19)

• Control-flow refinement by partial evaluation, and its application to termination and cost analysis
• Title not available (Why is that?)
• Inferring expected runtimes of probabilistic integer programs using expected sizes
• Automatic complexity analysis of integer programs via triangular weakly non-linear loops
• Decision tree learning in CEGIS-based termination analysis
• Reflections on termination of linear loops
• Algebraic model checking for discrete linear dynamical systems
• A new look at the automatic synthesis of linear ranking functions
• Ranking functions for linear-constraint loops
• Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs
• Title not available (Why is that?)
• Title not available (Why is that?)
• Termination analysis of programs with multiphase control-flow
• Targeting Completeness: Using Closed Forms for Size Bounds of Integer Programs
• Complexity of Bradley-Manna-Sipma lexicographic ranking functions
• What's decidable about discrete linear dynamical systems?
• Multiphase-linear ranking functions and their relation to recurrent sets
• Synthesizing ranking functions for loop programs via SVM
• Title not available (Why is that?)

This page was built for publication: On multiphase-linear ranking functions

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