Empirical Evaluation of "Maximal Termination"

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:
  1. 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.
  2. 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:

The table below contains the 15 additional examples that can now be handled by AProVE due to the use of "max" and "min", whereas AProVE failed on them in the termination competition 2007. Since AProVE was already the most powerful termination tool for TRSs in this competition, this clearly demonstrates that our new contribution considerably advances the state of the art in termination proving. Please click on any example to load it into the AProVE web interface or on the indicated runtime to view the proof. You can also view the full table which compares the performance of the new AProVE-version with the AProVE-version from the termination competition 2007 on all 1358 examples of the TPDB.  

ExampleAProVE 07AProVE MAX
KILLED60.00YES3.56
KILLED60.00YES4.33
KILLED60.00YES4.28
KILLED60.00YES3.61
KILLED60.00YES4.22
KILLED60.00YES3.42
KILLED60.00YES4.12
KILLED60.00YES5.09
KILLED60.00YES5.10
KILLED60.00YES8.29
KILLED60.00YES2.59
KILLED60.00YES2.72
KILLED60.00YES2.98
KILLED60.00YES3.63
KILLED60.00YES1.80