Weighted Automata for Proving Termination of String Rewriting
Johannes Waldmann · Universitätsbibliothek Gießen · 2007
We use weighted finite automata to automatically prove termination of string rewriting. The general scheme is to use a well-founded monotone algebra, constructed from the automaton. The ordering of the algebra depends on the strictness properties of the operations in the weight semi-ring. We obtain a unified treatment of the previously known matrix method and match bound method, where we use (plus, times) and (min,max), respectively, as weights. We obtain a new powerful termination method when choosing (min, plus). Our approach also handles relative termination.