Termination of cycle rewriting by transformation and matrix interpretation
From MaRDI portal
Publication:2980975
DOI10.23638/LMCS-13(1:11)2017zbMATH Open1398.68281arXiv1609.07065OpenAlexW2524395091MaRDI QIDQ2980975FDOQ2980975
Authors: David Sabel, Hans Zantema 
Publication date: 8 May 2017
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.
Full work available at URL: https://arxiv.org/abs/1609.07065
Recommendations
Cites Work
- Termination of term rewriting: Interpretation and type elimination
- Title not available (Why is that?)
- Matrix interpretations for proving termination of term rewriting
- Termination of \(\{aa\rightarrow bc,bb\rightarrow ac,cc\rightarrow ab\}\)
- Termination of String Rewriting with Matrix Interpretations
- Levels of undecidability in rewriting
- Transformation techniques for context-sensitive rewrite systems
- Arctic Termination ...Below Zero
- Title not available (Why is that?)
- Termination Competition (termCOMP 2015)
- Proving termination of programs automatically with AProVE
- Proving non-termination by finite automata
- Termination of cycle rewriting
- Proving termination of graph transformation systems using weighted type graphs over semirings
- Termination analysis for graph transformation systems
- Transforming cycle rewriting into string rewriting
- Transforming SAT into termination of rewriting
Cited In (7)
- Termination by Quasi-periodic Interpretations
- Transforming cycle rewriting into string rewriting
- An automated approach to the Collatz conjecture
- Termination of String Rewriting with Matrix Interpretations
- Weighted automata define a hierarchy of terminating string rewriting systems
- Termination of graph transformation systems using weighted subgraph counting
- Termination of cycle rewriting
Uses Software
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)
