Size-Change Termination and Constraint Transition Systems

Amir Ben-Amram

What is Size-Change Termination?

Size-Change Termination (SCT for short) is a method of proving the termination of computer programs. It is based on the following principle: we can deduce that a program terminates on all inputs if we show that every infinite computation would necessarily cause an infinite descent in some data values, that are by their nature well-founded.
For a simple example, consider any loop that is guaranteed to take an element out of some initial, finite list in every iteration. Assuming that the list does not grow while the loop is running, an infinite loop would imply infinite descent in the length of the list, which is impossible, therefore the loop must terminate.

Applying this approach to a program involves two steps:

Compared to other approaches to termination analysis, the size-change termination approach is surprisingly simple and general: proofs by lexicographic orders, multiset descent, descent of the maximum or minimum among a set of variables, and other scenarios are all handled automatically and without special treatment, with no need for synthesizing orderings on program states. Another aspect of its generality is that the approach is applicable to all kinds of programs: functional programs (even high-order), imperative programs, logic programs. All these cases can be found in the bibliography. In fact, it is a benefit of the modularity of the approach that only the "front end" needs to be adapted to a programming language. This could allow for "back end" software to be shared, although there are still technical challenges on the road to fully exploiting this opportunity.

Here are slides from an overview talk about size-change termination. The overview also touches on the more recent extensions described below.
For more advanced students of the topic, perhaps these slides from some lectures I gave might also be useful.

What are Constraint Transition Systems?

The theory of size-change termination has been evolving for more than a decade, and one of the important insights is that the framework described above is a special case of a more general one. Constraint Transition Systems (CTS) are a simple model whereby different kinds of programs can be represented, possibly thanks to abstraction, with an eye towards proving their termination (or related properties).

Generally, a CTS is a directed graph, which may be understood as the control-flow graph of the program, and whose arcs represent state transitions. A state is described by the control-flow point (node in the graph) plus a finite number of state variables. Every arc is annotated with a formula that specifies constraints on the state variables before and after the transition. Thus, depending on the domain of the variables and the expressivity of the constraint language, a CTS may be as expressive as a concrete program (for example, using natural numbers and a rather simple constraint language, we can represent a counter automaton). We may write CTS(L,D) for Constraint Transition Systems using the constraint language L over data D. The original SCT abstraction is CTS(scg,Ord) where scg stands for size-change graphs and Ord for well-founded sets. Recently, I have been working with CTS(mc,Int), the language of monotonicity constraints over the integers. Monotonicity constraints generalize size-change graphs as they are arbitrary conjunctions of relations of the kinds "greater than" or "greater than or equal to" between any pair of variables in the source and target states.

CTSs over the integers are suitable for representation of a wide range of programs (and the programs where SCT has been found useful typically use the natural numbers as the well-founded domain and therefore can also be represnted in CTS(mc,Int)). Research has established that a lot of the good understanding we have for the SCT abstraction can be extended to this more expressive model. For details look for related publications below.

Implementation and application.

The SCT approach has been implemented in several tools, ranging from demonstration prototypes to industry-strength tools. Most implementations combine SCT analysis with other techniques, in particular with front-ends for concrete programs. For further information look for "Implementations of SCT" and "systems that incorporate SCT analysis" below and also the bibliography.

Some Highlights of SCT Theory

(an arbitrary selection in no particular order)

My publications on size-change termination

(in chronological order)

The Size-Change Principle for Program Termination (with C. S. Lee and N. D. Jones), POPL 2001:
The initiation of the SCT project. This paper gives an abstract definition of the analysis problem (when size-change graphs are given), shows how it applies to a simple functional language, and establishes the problem's computational complexity as complete for PSPACE.

General Size-Change Termination and Lexicographic Descent, LNCS Vol. 2566, 2002:
A paper relating size-change termination with lexicographic descent, proving that while size-change termination encompasses rich class of programs, in terms of computability this class is not stronger then the class of programs with termination governed by lexicographic descent. This affirmed a conjecture previously made by Neil Jones. Note that the result has now become a corollary of later results on ranking functions, see below.

