A second-order formulation of non-termination

• We consider the termination/non-termination property of a class of loops.
• Second-order logic is a convenient language to express non-termination.
• We restrict this language to known decidable cases.
• We exhibit new classes of loops, the non-termination of which is decidable.
• We present a bunch of examples.

We consider the termination/non-termination property of a class of loops. Such loops are commonly used abstractions of real program pieces. Second-order logic is a convenient language to express non-termination. Of course, such property is generally undecidable. However, by restricting the language to known decidable cases, we exhibit new classes of loops, the non-termination of which is decidable. We present a bunch of examples.