Proving looping and non-looping non-termination by finite automata

J. Endrullis, H. Zantema

Onderzoeksoutput: Boek/rapportRapportAcademic

39 Downloads (Pure)

Samenvatting

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
Originele taal-2Engels
Uitgeverijs.n.
Aantal pagina's20
StatusGepubliceerd - 2015

Publicatie series

NaamarXiv
Volume1505.00478 [cs.LO]

Vingerafdruk Duik in de onderzoeksthema's van 'Proving looping and non-looping non-termination by finite automata'. Samen vormen ze een unieke vingerafdruk.

  • Citeer dit

    Endrullis, J., & Zantema, H. (2015). Proving looping and non-looping non-termination by finite automata. (arXiv; Vol. 1505.00478 [cs.LO]). s.n.