Non-termination using Regular Languages
J\"org Endrullis, Hans Zantema
TL;DR
This paper presents a method to prove non-termination in term rewriting systems by using regular tree automata as certificates, focusing on systems that do not admit looping reductions.
Contribution
It introduces a novel approach employing regular automata to certify non-termination in non-looping term rewriting systems.
Findings
Automata-based certificates effectively prove non-termination.
Method applies to systems without looping reductions.
Enhances non-termination analysis techniques.
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · semigroups and automata theory · Formal Methods in Verification