Termination of Cycle Rewriting

Papers

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 ]
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)  ]
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 ]

Online Tools

Try our Online Prover to prove cycle termination.

Transform a cycle rewrite system into a string rewrite system with our Online Transformer.

Experimental Results

Benchmarks for cycsrs-0.2.0.5, September 2016

We performed several experiments on StarExec. The results and job information can be found via the linked job pages on StarExec.

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

Termination and Complexity Competition 2016

Our tool cycsrs participated in the Cycle Rewriting category in the Termination and Complexity Competition 2016 which was affiliated with 15th International Workshop on Termination.

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

Benchmarks for cycsrs-0.2.0.0, April 2016

To benchmark the updated version of cycsrs, we performed several experiments on StarExec. The results and job information can be found via the linked job pages on StarExec.

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. prove cycle non-/termination by transformation and string termination and by trace-decreasing matrix interpretations 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. prove relative cycle non-/termination by transformation and relative string termination and by trace-decreasing matrix interpretations Job Job15020_output.zip Job15020_statistic.txt

Termination Competition 2015

Cycle Rewriting became a new category in the Termination Competition 2015 which was affiliated with CADE-15.

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.

Results obtained for the RTA 2015 paper

We tried to prove cycle termination of several problems using our developed techniques.

An overall summary of the experiments can be found [here].

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]
Due to their large size not all termination proofs generated by termination provers are included on the corresponding websites, but they can be downloaded as a single compressed tar-archive [here] (compressed size ~1,2GB, uncompressed ~26GB)

Downloads

torpacyc

The recent version of torpacyc (developed by Hans Zantema) can be download from this webpage.

Command line tool cycsrs (Version 0.2.0.5)

The new version of the command line tool cycsrs to transform cycle rewriting systems into string rewrite systems and to prove cycle termination by different tools is available as: It includes also the sources of the cycle non-termination checker cycnt and the cycle termination prover tdmi which searches for trace decreasing matrix interpretations using SMT-solvers.

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

Command line tool cycsrs (Version 0.1.0.0)

The command line tool to transform cycle rewriting systems into string rewrite systems and to prove cycle termination by different tools is available as: 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.