##
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
od
```

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.