Vortragsankündigung:


Weighted Tree Automata for Termination of Term Rewriting

Adam Koprowski (TU Eindhoven), http://www.win.tue.nl/~akoprows/
Johannes Waldmann (HTWK Leipzig), http://www.imn.htwk-leipzig.de/~waldmann/


Ein Ersetzungssystem terminiert, 
wenn es keine unendlich langen Berechnungen gestattet.
Wir interessieren uns für maschinelle Terminationsbeweise.

Ein wichtiges Beweisverfahren ist Interpretation
in eine monotone Algebra. Wir betrachten Interpretationen
durch gewichtete Baumautomaten. Als Gewichte verwenden wir
(a) natürliche Zahlen N mit Standard-Operationen (plus, mal),
(b) den arktischen Halbring (-infinity + N) mit (max, plus),
(c) den vollen arktischen Halbring (-infinity + Z).

Die Verfahren (a) und (b - bisher nur für Wortsersetzung) 
werden seit 2006 bzw. 2007 von mehreren erfolgreichen Teilnehmern 
der Termination Competitions 
http://www.lri.fr/~marche/termination-competition/  benutzt;
die Erweiterung von (b) für Termersetzung und (c) sind neu.

Im Vortrag diskutieren wir 
Korrektheit, Implementierung und formale Verifikation
sowie eine Verbindung zum Beschränktheitsproblem
für tropische (min,plus) Automaten.


Literatur:

Jörg Endrullis, Johannes Waldmann and Hans Zantema:
Matrix Interpretations for Proving Termination of Term Rewriting;
IJCAR 2006, JAR 2007.

Adam Koprowski and Hans Zantema:
Certification of Proving Termination of Term Rewriting 
by Matrix Interpretations;
SOFSEM 2008.

Johannes Waldmann: 
Weighted Automata for Proving Termination of String Rewriting;
WATA 2006, JALC 2007.