Abstract

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.

BibTeX

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