Universiteit van Amsterdam

Events

Institute for Logic, Language and Computation

Please note that this newsitem has been archived, and may contain outdated information or links.

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.

Please note that this newsitem has been archived, and may contain outdated information or links.