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

lmcs:1001 - Logical Methods in Computer Science, July 11, 2010, Volume 6, Issue 3
Size-Change Termination, Monotonicity Constraints and Ranking Functions

Authors: Ben-Amram, Amir M.

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.

DOI : 10.2168/LMCS-6(3:2)2010
Volume: Volume 6, Issue 3
Published on: July 11, 2010
Submitted on: September 29, 2009
Keywords: Computer Science - Logic in Computer Science,D.2.4, F.3.1


Consultation statistics

This page has been seen 146 times.
This article's PDF has been downloaded 53 times.