Termination Competition

Deadlines for 2011 Competition

Competition start: 30 May 2011, 9:00 CEST (9am in Belgrad)
Tool submission: 27 May 2011, 13:01 CEST
Problem submission: 27 May 2011, 13:01 CEST
Software requests: 13 May 2011, 13:01 CEST

TPDB

The Termination Problem Data Base (TPDB) is available as version 8. Programs are mainly available as source, and rewrite systems are represented in an XML-format. A converter is available to transform rewrite systems in the old format to the new XML format. Usage:

java -jar convert.jar someTrs.trs > someTrs.xml 
For the other direction, the following converter can be used. It is invoked as follows:
xsltproc xtc2tpdb.xsl someTrs.xml > someTrs.trs 
This requires that xsltproc is installed. The latter converter can be used by termination tools that do not accept the new XML format.

There also is an archive of example proofs where the aim is to certify these proofs (or detect that they are wrong). This archive consists of all generated proofs from the termination competition 2010 that validate against the schema. All proofs are given in the CPF-format (version 2.1).

New Problems

Please submit new problems for consideration in the TPDB to terminationcompetitionsc<at>lists.rwth-aachen.de with the subject prefixed by "[TPDB SUBMISSION]", before 12:01 CET on 27 May 2011.

Competition Categories

The following categories will be featured in 2011:

Other categories can be considered if enough participants are guaranteed.

Competition Procedure

All participants on the same category will be run on a subset of the existing problems of this category. The number of problems is not fixed and will depend on the number of existing problems. The selection algorithm is described below. The running time for each problem is 60 seconds.

For nearly all categories, the tools will be started in their directory and obtain two parameters, first the problem-file and second, the timeout in seconds. The tools are expected to give an answer (YES, NO, MAYBE) in the first line on stdout, followed by a proof in ASCII, HTML or CPF-format. Exceptions to these rules are listed below (e.g., other answers for certifiers and complexity tools, query for logic programs).

Although string rewriting problems will be considered as a particular case of the term rewrite systems in the TPDB, the string rewrite category will stay in the termination competition.

The certified categories will be run as follows:

  1. After the corresponding uncertified category of the competition has finished, the problems that have been solved (yes or no) are collected and form the initial selection for the certified category.
  2. Termination tools that can produce output in the new format and that participate in the certified competition are then run on the collection of 1, resulting in a collection of termination proofs. (Termination provers may use a different strategy from the uncertified competition, to increase chances of the proof being certified.)
  3. The certifiers are then run on the collection produced by 2.

The more detailed technical description for the certified competition is as follows.

Selection Algorithm

We will fix some number "c" with 0 < c < 1. This number indicates the percentage of problems to be taken from each family. So in principle, we would like to choose c * |F| problems from each family F. Here, |F| is the number of problems in the family F.

In order to avoid problems with very large or very small families, there will be two additional numbers "a" and "b" with 0 < a < b. Here, "a" is the minimum number of examples that should be chosen from each family. Similarly, "b" is the maximum number of examples that should be chosen from each family.

To illustrate this, let c = 1/2 and let a = 10 and b = 100. Then for a family F with 50 problems, we would randomly choose c * |F| = 25 problems from the family F. For a family F with 16 problems, we would not choose c * |F| = 8 problems, because this number would be smaller than a = 10. Instead, we would choose a = 10 problems randomly. For a family with 300 problems, we would not choose c * |F| = 150 problems, because this number would be larger than b = 100. Instead, we would choose b = 100 problems randomly.

To summarize, for every family F, we randomly choose:

    c * |F| problems, if a <= c*|F| <= b
    a       problems, if c*|F| < a           
    b       problems, if b < c*|F|

This rule is applied to every family with the same numbers a,b,c.

The numbers "a", "b" and "c" have been chosen as in the last year: (a = 10, b = 75, c = 0.3).

Use of External Software in Termination Tools.

  1. Standard tools (SAT/SMT solvers) will be installed by the host,
  2. The configuration of the host machine is available.
  3. Requests for changes in the configuration must be submitted two weeks in advance of the competition. (Submit to simon.bailey<at>uibk.ac.at with the subject prefixed by "[TC SOFTWARE]", before 12:01 CET on 13 May 2011.

Contact

To contact the steering committee of the termination competition, send email to terminationcompetitionsc<at>lists.rwth-aachen.de. The competition host can be reached at termcomp<at>informatik.uibk.ac.at.