Termination of cycle rewriting by transformation and matrix interpretation
From MaRDI portal
Publication:2980975
Abstract: We present techniques to prove termination of cycle rewriting, that is, string rewriting on cycles, which are strings in which the start and end are connected. Our main technique is to transform cycle rewriting into string rewriting and then apply state of the art techniques to prove termination of the string rewrite system. We present three such transformations, and prove for all of them that they are sound and complete. In this way not only termination of string rewriting of the transformed system implies termination of the original cycle rewrite system, a similar conclusion can be drawn for non-termination. Apart from this transformational approach, we present a uniform framework of matrix interpretations, covering most of the earlier approaches to automatically proving termination of cycle rewriting. All our techniques serve both for proving termination and relative termination. We present several experiments showing the power of our techniques.
Recommendations
Cites work
- scientific article; zbMATH DE number 4072419 (Why is no real title available?)
- scientific article; zbMATH DE number 2043538 (Why is no real title available?)
- Arctic Termination ...Below Zero
- Levels of undecidability in rewriting
- Matrix interpretations for proving termination of term rewriting
- Proving non-termination by finite automata
- Proving termination of graph transformation systems using weighted type graphs over semirings
- Proving termination of programs automatically with AProVE
- Termination Competition (termCOMP 2015)
- Termination analysis for graph transformation systems
- Termination of String Rewriting with Matrix Interpretations
- Termination of \(\{aa\rightarrow bc,bb\rightarrow ac,cc\rightarrow ab\}\)
- Termination of cycle rewriting
- Termination of term rewriting: Interpretation and type elimination
- Transformation techniques for context-sensitive rewrite systems
- Transforming SAT into termination of rewriting
- Transforming cycle rewriting into string rewriting
Cited in
(7)- An automated approach to the Collatz conjecture
- Transforming cycle rewriting into string rewriting
- Weighted automata define a hierarchy of terminating string rewriting systems
- Termination of cycle rewriting
- Termination of graph transformation systems using weighted subgraph counting
- Termination of String Rewriting with Matrix Interpretations
- Termination by Quasi-periodic Interpretations
This page was built for publication: Termination of cycle rewriting by transformation and matrix interpretation
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2980975)
