Termination Analysis and Algorithmic Synthesis of Schedulers

Speaker

Thomas Ströder, Research Group Computer Science 2

Title Termination Analysis and Algorithmic Synthesis of Schedulers
When 17.12.2008, 15.00 Uhr
Where Lecture Room Informatik 11
Abstract Termination analysis and algorithmic synthesis are different areas of research. But during my work in these fields I found an interesting connection between them. Techniques from termination analysis can also be used to solve synthesis problems. I illustrate this connection with my work on termination analysis of Prolog programs and the algorithmic synthesis of schedulers to solve the behaviour composition problem.

Termination analysis of logic programs is well studied. But most work on this field is limited to definite logic programs, while essential features of real programming languages – like the cut operator in Prolog – are ignored. In this talk I show a preprocessing method to transform a Prolog program with cuts into a new Prolog program, which is a definite logic program and where termination of the new program implies termination of the original one.

The behaviour composition problem is a general problem in teamwork situations. For a team one tries to find a scheduler telling the team members what action to perform when to realize a specified target behaviour of the team as a whole. The possible actions of the team members are constrained by their abilities on the one hand and by the environment on the other hand. The scheduler should schedule the team members in a way such that the target behaviour is reliably realized even in case of non-deterministic outcomes of the team members’ actions.

In both cases one can use a graph based technique as the core component to handle features of real programming languages in the case of termination analysis and to find an intuitive and constructive synthesis algorithm in the case of behaviour composition. The further investigation of connections between program analysis and algorithmic synthesis is a promising task where synergies can be found and used for progress in both fields.

Slides