Size-Change Termination in Polynomial Time (with C. S. Lee), ACM TOPLAS, 29:1 (2007):
This is research on how to perform the SCT analysis phase (the second step) efficiently. We propose a polynomial-time algorithm which we have also implemented. We claim that while the algorithm cannot recognize every terminating instance (as you might expect, given its efficiency), it covers a range of dataflow patterns that is sufficiently rich for wide applicability.

Size-Change Termination with Difference Constraints ACM TOPLAS, 30:3 (2008):
This is research on how to deduce size-change termination when bounds on increases are also pertinent (e.g., something increases and than decreases even more). As in the LJB paper, an abstract formulation of the problem and a theoretical complexity analysis is presented.

A Complexity Tradeoff in Ranking-Function Termination Proofs Acta Informatica 46:1 (2009):
Codish, Lagoon and Stuckey (ICLP 2005) noted an intimate relation of SCT termination proofs to proofs based on local, linear ranking functions (these concepts are taken from previous work but definitions are given in the paper). It's the locality that allows for the ranking functions to have a simple form (global ranking functions for SCT programs may be quite complex). But then, in the local approach, many ranking functions may be needed. This paper proves (under various sets of assumptions) that such a tradeoff is inherent.

A SAT-Based Approach to Size Change Termination with Global Ranking Functions (with Mike Codish), TACAS 2008:
We present a class of ranking functions which is strong enough for supplying termination witnesses for a significant subset of SCT instances. The subset of SCT instances covered is an NP-complete set. We have implemented an algorithm that recognizes these instances, using a SAT solver, and provides the ranking function: see SCNP in the implementations section below.

Ranking Functions for Size-Change Termination II (with Chin Soon Lee), Logical Methods in Computer Science Vol.5 Issue 2 (2009):
Improves on the complexity of global ranking functions constructed from SCT instances from triply-exponential (the upper bound known from the previous paper by CS Lee) to singly exponential, however for restricted classes of instances. We also prove matching lower bounds.

Size Change Termination, Monotonicity Constraints and Ranking Functions (Logical Methods in Computer Science, Vol.6 Issue 3, 2010):
Considers Monotonicity Constraints, a program abstraction that extends the SCT abstraction, and carries the essentials of the theory developed for SCT into this extended framework. It also presents an algorithm to construct global ranking functions for any such program, which also settles the problem of constructing GRFs for unrestricted SCT instances in singly-exponential complexity. MCs have an advantage of applicability to the Integer domain, which is not well-founded. The results are extended to this setting in:
Monotonicity Constraints for Termination in the Integer Domain (Logical Methods in Computer Science, Vol. 7 (3), 2011.).

SAT-Based Termination Analysis Using Monotonicity Constraints over the Integers (with Codish, Gonopolskiy, Fuhs and Giesl), Theory and Practice of Logic Programming, vol. 11, issue 4-5, pp. 503-520, 2011:
We introduce a class of termination witnesses, generalizing lexicographic ranking functions, designed for Integer Monotonicity Constraint Transition Systems. The subset of Constraint Transition Systems that has such witnesses is in NP and we have implemented an algorithm that recognizes these instances, using a SAT solver. We demonstrated its effectivity on benchmark suites of over 200 CTSs extracted from Java Bytecode programs by two different front-ends, and a few dozen CTSs from other sources.

Bounded Termination of Monotonicity-Constraint Transition Systems (with Michal Vainer):
We show that Monotonicity Constraint Transition Systems programs have a decidable complexity property: one can determine whether the length of all transition sequences can be bounded in terms of the initial state. We prove that the decision problem is PSPACE-complete. Moreover, if a bound exists, it must be polynomial. This may imply a complexity result for a source program from which the MCTS is extracted, depending on the source language and the way it is abstracted.

SCT Bibliography

You can see a list of every SCT-related paper I am aware of in this SCT bibliography in BibTeX format.
Don't hesitate to send additions; note however that this is not intended to be a bibliography on termination analysis in general, a very wide and deep subject indeed.

Implementations of SCT Algorithms

