David Sabel and Hans Zantema.

Termination of cycle rewriting by transformation and matrix interpretation.

*Logical Methods in Computer Science*, Volume 13, Issue 1,
March 2017.

[ bib | DOI | http ]

Termination of cycle rewriting by transformation and matrix interpretation.

[ bib | DOI | http ]

David Sabel and Hans Zantema.

Transforming Cycle Rewriting into String Rewriting.

In Maribel Fernández, editor,*26th International Conference
on Rewriting Techniques and Applications (RTA 2015)*, volume 36 of *
Leibniz International Proceedings in Informatics (LIPIcs)*, pages 285-300,
Dagstuhl, Germany, 2015. Schloss Dagstuhl-Leibniz-Zentrum fuer
Informatik.

[ bib | http | DOI | PDF (extended version) | slides (RTA 2015) ]

Transforming Cycle Rewriting into String Rewriting.

In Maribel Fernández, editor,

[ bib | http | DOI | PDF (extended version) | slides (RTA 2015) ]

David Sabel and Hans Zantema.

TermComp 2016 Partipicant: cycsrs 0.2.

In Aart Middeldorp and René Thiemann, editors,*Proceedings of the 15th International Workshop on Termination*, Obergurgl, Austria, pages 21:1, 2016.

[ http ]

TermComp 2016 Partipicant: cycsrs 0.2.

In Aart Middeldorp and René Thiemann, editors,

[ http ]

Benchmark set |
Time limit |
Description |
Job on StarExec |
Output of job |
Short summary of output |

SRS_Standard | 60 secs. | prove cycle non-/termination by transformation and string termination and by trace-decreasing matrix interpretations | Job | Job18404_output.zip | Job18404_statistic.txt |

SRS_Standard | 300 secs. | prove cycle non-/termination by transformation and string termination and by trace-decreasing matrix interpretations | Job | Job18405_output.zip | Job18405_statistic.txt |

SRS_Standard | 300 secs. | prove cycle non-/termination by transformation and relative string termination | Job | Job18414_output.zip | Job18414_statistic.txt |

SRS_Relative | 60 secs. | prove relative cycle non-/termination by transformation and relative string termination and by trace-decreasing matrix interpretations | Job | Job18412_output.zip | Job18412_statistic.txt |

SRS_Relative | 300 secs. | prove relative cycle non-/termination by transformation and relative string termination and by trace-decreasing matrix interpretations | Job | Job18415_output.zip | Job18415_statistic.txt |

The results from the competition are available here which were run on StarExec, the original job can be found here.

Benchmark set |
Time limit |
Description |
Job on StarExec |
Output of job |
Short summary of output |

SRS_Standard | 60 secs. | prove cycle non-/termination by transformation and string termination and by trace-decreasing matrix interpretations | Job | Job14995_output.zip | Job14995_statistic.txt |

SRS_Standard | 300 secs. | Job | Job15019_output.zip | Job15019_statistic.txt | |

SRS_Standard | 300 secs. | prove cycle non-/termination by transformation and relative string termination | Job | Job15075_output.zip | Job15075_statistic.txt |

SRS_Relative | 60 secs. | prove relative cycle non-/termination by transformation and relative string termination and by trace-decreasing matrix interpretations | Job | Job14994_output.zip | Job14994_statistic.txt |

SRS_Relative | 300 secs. | Job | Job15020_output.zip | Job15020_statistic.txt |

Our tool cycsrs (using many other termination and deduction tools) participated in the new category. The results from the competition are available here which were run on StarExec, the original job can be found here.

An overall summary of the experiments can be found

The detailed results for the following three problem sets can be found on separate webpages:

- The results of proving cycle termination of the 1315 problems of SRS_Standard-branch of the Termination Problem Data Base can be found
**[here]** - The results of proving cycle termination of 50000 randomly generated problems of size 12 over an alphabet of size 3 can be found
**[here]** - The results of proving cycle termination of some selected (and some quite hard) problems, including examples from the paper, are collected
**[here]**

- Source distribution as a cabalized Haskell-package: cycsrs-0.2.0.5.tar.gz

Type

`cycsrs help`

for a detailed usage information.
The tool can perform the transformations without any further tools, but for proving cycle termination the termination provers torpacyc, AProVE, and TTT2 (and their dependencies) are required to be installed. See the README for detailed explanations.

Changes for 0.2.0.5 compared to version 0.2.0.2:

- The cycle nontermination checker was improved

Changes for 0.2.0.2 compared to version 0.2.0.0:

- A bug in the cycle nontermination checker was fixed.

Changes compared to version 0.1.0.0:

- torpacyc 2014 is no longer available (torpacyc 2015 remains)
- several cycle termination techniques are extended for relative cycle termination
- a new cycle non-termination checker cycnt is included and can be called from cycsrs
- a new cycle termination checker tdmi is included and can be called from cycsrs, it searches for trace-decreasing matrix interpretations using the normal, tropical and arctic semi-ring. It targets QF_BV of SMT-LIB and thus can be used with different SMT-solvers.
- tdmi and cycnt are ready to use for relative cycle termination
- configuring the tool chain and distributing time limits on the several chain is more comfortable
- the source code was heavily rewritten, using the concept of non-/termination processors to allow for a more modular design

- Source distribution as a cabalized Haskell-package: CYCSRS-0.1.0.0.tar.gz
- Precompilied linux binaries: [32bit-dynamically linked | 64bit-dynamically linked | 64bit-statically linked]

`./CYCSRS help`

for a detailed usage information.
The tool can perform the transformations without any further tools, but for proving cycle termination the termination provers torpacyc, AProVE, and TTT2 (and their dependencies) are required to be installed. See the README for detailed explanations.