This page is no longer maintained

TCT is a tool for automatically proving (low) upper bounds on the derivational complexity and runtime complexity of terminating term rewriting systems. It is strongly based on the automatic termination prover TTT2.


The following files are available for download: For an installation instruction, please revice the file INSTALLATION in the root directory of the source package. The current version was updated last on Thu Feb 5 09:30:25 CET 2009 .


The usage of TCT is essentially the same as the usage of TTT2. It is called by ./tct [options] <file>. Most options which were allowed in TTT2 are also included in TCT (type ./tct --help for a complete list of the currently available options). For an explanation of these options, we refer to TTT2. The first new option added by TCT is --answer_type <answertype> (or -a <answertype>). This option controls what TCT prints in the first line of its output: allowed values for <answertype> are plain (just print YES or MAYBE), dc, rc, idc, and irc (add an upper bound on the (innermost) derivational or runtime complexity to a YES). The second new option is -v (or --version), which just prints the current version number, and then exits TCT.

Of the options inherited from TTT2, the option --strategy (respectively, -s) deserves special mentioning. This option takes as argument a string describing the strategy that TCT should use in order to attempt to prove termination and complexity bounds of the given TRS. For a description of the grammar for this argument string (the strategy language), we refer to TTT2 (ttt2-doc, Section "Module Strategy"). A list of atomic strategies in TCT is available. Here are some sample calls of TCT: Here is another sample strategy for TCT: For simplifying the usage of strategies, the file tct.conf in the subfolder tct/tests contains many complexity-specific strategy macros. Still, it is subject to further extension.

Experimental Results for the standard strategies of TCT

Note: due to an error in Lemma 22 of of the IJCAR 2008 paper by Hirokawa and Moser, the applicability of Corollaries 35 and 36 of that paper is reduced, which makes some of TCT's results in the Termination Competition unsound. The following table contains the result of our competition strategy, after considering the implications of that error:
Experimental Results
status DC DC innermost RC RC innermost
YES 225 226 271 304
total time 318.99 389.32 671.02 945.42
avg. time 1.42 1.72 2.48 3.11
MAYBE 0 948 515 757
total time 0.00 51.93 5241.34 21224.76
avg. time 0.00 0.05 10.28 28.22
TIMEOUT 221 220 608 333
total time 16553.45 16900.81 36959.21 19985.78
avg. time 74.90 76.82 60.79 60.02
(tables created with a modified version of a privately communicated script by Nao Hirokawa)
Note that the testbed we used here was a little bit smaller than the testbed used in this year's complexity competition: we filtered the TPDB for duplicate systems. A detailed overview on experimental results can be found here.