Monotonicity Constraints for Termination in the Integer Domain

Amir M. Ben-Amram

doi:10.2168/LMCS-7(3:4)2011

Amir M. Ben-Amram - Monotonicity Constraints for Termination in the Integer Domain

lmcs:1002 - Logical Methods in Computer Science, August 24, 2011, Volume 7, Issue 3 - https://doi.org/10.2168/LMCS-7(3:4)2011

Monotonicity Constraints for Termination in the Integer DomainArticle

Authors: Amir M. Ben-Amram

Size-Change Termination (SCT) is a method of proving program termination based on the impossibility of infinite descent. To this end we use a program abstraction in which transitions are described by Monotonicity Constraints over (abstract) variables. When only constraints of the form x>y' and x\geq y' are allowed, we have size-change graphs. In the last decade, both theory and practice have evolved significantly in this restricted framework. The crucial underlying assumption of most of the past work is that the domain of the variables is well-founded. In a recent paper I showed how to extend and adapt some theory from the domain of size-change graphs to general monotonicity constraints, thus complementing previous work, but remaining in the realm of well-founded domains. However, monotonicity constraints are, interestingly, capable of proving termination also in the integer domain, which is not well-founded. The purpose of this paper is to explore the application of monotonicity constraints in this domain. We lay the necessary theoretical foundation, and present precise decision procedures for termination; finally, we provide a procedure to construct explicit global ranking functions from monotonicity constraints in singly-exponential time, and of optimal worst-case size and dimension (ordinal).

https://doi.org/10.2168/LMCS-7(3:4)2011

Source: arXiv.org:1105.6317

Volume: Volume 7, Issue 3

Published on: August 24, 2011

Imported on: October 28, 2010

Keywords: Computer Science - Logic in Computer Science,D.2.4, F.3.1

Licence: arXiv.org - Non-exclusive license to distribute

Classifications

Mathematics Subject Classification 2020¹

Sources:

[1] zbMATH Open.

Bibliographic References

18 Documents citing this article

Martin Avanzini;Georg Moser;Michael Schaper, 2020, A modular cost analysis for probabilistic programs, Proceedings of the ACM on Programming Languages, 4, OOPSLA, pp. 1-30, 10.1145/3428240, https://doi.org/10.1145/3428240.

Sarah Winkler;Georg Moser, 2019, Smarter Features, Simpler Learning?, arXiv (Cornell University), 311, pp. 25-31, 10.4204/eptcs.311.4.

Yu-Fang Chen;Matthias Heizmann;Ondřej Lengál;Yong Li;Ming-Hsien Tsai;et al., Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, Advanced automata-based algorithms for program termination checking, 2018, Philadelphia PA USA, 10.1145/3192366.3192405.

Yu-Fang Chen;Matthias Heizmann;Ondřej Lengál;Yong Li;Ming-Hsien Tsai;et al., 2018, Advanced automata-based algorithms for program termination checking, ACM SIGPLAN Notices, 53, 4, pp. 135-150, 10.1145/3296979.3192405.

Thomas Colcombet;Laure Daviaud;Florian Zuleger, Lecture notes in computer science, Automata and Program Analysis, pp. 3-10, 2017, 10.1007/978-3-662-55751-8_1.

Amir M. Ben-Amram;Aviad Pineles, 2016, Flowchart Programs, Regular Expressions, and Decidability of Polynomial Growth-Rate, arXiv (Cornell University), 216, pp. 24-49, 10.4204/eptcs.216.2.

Martin Avanzini;Georg Moser, 2016, A combination framework for complexity, Information and Computation, 248, pp. 22-55, 10.1016/j.ic.2015.12.007, https://doi.org/10.1016/j.ic.2015.12.007.

Amir M. Ben-Amram;Samir Genaim, Lecture notes in computer science, Complexity of Bradley-Manna-Sipma Lexicographic Ranking Functions, pp. 304-321, 2015, 10.1007/978-3-319-21668-3_18, https://doi.org/10.1007/978-3-319-21668-3_18.

Florian Zuleger, Lecture notes in computer science, Asymptotically Precise Ranking Functions for Deterministic Size-Change Systems, pp. 426-442, 2015, 10.1007/978-3-319-20297-6_27.

Fred Mesnard;Étienne Payet, 2015, A second-order formulation of non-termination, 115, 11, pp. 882-885, 10.1016/j.ipl.2015.05.012, https://hal.univ-reunion.fr/hal-01451689.

Teng Long;Wenhui Zhang, 2015, Termination analysis with recursive calling graphs, Journal of Network and Computer Applications, 59, pp. 109-116, 10.1016/j.jnca.2015.06.019.

Amir M. Ben-Amram;Samir Genaim, 2014, Ranking Functions for Linear-Constraint Loops, arXiv (Cornell University), 61, 4, pp. 1-55, 10.1145/2629488, http://arxiv.org/abs/1208.4041.

None Teng Long;None Wenhui Zhang, 2014 IEEE Computers, Communications and IT Applications Conference, Termination analysis with recursive calling graphs, pp. 276-282, 2014, Beijing, China, 10.1109/comcomap.2014.7017210.

Laura Bozzelli;Sophie Pinchinat, 2013, Verification of gap-order constraint abstractions of counter systems, Theoretical Computer Science, 523, pp. 1-36, 10.1016/j.tcs.2013.12.002, https://doi.org/10.1016/j.tcs.2013.12.002.

Amir M. Ben-Amram;Samir Genaim;Abu Naser Masud, Lecture notes in computer science, On the Termination of Integer Loops, pp. 72-87, 2012, 10.1007/978-3-642-27940-9_6.

Amir M. Ben-Amram;Samir Genaim;Abu Naser Masud, 2012, On the Termination of Integer Loops, ACM Transactions on Programming Languages and Systems, 34, 4, pp. 1-24, 10.1145/2400676.2400679, https://doi.org/10.1145/2400676.2400679.

Florian Zuleger;Sumit Gulwani;Moritz Sinn;Helmut Veith, Lecture notes in computer science, Bound Analysis of Imperative Programs with the Size-Change Abstraction, pp. 280-297, 2011, 10.1007/978-3-642-23702-7_22.

MICHAEL CODISH;IGOR GONOPOLSKIY;AMIR M. BEN-AMRAM;CARSTEN FUHS;JÜRGEN GIESL, 2011, SAT-based termination analysis using monotonicity constraints over the integers, arXiv (Cornell University), 11, 4-5, pp. 503-520, 10.1017/s1471068411000147, https://arxiv.org/abs/1107.5980.

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 1529 times.

This article's PDF has been downloaded 433 times.