Document Open Access Logo

Loop Termination and Generalized Collatz Sequences

Author Mishel Carelli

PDF

File

Thumbnail PDF
PDF
LIPIcs.ICALP.2026.175.pdf
  • Filesize: 0.89 MB
  • 21 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Program Verification
  • Loop Termination
  • Generalized Collatz Sequences
  • Linear-Constraint Loops

Metrics

Abstract

Linear-constraint loops are programs whose transition relation is specified by a system of linear inequalities. The termination problem asks, given a loop, whether it admits an infinite computation. Decidability of termination remains open for linear-constraint loops over integers, rationals, and reals. We focus on loops over integers and show that they are tightly connected to generalized Collatz sequences - integer sequences generated by maps that are linear on each residue class modulo a fixed natural number. We prove that termination of one-variable linear-constraint loops is decidable in polynomial time, provided a long-standing conjecture about generalized Collatz sequences holds. Conversely, we show that any decision procedure for one-variable loops would prove or refute specific instances of this conjecture, which remain open. Moreover, we show that if a one-variable loop has a cyclic trace, then it also has a cyclic trace of length at most two.

Cite As Get BibTex

Mishel Carelli. Loop Termination and Generalized Collatz Sequences. In 53rd International Colloquium on Automata, Languages, and Programming (ICALP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 374, pp. 175:1-175:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.ICALP.2026.175

Author Details

Mishel Carelli
  • CISPA Helmholtz Center for Information Security, Saarbrücken, Germany

Funding

  • Carelli, Mishel: This work was supported by the European Research Council (ERC) Grant HYPER (No. 101055412).

Acknowledgements

I want to thank Arkadiy Aliev, Bernd Finkbeiner, and Joël Ouaknine for the useful discussions.

References

  1. Amir M. Ben-Amram. Mortality of Iterated Piecewise Affine Functions over the Integers: Decidability and Complexity. In Natacha Portier and Thomas Wilke, editors, 30th International Symposium on Theoretical Aspects of Computer Science (STACS 2013), volume 20 of Leibniz International Proceedings in Informatics (LIPIcs), pages 514-525, Dagstuhl, Germany, 2013. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.STACS.2013.514.
  2. Amir M. Ben-Amram, Samir Genaim, and Abu Naser Masud. On the termination of integer loops. ACM Trans. Program. Lang. Syst., 34(4), 2012. URL: https://doi.org/10.1145/2400676.2400679.
  3. Amir M. Ben-Amram, Samir Genaim, Joël Ouaknine, and James Worrell. Termination analysis of linear-constraint programs, 2025. URL: https://doi.org/10.48550/arXiv.2509.06752.
  4. Mark de Berg, Otfried Cheong, Marc van Kreveld, and Mark Overmars. Computational Geometry: Algorithms and Applications. Springer-Verlag TELOS, Santa Clara, CA, USA, 3rd ed. edition, 2008. Google Scholar
  5. Tewodros A. Beyene, Corneliu Popeea, and Andrey Rybalchenko. Solving existentially quantified horn clauses. In Natasha Sharygina and Helmut Veith, editors, Computer Aided Verification, pages 869-882, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-642-39799-8_61.
  6. Vincent D. Blondel, Olivier Bournez, Pascal Koiran, Christos H. Papadimitriou, and John N. Tsitsiklis. Deciding stability and mortality of piecewise affine dynamical systems. Theor. Comput. Sci., 255(1–2):687-696, March 2001. URL: https://doi.org/10.1016/S0304-3975(00)00399-6.
  7. Mark Braverman. Termination of integer linear programs. In Thomas Ball and Robert B. Jones, editors, Computer Aided Verification, pages 372-385, Berlin, Heidelberg, 2006. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/11817963_34.
  8. Byron Cook, Andreas Podelski, and Andrey Rybalchenko. Terminator: beyond safety. In Proceedings of the 18th International Conference on Computer Aided Verification, CAV'06, pages 415-418, Berlin, Heidelberg, 2006. Springer-Verlag. URL: https://doi.org/10.1007/11817963_37.
  9. Quentin Guilmant, Engel Lefaucheux, Joël Ouaknine, and James Worrell. The 2-Dimensional Constraint Loop Problem Is Decidable. In Karl Bringmann, Martin Grohe, Gabriele Puppis, and Ola Svensson, editors, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024), volume 297 of Leibniz International Proceedings in Informatics (LIPIcs), pages 140:1-140:21, Dagstuhl, Germany, 2024. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ICALP.2024.140.
  10. Matthias Heizmann, Jochen Hoenicke, Jan Leike, and Andreas Podelski. Linear ranking for linear lasso programs. In Dang Van Hung and Mizuhito Ogawa, editors, Automated Technology for Verification and Analysis, pages 365-380, Cham, 2013. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-02444-8_26.
  11. Mehran Hosseini, Joël Ouaknine, and James Worrell. Termination of Linear Loops over the Integers. In Christel Baier, Ioannis Chatzigiannakis, Paola Flocchini, and Stefano Leonardi, editors, 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019), volume 132 of Leibniz International Proceedings in Informatics (LIPIcs), pages 118:1-118:13, Dagstuhl, Germany, 2019. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ICALP.2019.118.
  12. Jeffrey C. Lagarias. The 3x+1 problem: An overview, 2021. URL: https://arxiv.org/abs/2111.02635.
  13. George M. Leigh. A markov process underlying the generalized syracuse algorithm. Acta Arithmetica, 46:125-143, 1986. URL: https://api.semanticscholar.org/CorpusID:117635633.
  14. Hendrik W. Lenstra. Integer programming with a fixed number of variables. Math. Oper. Res., 8:538-548, 1983. URL: https://doi.org/10.1287/MOOR.8.4.538.
  15. Keith R. Matthews. Some borel measures associated with the generalized collatz mapping. Colloquium Mathematicum, 63:191-202, 1992. URL: https://api.semanticscholar.org/CorpusID:54607478.
  16. Keith R Matthews. Generalized 3x+ 1 mappings: markov chains and ergodic theory. The ultimate challenge: The 3x, 1:79-103, 2010. Google Scholar
  17. Keith R. Matthews and A. M. Watts. A markov approach to the generalized syracuse algorithm. Acta Arithmetica, 45:29-42, 1985. URL: https://api.semanticscholar.org/CorpusID:118600406.
  18. Watts A. Matthews K. A generalization of hasse’s generalization of the syracuse algorithm. Acta Arithmetica, 43(2):167-175, 1984. URL: http://eudml.org/doc/205897.
  19. H. Möller. Über hasses verallgemeinerung des syracuse-algorithmus (kakutanis problem). Acta Arithmetica, 34:219-226, 1978. URL: https://api.semanticscholar.org/CorpusID:117690327.
  20. Christos H. Papadimitriou. On the complexity of integer programming. J. ACM, 28(4):765-768, October 1981. URL: https://doi.org/10.1145/322276.322287.
  21. A. Podelski and A. Rybalchenko. Transition invariants. In Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, 2004., pages 32-41, 2004. URL: https://doi.org/10.1109/LICS.2004.1319598.
  22. Andreas Podelski and Andrey Rybalchenko. A complete method for the synthesis of linear ranking functions. In Verification, Model Checking, and Abstract Interpretation, 5th International Conference, VMCAI 2004, Venice, Italy, January 11-13, 2004, Proceedings, volume 2937, pages 239-251, January 2004. URL: https://doi.org/10.1007/978-3-540-24622-0_20.
  23. R. Tyrrell Rockafellar. Convex Analysis. Princeton Landmarks in Mathematics and Physics. Princeton University Press, 1970. Google Scholar
  24. Alexander Schrijver. Theory of linear and integer programming. John Wiley & Sons, Inc., USA, 1986. Google Scholar
  25. Simon Telen. Introduction to toric geometry, 2022. URL: https://arxiv.org/abs/2203.01690.
  26. A. Tiwari. Termination of linear programs. In R. Alur and D. Peled, editors, Computer-Aided Verification, CAV, volume 3114 of LNCS, pages 70-82. Springer, July 2004. URL: https://doi.org/10.1007/978-3-540-27813-9_6.
  27. Hiroshi Unno, Tachio Terauchi, and Eric Koskinen. Constraint-based relational verification. In Alexandra Silva and K. Rustan M. Leino, editors, Computer Aided Verification, pages 742-766, Cham, 2021. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-81685-8_35.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact