Ranking functions for linear-constraint loops
From MaRDI portal
Publication:5501930
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.
Recommendations
Cites work
- A LIBRARY FOR DOING POLYHEDRAL OPERATIONS
- A new look at the automatic synthesis of linear ranking functions
- A Strongly Polynomial Algorithm to Solve Combinatorial Linear Programs
- Alternation for termination
- An Improved Tight Closure Algorithm for Integer Octagonal Constraints
- Automatic numeric abstractions for heap-manipulating programs
- Closed-form upper bounds in static cost analysis
- Computer Aided Verification
- Computing Two-Dimensional Integer Hulls
- CONCUR 2005 – Concurrency Theory
- Cost analysis of object-oriented bytecode programs
- scientific article; zbMATH DE number 1701751 (Why is no real title available?)
- scientific article; zbMATH DE number 4089320 (Why is no real title available?)
- scientific article; zbMATH DE number 3639144 (Why is no real title available?)
- scientific article; zbMATH DE number 1903370 (Why is no real title available?)
- Linear ranking for linear lasso programs
- Logic Programming
- Loop Summarization and Termination Analysis
- Monotonicity constraints for termination in the integer domain
- Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs
- On Linear Characterizations of Combinatorial Optimization Problems
- On the \textsc{Linear Ranking} problem for integer linear-constraint loops
- On the termination of integer loops
- Ramsey versus lexicographic termination proving
- Ranking function synthesis for bit-vector relations
- Recurrence with affine level mappings is P-time decidable for CLP
- Some efficient solutions to the affine scheduling problem. I: One- dimensional time
- Some efficient solutions to the affine scheduling problem. II: Multidimensional time
- Termination of Integer Linear Programs
- The size-change principle for program termination
- Transition invariants and transition predicate abstraction for program termination
- Verification of gap-order constraint abstractions of counter systems
- Verification, Model Checking, and Abstract Interpretation
- Verification, Model Checking, and Abstract Interpretation
Cited in
(28)- A linear time randomizing algorithm for searching ranked functions
- On the linear ranking problem for simple floating-point loops
- Complexity of Bradley-Manna-Sipma lexicographic ranking functions
- Inferring expected runtimes of probabilistic integer programs using expected sizes
- Synthesizing ranking functions for loop programs via SVM
- Algebraic model checking for discrete linear dynamical systems
- How to find the convex hull of all integer points in a polyhedron?
- On multiphase-linear ranking functions
- Time-bounded termination analysis for probabilistic programs with delays
- On the \textsc{Linear Ranking} problem for integer linear-constraint loops
- Termination of single-path polynomial loop programs
- The hardness of finding linear ranking functions for lasso programs
- scientific article; zbMATH DE number 7559471 (Why is no real title available?)
- Termination of linear loops over the integers
- Control-flow refinement by partial evaluation, and its application to termination and cost analysis
- Tight polynomial worst-case bounds for loop programs
- Ranking Templates for Linear Loops
- Computer Aided Verification
- Termination of linear loops under commutative updates
- What's decidable about discrete linear dynamical systems?
- Multiphase-linear ranking functions and their relation to recurrent sets
- Termination analysis of programs with multiphase control-flow
- The 2-dimensional constraint loop problem is decidable
- T-rex: termination of recursive functions using lexicographic linear combinations
- Termination of triangular polynomial loops
- Targeting completeness: automated complexity analysis of integer programs
- On termination of polynomial programs with equality conditions
- Decision tree learning in CEGIS-based termination analysis
This page was built for publication: Ranking functions for linear-constraint loops
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5501930)
