Non-Termination Sets of Simple Linear Loops

TL;DR

This paper investigates the non-termination sets of simple linear loops, providing a complete algorithm for two variables and showing limitations for more variables.

Contribution

It introduces a complete algorithm for determining non-termination inputs in two-variable simple linear loops and highlights the complexity increase with more variables.

Findings

Complete algorithm for two-variable loops

Non-termination set cannot be generally described by Tarski formulae for more variables

Complexity increases with the number of program variables

Abstract

A simple linear loop is a simple while loop with linear assignments and linear loop guards. If a simple linear loop has only two program variables, we give a complete algorithm for computing the set of all the inputs on which the loop does not terminate. For the case of more program variables, we show that the non-termination set cannot be described by Tarski formulae in general