Non-polynomial worst-case analysis of recursive programs

DOI10.1007/978-3-319-63390-9_3MaRDI QIDQ2164209zbMATH OpenOpenAlexFDO

Authors Krishnendu Chatterjee, Hongfei Fu, Amir Kafshdar Goharshady

Publication date 12 August 2022

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

zbMATH Keywords

recursive programsworst-case boundFLO11 expressiontemplate variablestriple constraint

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Analysis of algorithms (68W40) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Abstract: We study the problem of developing efficient approaches for proving worst-case bounds of non-deterministic recursive programs. Ranking functions are sound and complete for proving termination and worst-case bounds of nonrecursive programs. First, we apply ranking functions to recursion, resulting in measure functions. We show that measure functions provide a sound and complete approach to prove worst-case bounds of non-deterministic recursive programs. Our second contribution is the synthesis of measure functions in nonpolynomial forms. We show that non-polynomial measure functions with logarithm and exponentiation can be synthesized through abstraction of logarithmic or exponentiation terms, Farkas' Lemma, and Handelman's Theorem using linear programming. While previous methods obtain worst-case polynomial bounds, our approach can synthesize bounds of the form $mathcalO(nlogn)$ as well as $mathcalO(n^r)$ where $r$ is not an integer. We present experimental results to demonstrate that our approach can obtain efficiently worst-case bounds of classical recursive algorithms such as (i) Merge-Sort, the divide-and-conquer algorithm for the Closest-Pair problem, where we obtain $mathcalO(nlogn)$ worst-case bound, and (ii) Karatsuba's algorithm for polynomial multiplication and Strassen's algorithm for matrix multiplication, where we obtain $mathcalO(n^r)$ bound such that $r$ is not an integer and close to the best-known bounds for the respective algorithms.

Recommendations

• Recursion Schemes and Recursive Programs are Exponentially Hard to Analyze
• Synthesis with asymptotic resource bounds
• Quasiconvex analysis of multivariate recurrence equations for backtracking algorithms
• Quasiconvex analysis of backtracking algorithms
• Automated recurrence analysis for almost-linear expected-runtime bounds

Cited in

(13)

• Time-bounded termination analysis for probabilistic programs with delays
• ATLAS: automated amortised complexity analysis of self-adjusting data structures
• Synthesis with asymptotic resource bounds
• Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic Programs
• Runtime complexity analysis of logically constrained rewriting
• Worst Case Branching and Other Measures of Nondeterminism
• What else is undecidable about loops?
• Recursion Schemes and Recursive Programs are Exponentially Hard to Analyze
• Affine Loop Invariant Generation via Matrix Algebra
• Beyond the Worst-Case Analysis of Algorithms
• MDPs as distribution transformers: affine invariant synthesis for safety objectives
• Deciding fast termination for probabilistic VASS with nondeterminism
• Type-based analysis of logarithmic amortised complexity

This page was built for publication: Non-polynomial worst-case analysis of recursive programs

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