Termination Analysis by Tree Automata Completion

Martin Korp

PhD thesis, University of Innsbruck, 2010.


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-ound 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.




author = "Martin Korp",
title = "Termination Analysis by Tree Automata Completion",
school = "University of Innsbruck",
year = 2010
Nach oben scrollen