Facets of Synthesis: Revisiting Church's Problem

In this essay we discuss the origin, central results, and some perspectives of algorithmic synthesis of nonterminating reactive programs. We recall the fundamental questions raised more than 50 years ago in “Church’s Synthesis Problem” that led to the foundation of the algorithmic theory of infinite games. We outline the methodology developed in more recent years for solving such games and address related automata theoretic problems that are still unresolved. 1 Prologue The objective of “synthesis” is to pass from a specification to a program realizing it. This is a central task in computer science, and – unfortunately or fortunately, depending on the point of view – its solution cannot in general be automatized. However, there are classes of specifications for which algorithmic synthesis is possible. In the present paper we deal with a fundamental class of this kind, the regular specifications for nonterminating reactive programs. In another terminology, this amounts...

• Type: Conference
• Year: 2009
• Where: FOSSACS
• Authors: Wolfgang Thomas
• Keywords: Algorithmic, Applied Computing, FOSSACS 2009, Infinite Games, Nonterminating Reactive Programs