Non-termination using Regular Languages
Jörg Endrullis, Hans Zantema · arXiv (Cornell University) · 2014
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.