What Else is Undecidable About Loops?

Abstract

We address algebraic aspects of invariant generation and proving termination, two central questions of program analysis, for non-deterministic loops with polynomial updates. Our focus is sketching the boundary of (un-)decidability for both problems between different classes of programs. The first main contribution of this work is related to the question raised by Braverman in 2006: “How much non-determinism can be introduced in a linear loop before termination becomes undecidable?” We show that termination of loops with a purely non-deterministic choice between linear updates is undecidable in the presence of linear inequality loop conditions. In the context of invariants, an algorithm is known that computes all polynomial relations among variables of loops with multiple linear updates. At the same time, allowing polynomial assignments of higher degrees was shown to result in algorithmic unsolvability. We highlight that negative results in fact do not exploit general polynomial updates. We show that no algorithm can find all polynomial relations for programs as soon as quadratic updates or updates guarded by affine equalities are involved.