On termination of integer linear loops

DOI10.1137/1.9781611973730.65MaRDI QIDQ5363097zbMATH OpenOpenAlexFDO

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)

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

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)

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).

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

Cited in

(22)

• On eventual non-negativity and positivity for the weighted sum of powers of matrices
• TERMINATION ANALYSIS OF LINEAR LOOPS
• 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
• Termination of polynomial loops
• scientific article; zbMATH DE number 6401180 (Why is no real title available?)
• 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
• scientific article; zbMATH DE number 7204378 (Why is no real title available?)

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)