Non-termination using Regular Languages

2014/05/22 by Jörg Endrullis, Endrullis, Jörg, Hans Zantema +1
Computer Science · #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #cs.LO

paper · pdf · doi:10.48550/arxiv.1405.5662

Published at International Workshop on Termination 2014

arxiv created 2014/05/22 · arxiv updated 2014/05/23

Abstract

We describe a method for proving non-looping non-termination, that is, of term rewriting systems that do not admit looping reductions. As certificates of non-termination, we employ regular (tree) automata.

Related

• Proving Looping and Non-Looping Non-Termination by Finite Automata
• Non-Termination in Term Rewriting and Logic Programming
• Binary Non-Termination in Term Rewriting and Logic Programming
• Disproving Termination of Non-Erasing Sole Combinatory Calculus with Tree Automata (Full Version)
• A Second-Order Formulation of Non-Termination