Copenhagen Programming Language Seminar


A Complexity Tradeoff in Ranking-Function Termination Proofs

Amir M. Ben-Amram,
Academic College of Tel-Aviv, Israel

Thursday, February 15th, Time: 15:15 - 16:00
DIKU, Universitetsparken 1, Room N034


To prove that a program terminates, we can employ a ranking function argument, where all program states are ranked so that every transition decreases the rank. Alternatively, we can use a set of ranking functions with the property that every cycle in the program's flow-chart can be ranked with one of the functions. This "local" approach has gained interest recently on the grounds that local ranking functions would be simpler and easier to find. The current study is aimed at better understanding the tradeoffs involved, and at making a step from the intuitive or empirical to the formal. With this aim, we concentrate on a convenient setting, namely the Size-Change Termination framework (SCT). In SCT analysis source programs are replaced by an abstraction whose termination property is decidable. Moreover, we have an explicit characterization of sufficient classes of ranking functions (both global and local). In this setting, we will show a tradeoff: either exponenially many local functions (of certain simple types) or an exponentially complex global function may be required for proving termination.

Scientific host: Neil Jones. Administrative host: Camilla Torp-smith. All are welcome.
The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, ITU and KVL.
COPLAS is sponsored by FIRST Graduate School.
To receive information about COPLAS talks by email, send a message to prog-lang-request@mail.it-c.dk with the word 'subscribe' as subject or in the body.

For more information about COPLAS, see http://www.coplas.org