1. Termination of Linear Loops over the Integers
- Author
-
Hosseini, M, Ouaknine, J, Worrell, J, and Wagner, Michael
- Subjects
FOS: Computer and information sciences ,050101 languages & linguistics ,000 Computer science, knowledge, general works ,Formal Languages and Automata Theory (cs.FL) ,05 social sciences ,Computer Science - Formal Languages and Automata Theory ,02 engineering and technology ,Computational Complexity (cs.CC) ,Computer Science - Computational Complexity ,Computer Science ,0202 electrical engineering, electronic engineering, information engineering ,020201 artificial intelligence & image processing ,0501 psychology and cognitive sciences ,Computer Science::Formal Languages and Automata Theory - Abstract
We consider the problem of deciding termination of single-path while loops with integer variables, affine updates, and affine guard conditions. The question is whether such a loop terminates on all integer initial values. This problem is known to be decidable for the subclass of loops whose update matrices are diagonalisable, but the general case has remained open since being conjectured decidable by Tiwari in 2004. In this paper we show decidability of determining termination for arbitrary update matrices, confirming Tiwari's conjecture. For the class of loops considered in this paper, the question of deciding termination on a specific initial value is a longstanding open problem in number theory. The key to our decision procedure is in showing how to circumvent the difficulties inherent in deciding termination on a fixed initial value., Comment: Published in ICALP 2019
- Published
- 2019
- Full Text
- View/download PDF