Document Open Access Logo

Proving non-termination by finite automata

Authors Jörg Endrullis, Hans Zantema



PDF
Thumbnail PDF

File

LIPIcs.RTA.2015.160.pdf
  • Filesize: 0.6 MB
  • 17 pages

Document Identifiers

Author Details

Jörg Endrullis
Hans Zantema

Cite AsGet BibTex

Jörg Endrullis and Hans Zantema. Proving non-termination by finite automata. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 160-176, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2015)
https://doi.org/10.4230/LIPIcs.RTA.2015.160

Abstract

A new technique is presented to prove non-termination of term rewriting. The basic idea is to find a non-empty regular language of terms that is closed under rewriting and does not contain normal forms. It is automated by representing the language by a tree automaton with a fixed number of states, and expressing the mentioned requirements in a SAT formula. Satisfiability of this formula implies non-termination. Our approach succeeds for many examples where all earlier techniques fail, for instance for the S-rule from combinatory logic.
Keywords
  • non-termination
  • finite automata
  • regular languages

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail