31 October 2000, Computational Logic Seminar

31 October 2000, Computational Logic Seminar
Title: Termination Analysis: a New Perspective
Speaker: Neil Jones (DIKU, Copenhagen)
Date and Time: October 31, 2000, 13.00 - 14.00
Location: ILLC, Plantage Muidergracht 24, Amsterdam

Abstract:
A simple sufficient criterion is given to determine whether a program terminates for all input data. It is shown to be decidable but in general hard: complete for PSPACE.
THE CRITERION: Size Change Graphs are constructed from a functional program with well-founded data. Each is a local call graph "G_c" for a function call "c" appearing in the program. G_c summarizes the parameter size changes resulting from the call. The program is "size-change-terminating" if for every infinite call sequence cs = c1 c2 c3..., the concatenation G_c1 G_c2 ... has a thread (data path) with infinite descent: some value decreases infinitely often, without increase. Thus no legal computation path can be infinite, and so the program terminates in all actual runs.
ITS DECISION: The set of infinite call sequences cs = c1 c2 c3... with an infinitely descending thread is omega-regular: accepted by a finite-state Buechi or Rabin automaton. These automata have all the properties of usual finite automata on finite words, with well-understood algorithms to test for infiniteness, containment, etc. The criterion tests equality of two omega-regular sets.
This criterion is more general, and the method more automatic than traditional methods based on lexicographic and other orders. Further, reduction from a problem involving Boolean programs shows that this simple criterion is (surprisingly) also hard for PSPACE.

This is joint work with Chin Soon Lee and Amir Ben-Amram.

For more information, see http://www.illc.uva.nl/~mdr/ACLG/Local/seminar00-2.html.