Most methods and tools for termination analysis of term rewrite systems (TRSs) essentially
try to find arguments of functions that decrease in recursive calls.
However, they fail if the reason for termination is that an argument is
increased in recursive calls repeatedly until it reaches a bound.
In the paper "Proving Termination by Bounded Increase",
we solve that problem and present a method to prove termination of TRSs with
bounded increase automatically.
In our experiments, we want to assess the power of our new termination method
by running it on prototypical examples for bounded increase. We also show
that these examples cannot be handled by any of the tools in the
International Competition of Termination Tools 2006.
Implementation in AProVE
We integrated our approach in the
termination tool AProVE. A
special version of AProVE that allows to repeat the experiments
below can be accessed via a special web
interface.
Tools
In our experiments we use two versions of AProVE (with and without our
new method) as well as all other tools that took part in the
International Competition of Termination Tools 2006:
- APROVE Increasing:
Our new method yields constraints over integer polynomials. These are encoded
into propositional SAT problems (cf. SAT Solving for Termination Analysis with Polynomial Interpretations)
which, in turn, are solved by the SAT solver MiniSAT.
- AProVE WST06
The 2006 competition version of our AProVE tool.
- CiME 2.0.4:
The 2006 competition version of the CiME tool from Paris.
- Jambox 2.0e:
The 2006 competition version of the Jambox tool from Amsterdam.
- Matchbox/SatELite:
The 2006 competition version of the Matchbox from Leipzig.
- MU-TERM 4.3:
The 2006 competition version of the MU-TERM from Valencia.
- TEPARLA:
The 2006 competition version of the TEPARLA from Eindhoven.
- TPA:
The 2006 competition version of the TPA tool from Eindhoven.
- TTTbox:
The 2006 competition version of the TTTbox tool from Innsbruck.
Examples and Settings
In our experiments, we tested the tools on the 17 prototypical examples for
bounded increase from the appendix of the paper "Proving Termination by Bounded Increase". These examples include the challenge example posed at
last years termination competition. They also include examples
with non-boolean (possibly nested) functions in the bound,
examples with combinations of bounds, examples containing increasing
or decreasing defined symbols, examples with bounds on lists,
examples with different increases in different arguments, increasing
TRSs that go beyond the shape of functional programs, etc.
We use all tools in their fully automated competition version (thus, they
require no manual settings).
The AProVE version containing our new contribution
applies the same strategy as the AProVE version used in the competition with
only the addition of our new method for bounded increase at a suitable position.
Since Jambox, Teparla, TPA, and TTTbox do not handle examples with an "innermost" strategy, we tried to prove full termination of the examples with these tools.
For our experiments, the tools were run on an AMD 64-bit machine with 2.2 GHz core frequency.
For each example, we imposed a time limit of 60 seconds (corresponding to the way
tools are evaluated in the annual competition).
Experiments
In the following table, each row shows the behavior of the different
tools on one example. The entry "YES" means that innermost termination of that example could
be proved by the corresponding tool while "MAYBE" states that the tool gave up
without success. Finally, "KILLED" indicates that the tool exceeded the given time limit by more than
five seconds and was therefore killed. By clicking on the respective runtime, one can inspect the output produced by the tool. To load an example into our web interface,
just click on the corresponding button in the first column. Then you can run the new version of AProVE on the respective example yourself.
Except for the AProVE version containing our new contributions, none of the tools
is able to solve any of these examples. To determine if the time limit was
an issue for the other tools, we re-ran the experiment with a time limit of
10 minutes. This led to the same results.