Competition 2005 of termination tools

C. Marché and H. Zantema

March 2, 2005

1  Overview of the event

In April 2005, the third termination competition will be run.

The competition will be a completely automatic process that will be run without user interaction. During this competition, a large set of termination problems, mainly extracted from the termination problem database (TPDB), will be considered, and each of these problems will be submitted to each tool willing to participate. Given a termination problem, each tool is supposed to answer whether the given system/program is terminating. Each tool must run without any user interaction.

The precise rules of the competition are detailed in the next section. Those who are willing to participate should register to the mailing dedicated to the competition, by sending a mail at
subscribe termtools
in the body of the message.

2  Rules of the competition

A tool participating to the competition will be evaluated by a completely automatic process. There will be three categories: term rewrite systems, string rewrite systems, and logic programs. A tool may participate to any number of categories.

The tool must be available as an executable that takes as argument the name of a file describing a termination problem. The tool must run without any user interaction, and the answer must finally be printed on standard output.

For the term or string rewrite system category, the input file will be in the common format of the TPDB, available as a separate document. The answer must start by either YES or NO, meaning that the given rewrite system is terminating (respectively, not terminating) under the STRATEGY given in the input file. If there is no strategy annotation, strong termination is taken as the default. This text YES or NO should be followed by a proof or proof sketch in English of the claimed result.

Any output not starting by YES or NO is considered as DON'T KNOW. For every termination problem the maximal CPU time allowed is defined to be 60 seconds. If a tool is still running when this maximal CPU time is reached, its process will be killed.

For the logic program category, the input file will be a Prolog program in a standard syntax as in the TPDB. Additionally, in the command line will be given an input query, of the form id(x1,...,xn) where each xi is either i or o. The tool should answer whether the given program terminates on every query with that moding.

If it appears that for some termination problem a wrong answer is given, then the tool will be ``disqualified''.

On the web page. a score table will be presented for each category, by giving one point for each (correct) answer. Classifications will be computed for each category, several classifications will be made in the rewriting categories, with respect to strategies. The CPU time used will also be listed in the score table; the generated proofs or proof sketches will be accessible from the web page. There is nothing to win, except of being declared as ``the best automatic termination prover in the world in 2005'' in the given category. The main results of the competition will be reported on the 16th International Conference on Rewriting Techniques and Applications (RTA) , April 19 - 21, 2005, in Nara, Japan.

3  The set of termination problems

The set of termination problems will be mainly extracted from the termination problem database (TPDB) as it is on March 14, 2005. Any one may submit new termination problems for this database until March 11, 2005. Essentially all problems in the database will participate in the competition, only duplicates may be removed.

In order to make the competition more exciting, the set of termination problems used for the competition is extended by a secret list. This secret list is composed from systems that are submitted by the participants just before the competition. More precisely, Every participant may submit at most 5 termination problems for the secret list for every category he participates. Typically, he may try to choose problems that can be solved by his tool while they are expected not to be solvable by the other tools. For the categories of string rewriting and term rewriting the problems should satisfy the following requirements: no more than 10 rules, no more than 10 distinct operation symbols, every lhs and rhs contains no more than 10 operation symbols.

4  Technical details for participants

If you are willing to participate to the competition, here is what you have to do in details: The program must follow this specification:
This document was translated from LATEX by HEVEA.