|
Abstract:
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.
|