A Second-Order Formulation of Non-Termination

TL;DR

This paper explores the use of second-order logic to analyze non-termination in loops, identifying new decidable classes within known undecidable cases, thus advancing understanding of program non-termination.

Contribution

It introduces a second-order formulation for non-termination analysis and identifies new decidable classes of loops within known undecidable cases.

Findings

Decidable classes of non-termination in certain loops

Second-order logic effectively models non-termination properties

Examples illustrating the application of the new approach

Abstract

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.