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

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

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

(27)

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

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)