The use of automata techniques to prove the termination of string rewrite
systems and left-linear term rewrite systems is advocated by Geser
et al. in a recent sequence of papers. We extend their work to
non-left-linear rewrite systems. The key to this extension is the
introduction of so-called raise rules and the use of tree automata that
are not quite deterministic. Furthermore, to increase the applicability of
the method we show how it can be incorporated into the dependency pair
framework. To achieve this we introduce two new enrichments which take
the special properties of dependency pair problems into account.

@article{KM09c,
  author      = "Martin Korp and Aart Middeldorp",
  title       = "Match-Bounds Revisited",
  journal     = "Information and Computation",
  volume      = 207,
  number      = 11,
  pages       = "1259--1283",
  year        = 2009}

In this paper we introduce a modular framework which allows to infer
(feasible) upper bounds on the (derivational) complexity of term rewrite
systems by combining different criteria. All current investigations to
analyze the derivational complexity are based on a single termination
proof, possibly preceded by transformations. We prove that the modular
framework is strictly more powerful than the conventional setting.
Furthermore, the results have been implemented and experiments show
significant gains in power.

@inproceedings{ZK10a,
  author      = "Harald Zankl and Martin Korp",
  title       = "Modular Complexity Analysis via Relative Complexity",
  booktitle   = "Proceedings of the 21st International Conference on
                 Rewriting Techniques and Applications (RTA)",
  address     = "Edinburgh",
  series      = "Leibnitz International Proceedings in Informatics",
  publisher   = "Schloss Dagstuhl",
  volume      = 6
  pages       = "385--400",
  year        = 2010}

This paper describes the second edition of the Tyrolean Termination
Tool--a fully automatic termination analyzer for first-order term
rewrite systems. The main features of this tool are its
(non-)termination proving power, its speed, its flexibility due to
a strategy language, and the fact that the source code of the whole
project is freely available. The clean design together with a
stand-alone OCaml library for term rewriting, make it a perfect
starting point for other tools concerned with rewriting as well as
experimental implementations of new termination methods.

@inproceedings{KSZM09,
  author      = "Martin Korp, Christian Sternagel, Harald Zankl and Aart Middeldorp",
  title       = "Tyrolean Termination Tool 2",
  booktitle   = "Proceedings of the 20th International Conference on
                 Rewriting Techniques and Applications (RTA)",
  address     = "Brazilia",
  series      = "Lecture Notes in Computer Science",
  publisher   = "Springer-Verlag",
  volume      = 5595,
  pages       = "295--304",
  year        = 2009}

The use of automata techniques to prove the termination of string rewrite
systems and left-linear term rewrite systems is advocated by Geser
et al. in a recent sequence of papers. We extend their work to
non-left-linear rewrite systems. The key to this extension is the
introduction of so-called raise rules and the use of tree automata that
are not quite deterministic. Furthermore, we present negative solutions
to two open problems related to string rewrite systems.

@inproceedings{KM07,
  author      = "Martin Korp and Aart Middeldorp",
  title       = "Proving Termination of Rewrite Systems using Bounds",
  booktitle   = "Proceedings of the 18th International Conference on
                 Rewriting Techniques and Applications (RTA)",
  address     = "Paris",
  series      = "Lecture Notes in Computer Science",
  publisher   = "Springer-Verlag",
  volume      = 4533,
  pages       = "273--287",
  year        = 2007}

The dependency pair framework is a powerful technique for proving
termination of rewrite systems. One of the most frequently used methods
within the dependency pair framework is the dependency graph processor.
In this note we improve this processor by incorporating right-hand sides
of forward closures. In combination with tree automata completion we obtain
an effective processor which can be used instead of the dependency graph
approximations that are in common use in termination provers.

@inproceedings{KM09a,
  author      = "Martin Korp and Aart Middeldorp",
  title       = "Beyond Dependency Graphs",
  booktitle   = "Proceedings of the 10th International Workshop on
                 Termination (WST)",
  address     = "Leipzig",
  pages       = "52--55",
  year        = 2009}

Establishing termination of programs and processes is one of the most
fundamental problems in computer science. In the area of term rewriting,
a Turing-complete model of computation which forms the theoretical basis
of functional programming, termination has been studied for several decades.
Although termination is undecidable in general, many powerful termination
criteria have been developed. In this dissertation we focus on methods that
uses automata techniques, especially tree automata completion,
to automatically prove the termination of rewrite systems. 

A relatively new and elegant method within this scope is the so called
match-bound technique proposed by Geser, Hofbauer, and Waldmann.
It uses tree automata completion to prove the termination of
rewrite systems. In this thesis we extend the match-bound technique in
three directions. The first extension is the removal of the left-linearity
restriction to increase the applicability of the method. The second extension
is the integration of the match-bound technique into the dependency pair
framework, a powerful framework to automatically prove the termination of
rewrite systems. The third extension discusses how the match-bound technique
can be used for modular complexity analysis.

Another termination technique that can benefit from the use of automata
techniques is the so called dependency graph processor, which is
one of the most frequently used techniques within the dependency pair
framework. We illustrate that by using tree automata completion tremendous
gains in power can be achieved.

The developed techniques have been integrated into the tool TTT2, a fully
automatic termination analyzer for first-order term rewrite systems, as well
as the complexity analyzer CaT.

@phdthesis{K10,
  author      = "Martin Korp",
  title       = "Termination Analysis by Tree Automata Completion",
  school      = "University of Innsbruck",
  year        = 2010}