Amir M. Ben-Amram - Size-Change Termination, Monotonicity Constraints and Ranking Functions

lmcs:1001 - Logical Methods in Computer Science, July 11, 2010, Volume 6, Issue 3 - https://doi.org/10.2168/LMCS-6(3:2)2010
Size-Change Termination, Monotonicity Constraints and Ranking FunctionsArticle

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 may 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>=y' are allowed, we have size-change graphs. Both theory and practice are now more evolved in this restricted framework then in the general framework of monotonicity constraints. This paper shows that it is possible to extend and adapt some theory from the domain of size-change graphs to the general case, thus complementing previous work on monotonicity constraints. In particular, we present precise decision procedures for termination; and we provide a procedure to construct explicit global ranking functions from monotonicity constraints in singly-exponential time, which is better than what has been published so far even for size-change graphs.


    Volume: Volume 6, Issue 3
    Published on: July 11, 2010
    Imported on: September 29, 2009
    Keywords: Computer Science - Logic in Computer Science,D.2.4, F.3.1

    13 Documents citing this article

    Consultation statistics

    This page has been seen 927 times.
    This article's PDF has been downloaded 233 times.