General comment: the SCT framework (as presented in our POPL 2001 paper) only deals with descent constraints (x ≥ y' or x > y', where the primed variable represents a value after a transition). But several of the implementations below support both types of monotonicity constraints, that is, also x ≤ y' or x < y', or otherwise incorporate SCT in a more extended program analysis framework.

Ranking Functions for Size-Change Termination: A Practical Procedure to Derive Them by Chin Soon Lee: global ranking-function generation from a set of size-change graphs. A web-demo of an algorithm more sophisticated and in general far more efficient than the one described in my paper.

SCT and SCP implementation by Chin Soon Lee: SCP stands for Size-Change termination in Polynomial time. This implementation accompanies our joint paper listed above. It was meant to compare the polynomial-time algorithm with the precise (graph closure) algorithm. The implementation of the latter is graph-based and somewhat optimized. C code is downloadable. This implementation is a back end; it can read size-change graphs in a simple ascii text format. For a front end, we used Terminweb (see below).

In this paper, James Avery analyzes C programs using a variant of the SCT method. It considers both descending and ascending values, together with information about bounded expressions to replace the well-foundedness assumption. The goal is to handle programs that compute over the integers. (The web site by is currently out of order)

William Blum's MSc Thesis includes an implementation of SCT analysis for a rudimentary high-order functional language. Source code is available.

Ariel's Snir MSc project is a demo implementation of gloabl ranking-function generation from size-change graphs or monotonicity constraints (based on the LMCS 2010 article listed above). To try out the software itself, please contact Amir Ben-Amram.

Termilog is a termination analyzer for Prolog, based on work by Lindenstrauss, Y. Sagiv and others. Terminweb is based on work by Codish, Taboch and others. Both systems include both a program analysis (that determines norms for variables and generates constraints) and a closure analysis (similar to SCT analysis). (The on-line demonstration interface of Terminweb is currently out of order)

SCNP is an SCT subset that has polynomial-size termination witnesses, namely expressions whose value decreases on every transition (ranking functions). This web-accessible analyser takes a size-change graph set and, if it is in SCNP, exhibits the ranking expression. (The web application is currently out of order)

MCNP is an implementation of a SAT-solver-based strategy to termination analysis with monotonicity constraints over the integers. It has been applied with satisfactory success to analyze constraint-transition systems obtained by abstracting imperative programs, mostly in Java; we have a web page with experimental evaluation.

On-line SCT Analyzer by Carl C. Frederiksen: analyzes programs in a simple first-order functional language, creates and graphically displays size-change graphs and performs closure computation and termination deduction. Thus, it includes both a front end (program analysis) component and a back end (termination analysis from size-change graphs, using the graph closure algorithm). (The web application is currently out of order)

A few systems that incorporate SCT analysis:

proff: a Prolog offline partial evaluator uses size-change analysis (combined with binding-time analysis) to ensure termination of partial evaluation (described in a PEPM 2007 paper).

PGG is a partial evaluator for Scheme. In this implementation by Arne Glenstrup, SCT analysis (tailored to the needs of a specializer) is used to guarantee termination.

AProVE is a termination checker targeted at term rewriting systems, but also accepting input in several programmer-oriented formalisms, including Haskell syntax. AProVE incorporates the SCT method, as described in the bibliography.

ACL2s includes a programming language (a LISP dialect) and a theorem proving system. Among other features, it now incorporates an automatic termination prover that uses SCT.

The theorem prover Isabelle now uses SCNP (see above) for verifying recursive function definitions.

the Julia termination prover for Java bytecode transforms the JBC program into a CLP (constraint logic program) which is handled by methods which resemble Terminweb above.

Open problem section

Here is a theoretical open problem suggested by our recent work on SCT and global ranking function (see "Advances in theory" above): given an SCT instance and a suitable expression for a function, it is possible to check if this is indeed a ranking function. Under natural assumptions on representation, the problem is coNP (since to prove that a function is not ranking, a single counterexample suffices). But what is its complexity class exactly?

Web Pages of My Collaborators

Neil D. Jones
Michael Codish
Jürgen Giesl
Carsten Fuhs

Footnote: I have done some other work in program analysis, unrelated to size-change termination. If you are interested, please check out my publication list.