On termination of integer linear loops

DOI10.1137/1.9781611973730.65zbMATH Open1372.68065arXiv1407.1891OpenAlexW2951018967MaRDI QIDQ5363097FDOQ5363097

Authors: Joël Ouaknine, J. Sousa Pinto, James Worrell 

Publication date: 5 October 2017

Published in: Proceedings of the Twenty-Sixth Annual ACM-SIAM Symposium on Discrete Algorithms (Search for Journal in Brave)

Abstract: A fundamental problem in program verification concerns the termination of simple linear loops of the form x := u ; while Bx >= b do {x := Ax + a} where x is a vector of variables, u, a, and c are integer vectors, and A and B are integer matrices. Assuming the matrix A is diagonalisable, we give a decision procedure for the problem of whether, for all initial integer vectors u, such a loop terminates. The correctness of our algorithm relies on sophisticated tools from algebraic and analytic number theory, Diophantine geometry, and real algebraic geometry. To the best of our knowledge, this is the first substantial advance on a 10-year-old open problem of Tiwari (2004) and Braverman (2006).

Full work available at URL: https://arxiv.org/abs/1407.1891

Recommendations

• Termination of Integer Linear Programs
• Computer Aided Verification
• TERMINATION ANALYSIS OF LINEAR LOOPS
• Termination of linear programs with nonlinear constraints
• Termination analysis of linear loop programs

Mathematics Subject Classification ID

Applications of commutative algebra (e.g., to statistics, control theory, optimization, etc.) (13P25) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semialgebraic sets and related spaces (14P10) Loops, quasigroups (20N05) Decidability (number-theoretic aspects) (11U05)

Cited In (22)

• TERMINATION ANALYSIS OF LINEAR LOOPS
• On eventual non-negativity and positivity for the weighted sum of powers of matrices
• Reflections on termination of linear loops
• Termination of triangular Integer loops is decidable
• Vector and scalar reachability problems in \(\operatorname{SL}(2, \mathbb{Z})\)
• On the Identity Problem for the Special Linear Group and the Heisenberg Group.
• Non-termination Sets of Simple Linear Loops
• Witness to non-termination of linear programs
• A calculus for modular loop acceleration
• The membership problem for subsemigroups of \(\operatorname{GL}_2(\mathbb{Z})\) is \textbf{NP}-complete
• On the termination of integer loops
• Title not available (Why is that?)
• Termination of polynomial loops
• On the mortality problem: from multiplicative matrix equations to linear recurrence sequences and beyond
• On the identity and group problems for complex Heisenberg matrices
• Reachability problems for one-dimensional piecewise affine maps
• Computing expected runtimes for constant probability programs
• On the mortality problem: from multiplicative matrix equations to linear recurrence sequences and beyond
• Complexity of Restricted Variants of Skolem and Related Problems
• Termination of Integer Linear Programs
• CONCUR 2005 – Concurrency Theory
• Title not available (Why is that?)

This page was built for publication: On termination of integer linear loops

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5363097)