Testing for termination with monotonicity constraints

Michael Codish, Vitaly Lagoon, Peter J. Stuckey

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review

37 Citations (Scopus)


Termination analysis is often performed over the abstract domains of monotonicity constraints or of size change graphs. First, the transition relation for a given program is approximated by a set of descriptions. Then, this set is closed under a composition operation. Finally, termination is determined if all of the idempotent loop descriptions in this closure have (possibly different) ranking functions. This approach is complete for size change graphs: An idempotent loop description has a ranking function if and only if it has one which indicates that some specific argument decreases in size. In this paper we generalize the size change criteria for size change graphs which are not idempotent. We also illustrate that proving termination with monotonicity constraints is more powerful than with size change graphs and demonstrate that the size change criteria is incomplete for monotonicity constraints. Finally, we provide a complete termination test for monotonicity constraints.

Original languageEnglish
Title of host publicationLogic Programming
Subtitle of host publication21st International Conference, ICLP 2005 Sitges, Spain, October 2-5, 2005 Proceedings
EditorsMaurizio Gabbrielli, Gopal Gupta
Place of PublicationBerlin Germany
Number of pages15
ISBN (Print)354029208X, 9783540292081
Publication statusPublished - 31 Oct 2005
Externally publishedYes
EventInternational Conference on Logic Programming 2005 - Sitges, Spain
Duration: 2 Oct 20055 Oct 2005
Conference number: 21st
https://link.springer.com/book/10.1007/11562931 (Proceedings)

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743


ConferenceInternational Conference on Logic Programming 2005
Abbreviated titleICLP 2005
Internet address

Cite this