[Termtools] Remarks on the Termination Competition

[Juergen Giesl]

Dear all,

> Now what to do? Should TTT2 be removed from the TRS table since
> correctness is not guaranteed? We wonder though what message that
> conveys. Only three participants in the TRS category? AProVE against
> a weak version of Jambox (due to unclear time limits?) and a tool
> (NTI) that "only" aims to disprove termination?

I think that this year's termination competition suffered from 2 problems:

1. The time limits were unclear and didn't correspond to what was
    discussed before. It seems that most participants assumed that the time limit
    would be 60 seconds wall-clock-time, but it turned out that
    a different time limit of 120 seconds user-time was used.

2. There were many tools where bugs were discovered during the competition.

Concerning buggy tools, I don't think that disqualification is
the right idea. After all, the tools that are not disqualified are not
at all guaranteed to be bug-free. They were probably just lucky. Indeed,
for several of the successful tools in the 2006-competition, bugs were
discovered afterwards.

I think that a main goal of the competition is to demonstrate the
state-of-the-art in termination proving. As it is now (and even more if
TTT2 would be disqualified), the impression that one gets from the webpages
of the competition is that almost nobody is working on TRS-termination anymore
and that the only really active research area is SRS-termination.
I am not happy with giving this impression.

After all, this "competition" is not really concerned with money or anything like
that, and we should not behave like competitors, but like colleagues. Therefore,
my proposal would be the following:

- Give all tools with known bugs the chance to repair these bugs. We would trust
   the tool authors that they only perform bug fixes and will not tune their tools further.
   One should impose a deadline for the submission of the repaired tools
   (e.g., beginning of next week).

- Then re-run the competition with all tools (including the fixed ones),
   but with the time limit that was assumed by the participants
   (60 seconds wall-clock time, not user time).

This should enable the tools with bugs as well as Jambox (who suffered
most from the modified time limit) to participate in the competition in a sensible way.
Re-running the competition would then still be finished in time for RDP.

Best Regards
Juergen