Checking and Bounding the Solutions of Some Recurrence Relations (TR)

Roberto Bagnara and Alessandro Zaccagnini


Recurrence relations play an important role in the field of complexity analysis since complexity measures can often be elegantly expressed by systems of such relations. This justifies the interest in automatic, precise, efficient and correct systems able to solve or to approximate the solution of systems of recurrence relations. Assume such a system is built. Since closed-form solutions for recurrences of even modest complexity can be so big and complex to be unmanageable, how can confidence on such a system be gained? How can we quickly validate or perhaps disprove its results? And, in those cases where the exact solution is too complex to be of practical use, how can we trade precision for efficiency by approximating them from below and from above? We also concern ourselves with a problem related to the handling of sets of solutions of recurrence relations: how can we confine by means of a lower bound and an upper bound a set of such solutions? We provide some solutions to these problems where we are careful to rely, whenever possible, on fast integer computations and/or conditions that are easy to check in a completely automatic way. The ongoing experimental evaluation of these ideas is giving very promising results, showing order-of-magnitude speedups over the more traditional methods.

Available: PDF, 300 DPI, 600 DPI, and 1200 DPI PostScript, DVI, and BibTeX entry.

[Page last updated on January 09, 2004, 21:44:21.]

Page maintained by
Enea Zaffanella

Home | People | Projects | Publications | Seminars | Software | Links