Polynomial interpretations over the naturals
are one of the most popular techniques for
automated termination analysis, especially in the context of the
dependency pair framework.
In the paper
Maximal Termination,
we present a new approach for
termination proofs that uses polynomial interpretations (with possibly
negative coefficients) together with the "maximum" function.
To obtain a powerful automatic method, we solve two main challenges:
-
So far, using polynomials with negative coefficients for proofs of
full (instead of innermost) termination had a severe drawback: The usable
rules or even all rules of the input TRS had to be oriented by
equality for the termination proof to succeed. Due to this, the
power of this approach was limited.
In our new method, this restriction is dropped.
-
We show how to automate the search for such interpretations
by integrating "maximum" into recent SAT-based methods for
polynomial interpretations. It turns out that
the power of termination analysis is increased significantly
if function symbols may be interpreted
by polynomials that also contain the "maximum" function.
Moreover, this also allows for an efficient automation of the search
for polynomial interpretations with negative coefficients, which up
to now were searched for using trial-and-error methods.
Implementation in AProVE
We have integrated our approach
into the automated termination prover AProVE.
To experiment with this new version of
AProVE, please use the AProVE
web interface.
Examples and Settings
In our experiments below, we want to assess the power of our new method.
Therefore, we tested the new version of AProVE
on the Termination Problem Data Base (TPDB) 4.0.
This is the collection of problems used in the annual International
Termination Competition 2007. We compared the performance of our
new version of AProVE against the version of AProVE that won the
termination competition in 2007.
For our experiments, the tools were run on Dual Intel Xeons at 2.33 GHz.
For each example, we imposed a time limit of 60 seconds (corresponding to the way
tools were evaluated in most of the previous competitions).
As our results indicate, the contributions of
this paper increase the power of AProVE considerably. More precisely,
15 examples from the Termination Problem Data Base that could not be
handled by the previous version of AProVE are now covered. Several of these
examples had not been proved terminating by any tool at the
competitions before. Moreover, AProVE now also succeeds on
all examples from the paper (e.g., Ex. 2, 12, and 13), whereas all
previous tools from the competitions failed (with the exception of TPA
that could already solve Ex. 2). Please click on the following buttons
to load the TRSs from these 3 examples into the web interface: