Termination of Cycle Rewriting by Transformation and Matrix Interpretation

We present techniques to prove termination of cycle rewriting, that is,string rewriting on cycles, which are strings in which the start and end areconnected. Our main technique is to transform cycle rewriting into stringrewriting and then apply state of the art techniques to prove termination ofthe string rewrite system. We present three such transformations, and prove forall of them that they are sound and complete. In this way not only terminationof string rewriting of the transformed system implies termination of theoriginal cycle rewrite system, a similar conclusion can be drawn fornon-termination. Apart from this transformational approach, we present auniform framework of matrix interpretations, covering most of the earlierapproaches to automatically proving termination of cycle rewriting. All ourtechniques serve both for proving termination and relative termination. Wepresent several experiments showing the power of our techniques.Comment: 38 pages, 1 figur