article
Non-polynomial worst-case analysis of recursive programs
published
yes
Krishnendu
Chatterjee
author 2E5DCA20-F248-11E8-B48F-1D18A9856A870000-0002-4561-241X
Hongfei
Fu
author
Amir Kafshdar
Goharshady
author 391365CE-F248-11E8-B48F-1D18A9856A870000-0003-1702-6584
KrCh
department
Efficient Algorithms for Computer Aided Verification
project
Rigorous Systems Engineering
project
Quantitative Graph Games: Theory and Applications
project
Quantitative Analysis of Probablistic Systems with a focus on Crypto-currencies
project
Quantitative Game-theoretic Analysis of Blockchain Applications and Smart Contracts
project
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 $\mathcal{O}(n\log n)$
as well as $\mathcal{O}(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
$\mathcal{O}(n \log n)$ worst-case bound, and (ii) Karatsuba's algorithm for
polynomial multiplication and Strassen's algorithm for matrix multiplication,
where we obtain $\mathcal{O}(n^r)$ bound such that $r$ is not an integer and
close to the best-known bounds for the respective algorithms.
ACM2019
eng
ACM Transactions on Programming Languages and Systems
1705.0031710.1145/3339984
414
Chatterjee, Krishnendu, et al. “Non-Polynomial Worst-Case Analysis of Recursive Programs.” <i>ACM Transactions on Programming Languages and Systems</i>, vol. 41, no. 4, 20, ACM, 2019, doi:<a href="https://doi.org/10.1145/3339984">10.1145/3339984</a>.
Chatterjee K, Fu H, Goharshady AK. 2019. Non-polynomial worst-case analysis of recursive programs. ACM Transactions on Programming Languages and Systems. 41(4), 20.
Chatterjee, Krishnendu, Hongfei Fu, and Amir Kafshdar Goharshady. “Non-Polynomial Worst-Case Analysis of Recursive Programs.” <i>ACM Transactions on Programming Languages and Systems</i> 41, no. 4 (2019). <a href="https://doi.org/10.1145/3339984">https://doi.org/10.1145/3339984</a>.
K. Chatterjee, H. Fu, and A. K. Goharshady, “Non-polynomial worst-case analysis of recursive programs,” <i>ACM Transactions on Programming Languages and Systems</i>, vol. 41, no. 4, 2019.
Chatterjee K, Fu H, Goharshady AK. Non-polynomial worst-case analysis of recursive programs. <i>ACM Transactions on Programming Languages and Systems</i>. 2019;41(4). doi:<a href="https://doi.org/10.1145/3339984">10.1145/3339984</a>
K. Chatterjee, H. Fu, A.K. Goharshady, ACM Transactions on Programming Languages and Systems 41 (2019).
Chatterjee, K., Fu, H., & Goharshady, A. K. (2019). Non-polynomial worst-case analysis of recursive programs. <i>ACM Transactions on Programming Languages and Systems</i>, <i>41</i>(4). <a href="https://doi.org/10.1145/3339984">https://doi.org/10.1145/3339984</a>
70142019-11-13T08:33:43Z2020-01-21T13:21:56Z