Termination of equality-constrained linear loops

Klaus Dräger

It is well known that for general linear loops of the form

while A do
           B_1 -> v := C_1 v + d_1  |  ...  |  B_n -> v := C_n v + d_n

involving a nondeterministic choice over guarded linear assignments, termination is undecidable when the conditions A, B_1, ... , B_n can be arbitrary linear constraints. Interestingly, requiring them to be conjunctions of linear equations is enough to make the problem decidable. I will show a proof of this which uses surprisingly elementary methods.