Complexity of Bradley-Manna-Sipma lexicographic ranking functions

DOI10.1007/978-3-319-21668-3_18MaRDI QIDQ1702898zbMATH OpenOpenAlexFDO

Authors Amir M. Ben-Amram, Samir Genaim

Publication date 1 March 2018

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

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Analysis of algorithms and problem complexity (68Q25)

Abstract: In this paper we turn the spotlight on a class of lexicographic ranking functions introduced by Bradley, Manna and Sipma in a seminal CAV 2005 paper, and establish for the first time the complexity of some problems involving the inference of such functions for linear-constraint loops (without precondition). We show that finding such a function, if one exists, can be done in polynomial time in a way which is sound and complete when the variables range over the rationals (or reals). We show that when variables range over the integers, the problem is harder -- deciding the existence of a ranking function is coNP-complete. Next, we study the problem of minimizing the number of components in the ranking function (a.k.a. the dimension). This number is interesting in contexts like computing iteration bounds and loop parallelization. Surprisingly, and unlike the situation for some other classes of lexicographic ranking functions, we find that even deciding whether a two-component ranking function exists is harder than the unrestricted problem: NP-complete over the rationals and $Sigm{a}_2^P$-complete over the integers.

Recommendations

• Ranking functions for linear-constraint loops
• On the \textsc{Linear Ranking} problem for integer linear-constraint loops
• The hardness of finding linear ranking functions for lasso programs
• On multiphase-linear ranking functions
• Automata, Languages and Programming

Cited in

(8)

• On multiphase-linear ranking functions
• On the \textsc{Linear Ranking} problem for integer linear-constraint loops
• The hardness of finding linear ranking functions for lasso programs
• scientific article; zbMATH DE number 7559471 (Why is no real title available?)
• Ranking functions for linear-constraint loops
• On Lexicographic Proof Rules for Probabilistic Termination
• On lexicographic proof rules for probabilistic termination
• Termination analysis of programs with multiphase control-flow

This page was built for publication: Complexity of Bradley-Manna-Sipma lexicographic ranking functions

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