[Termtools] TTT2 report

[Martin Johann Korp]

Dear all,

Here is a short report on the performance of TTT2 at the recent
termination competition. TTT2 participated in two categories, SRS
standard and TRS standard, with two aims:

(1) to win the SRS category
(2) to have a very fast but still powerful tool for the TRS category

Johannes already remarked that arctic matrices play an important role in
(1). TTT2 uses fewer techniques than AProVE, but we use matrices with
higher dimensions.

We are not sure about the outcome, if the best SRS tools of 2007
(Matchbox and TORPA) would have participated.

Concerning (2), we wanted to demonstrate that there is no need for a 60
seconds timeout. Running TTT2 at full power would have brought additional
TRSs, but still far short of AProVE's score.  We believe that some
measures are in order to encourage other tools to participate in the TRS
category.

Inspired by the observation that building a fresh tool (CaT, TCT) on an
existing tool (TTT2) is considerably less work than starting from
scratch, one contribution we can (and will) do is to clean up the TTT2
source and make it publicly available.

Greetings from Innsbruck,
  TTT2